InformationTheory

InformationTheory.Shannon.Cramer.LC2PhaseC

source

Imports 12

Cramér lower bound on the canonical infinitePi product #

This file states the Cramér lower bound for the canonical i.i.d. infinite product setting, reducing the change-of-measure step to the CLT-boundary headline CramerCltBoundary.cramer_lower_boundary.

The change-of-measure step relates the tilted infinite-product measure Measure.infinitePi (fun _ : ℕ ↦ μ₀.tilted (lam * Y ·)) to the cylinder tilt of the un-tilted product measure (Measure.infinitePi (fun _ : ℕ ↦ μ₀)).tilted (...) on cylinders of width n, identified through the predicate IsMeasureInfinitePiTiltedEq (defined upstream in CramerBoundaryUpstream.lean).

Main statements #

Cramér lower bound and the two-sided limit #

theorem

InformationTheory.Shannon.Cramer.TiltedLLN.cramer_lower_infinitePi

source
{Ω₀ : Type u_1} [MeasurableSpace Ω₀] {μ₀ : MeasureTheory.Measure Ω₀} [MeasureTheory.IsProbabilityMeasure μ₀] {Y : Ω₀ → ℝ} (hY_meas : Measurable Y) (h_bdd : ∃ (M : ℝ), ∀ (ω : Ω₀), |Y ω| ≤ M) (a lam : ℝ) (hlam : 0 ≤ lam) (h_deriv : deriv (ProbabilityTheory.cgf (fun (ω : ℕ → Ω₀) => Y (ω 0)) (MeasureTheory.Measure.infinitePi fun (x : ℕ) => μ₀)) lam = a) (hVar : 0 < ProbabilityTheory.variance (fun (ω : ℕ → Ω₀) => Y (ω 0)) (MeasureTheory.Measure.infinitePi fun (x : ℕ) => μ₀.tilted fun (ω : Ω₀) => lam * Y ω)) (h_coboundedBelow : Filter.IsCoboundedUnder (fun (x1 x2 : ℝ) => x1 ≥ x2) Filter.atTop fun (n : ℕ) => 1 / ↑n * Real.log ((MeasureTheory.Measure.infinitePi fun (x : ℕ) => μ₀).real {ω : ℕ → Ω₀ | a * ↑n ≤ ∑ i ∈ Finset.range n, Y (ω i)})) :
-(lam * a - ProbabilityTheory.cgf (fun (ω : ℕ → Ω₀) => Y (ω 0)) (MeasureTheory.Measure.infinitePi fun (x : ℕ) => μ₀) lam) ≤ Filter.liminf (fun (n : ℕ) => 1 / ↑n * Real.log ((MeasureTheory.Measure.infinitePi fun (x : ℕ) => μ₀).real {ω : ℕ → Ω₀ | a * ↑n ≤ ∑ i ∈ Finset.range n, Y (ω i)})) Filter.atTop

The Cramér lower bound for the canonical i.i.d. product-measure setting X i ω := Y (ω i) with Y : Ω₀ → ℝ bounded and measurable, on the un-tilted infinite product μ := Measure.infinitePi (fun _ ↦ μ₀): the asymptotic liminf lower bound at threshold a and tilt lam.

The optimal-tilt hypothesis h_deriv : deriv (cgf (Y∘·0) (infinitePi μ₀)) lam = a is required for truth: without it the per-lam bound fails for general a (e.g. μ₀ = Bernoulli(1/2), Y(0)=0, Y(1)=1, lam=0, a=0.9); the bound is tight precisely at the optimal tilt, where lam·a − Λ(lam) = cramerRate a. The non-degeneracy hypothesis hVar and the cobounded-below hypothesis h_coboundedBelow are regularity preconditions, not part of the proof core.

@audit:ok (body is a verbatim exact of the headline cramer_lower_boundary. hVar is non-load-bearing: the window-mass ≥ 1/4 core is derived inside the CLT of the headline, where hVar is consumed only as the non-degeneracy input; at Var = 0 the tilted sum is a.e. constant and the argument collapses, so granting hVar alone does not hand over the conclusion.)

Used by
    theorem

    InformationTheory.Shannon.Cramer.TiltedLLN.cramer_lower_legendre_infinitePi

    source
    {Ω₀ : Type u_1} [MeasurableSpace Ω₀] {μ₀ : MeasureTheory.Measure Ω₀} [MeasureTheory.IsProbabilityMeasure μ₀] {Y : Ω₀ → ℝ} (hY_meas : Measurable Y) (h_bdd : ∃ (M : ℝ), ∀ (ω : Ω₀), |Y ω| ≤ M) (a lam : ℝ) (hlam : 0 ≤ lam) (hlam_opt : lam * a - ProbabilityTheory.cgf (fun (ω : ℕ → Ω₀) => Y (ω 0)) (MeasureTheory.Measure.infinitePi fun (x : ℕ) => μ₀) lam = cramerRate (fun (ω : ℕ → Ω₀) => Y (ω 0)) (MeasureTheory.Measure.infinitePi fun (x : ℕ) => μ₀) a) (h_deriv : deriv (ProbabilityTheory.cgf (fun (ω : ℕ → Ω₀) => Y (ω 0)) (MeasureTheory.Measure.infinitePi fun (x : ℕ) => μ₀)) lam = a) (hVar : 0 < ProbabilityTheory.variance (fun (ω : ℕ → Ω₀) => Y (ω 0)) (MeasureTheory.Measure.infinitePi fun (x : ℕ) => μ₀.tilted fun (ω : Ω₀) => lam * Y ω)) (h_coboundedBelow : Filter.IsCoboundedUnder (fun (x1 x2 : ℝ) => x1 ≥ x2) Filter.atTop fun (n : ℕ) => 1 / ↑n * Real.log ((MeasureTheory.Measure.infinitePi fun (x : ℕ) => μ₀).real {ω : ℕ → Ω₀ | a * ↑n ≤ ∑ i ∈ Finset.range n, Y (ω i)})) :
    -cramerRate (fun (ω : ℕ → Ω₀) => Y (ω 0)) (MeasureTheory.Measure.infinitePi fun (x : ℕ) => μ₀) a ≤ Filter.liminf (fun (n : ℕ) => 1 / ↑n * Real.log ((MeasureTheory.Measure.infinitePi fun (x : ℕ) => μ₀).real {ω : ℕ → Ω₀ | a * ↑n ≤ ∑ i ∈ Finset.range n, Y (ω i)})) Filter.atTop

    The Legendre form of cramer_lower_infinitePi, with the conclusion expressed as -cramerRate a. The Legendre-attainment hypothesis hlam_opt bridges lam·a − Λ(lam) to cramerRate a; together with h_deriv (optimal tilt) and hVar (non-degeneracy) these are regularity preconditions, not part of the proof core.

    @audit:ok (threads root preconditions through and rewrites the conclusion via the hlam_opt Legendre-attainment precondition. hVar, h_deriv, hlam_opt are all regularity preconditions, no load-bearing core.)

    Used by
      theorem

      InformationTheory.Shannon.Cramer.TiltedLLN.cramer_tendsto_infinitePi

      source
      {Ω₀ : Type u_1} [MeasurableSpace Ω₀] {μ₀ : MeasureTheory.Measure Ω₀} [MeasureTheory.IsProbabilityMeasure μ₀] {Y : Ω₀ → ℝ} (hY_meas : Measurable Y) (h_bdd : ∃ (M : ℝ), ∀ (ω : Ω₀), |Y ω| ≤ M) (a lam : ℝ) (hlam : 0 ≤ lam) (hlam_opt : lam * a - ProbabilityTheory.cgf (fun (ω : ℕ → Ω₀) => Y (ω 0)) (MeasureTheory.Measure.infinitePi fun (x : ℕ) => μ₀) lam = cramerRate (fun (ω : ℕ → Ω₀) => Y (ω 0)) (MeasureTheory.Measure.infinitePi fun (x : ℕ) => μ₀) a) (h_deriv : deriv (ProbabilityTheory.cgf (fun (ω : ℕ → Ω₀) => Y (ω 0)) (MeasureTheory.Measure.infinitePi fun (x : ℕ) => μ₀)) lam = a) (hVar : 0 < ProbabilityTheory.variance (fun (ω : ℕ → Ω₀) => Y (ω 0)) (MeasureTheory.Measure.infinitePi fun (x : ℕ) => μ₀.tilted fun (ω : Ω₀) => lam * Y ω)) (h_pos : ∀ᶠ (n : ℕ) in Filter.atTop, 0 < (MeasureTheory.Measure.infinitePi fun (x : ℕ) => μ₀).real {ω : ℕ → Ω₀ | a * ↑n ≤ ∑ i ∈ Finset.range n, Y (ω i)}) (h_cobdd : Filter.IsCoboundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) Filter.atTop fun (n : ℕ) => 1 / ↑n * Real.log ((MeasureTheory.Measure.infinitePi fun (x : ℕ) => μ₀).real {ω : ℕ → Ω₀ | a * ↑n ≤ ∑ i ∈ Finset.range n, Y (ω i)})) (h_coboundedBelow : Filter.IsCoboundedUnder (fun (x1 x2 : ℝ) => x1 ≥ x2) Filter.atTop fun (n : ℕ) => 1 / ↑n * Real.log ((MeasureTheory.Measure.infinitePi fun (x : ℕ) => μ₀).real {ω : ℕ → Ω₀ | a * ↑n ≤ ∑ i ∈ Finset.range n, Y (ω i)})) (h_bdd_above : Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) Filter.atTop fun (n : ℕ) => 1 / ↑n * Real.log ((MeasureTheory.Measure.infinitePi fun (x : ℕ) => μ₀).real {ω : ℕ → Ω₀ | a * ↑n ≤ ∑ i ∈ Finset.range n, Y (ω i)})) (h_bdd_below : Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≥ x2) Filter.atTop fun (n : ℕ) => 1 / ↑n * Real.log ((MeasureTheory.Measure.infinitePi fun (x : ℕ) => μ₀).real {ω : ℕ → Ω₀ | a * ↑n ≤ ∑ i ∈ Finset.range n, Y (ω i)})) :
      Filter.Tendsto (fun (n : ℕ) => 1 / ↑n * Real.log ((MeasureTheory.Measure.infinitePi fun (x : ℕ) => μ₀).real {ω : ℕ → Ω₀ | a * ↑n ≤ ∑ i ∈ Finset.range n, Y (ω i)})) Filter.atTop (nhds (-cramerRate (fun (ω : ℕ → Ω₀) => Y (ω 0)) (MeasureTheory.Measure.infinitePi fun (x : ℕ) => μ₀) a))

      Cramér's theorem (Tendsto form): the empirical log-tail rate converges to -cramerRate a. All hypotheses are regularity preconditions or cobounded side-conditions.

      See also cramer_upper_legendre and cramer_lower_legendre_infinitePi.

      @audit:ok (genuine le_antisymm-style sandwich of cramer_upper_legendre and cramer_lower_legendre_infinitePi. All hypotheses are regularity preconditions or cobounded side-conditions.)

      Used by

        Predicate interface #

        theorem

        InformationTheory.Shannon.Cramer.TiltedLLN.isMeasureInfinitePiTiltedEq_iff

        source
        {Ω₀ : Type u_1} [MeasurableSpace Ω₀] (μ₀ : MeasureTheory.Measure Ω₀) (Y : Ω₀ → ℝ) (lam : ℝ) :
        IsMeasureInfinitePiTiltedEq μ₀ Y lam ↔ ∀ (a ε : ℝ), 0 < ε → ∃ C > 0, ∀ᶠ (n : ℕ) in Filter.atTop, C * Real.exp (-↑n * (lam * a - ProbabilityTheory.cgf Y μ₀ lam + lam * ε)) ≤ (MeasureTheory.Measure.infinitePi fun (x : ℕ) => μ₀).real {ω : ℕ → Ω₀ | a * ↑n ≤ ∑ i ∈ Finset.range n, Y (ω i)}

        The defining shape ∀ a ε, ... ∃ C ... of IsMeasureInfinitePiTiltedEq, exposed for downstream callers who want to inline the construction.

        Used by