InformationTheory.Shannon.Cramer.InfinitePiTiltedChangeOfMeasure

Imports 6

infinitePi-tilted change-of-measure #

This file builds on the finite Measure.pi tilt factorization (MeasurePiTiltedFactorization.pi_tilted_sum_eq_pi_tilted) to supply the infinite-product change-of-measure machinery behind the Cramér lower bound.

Main statements #

pi_tilted_sum_eq_pi_tilted_fintype — the tilt of a finite product measure by the sum exponent factors as the product of per-coordinate tilts, generalized from Fin n to an arbitrary Fintype index.
cramer_lower_infinitePi' — the end-to-end liminf lower bound from the optimal-tilt inputs.
tiltedWindow_eventually_large_of_cgfDeriv_interior — the tilted-window mass is eventually ≥ 1/2 when the cgf derivative lands strictly inside the window.

Fintype generalization of the lintegral Fubini identity #

theorem

InformationTheory.Shannon.Cramer.TiltedLLN.lintegral_pi_prod_fintype

source

{ι : Type u_2} [Fintype ι] {E : ι → Type u_3} {mE : (i : ι) → MeasurableSpace (E i)} {μ : (i : ι) → MeasureTheory.Measure (E i)} [∀ (i : ι), MeasureTheory.SigmaFinite (μ i)] {g : (i : ι) → E i → ENNReal} (hg : ∀ (i : ι), Measurable (g i)) :

∫⁻ (x : (i : ι) → E i), ∏ i : ι, g i (x i) ∂MeasureTheory.Measure.pi μ = ∏ i : ι, ∫⁻ (ω : E i), g i ω ∂μ i

Used by

Fintype generalization of the box Tonelli and tilt factorization #

theorem

InformationTheory.Shannon.Cramer.TiltedLLN.setLIntegral_pi_prod_factor_fintype

source

{Ω₀ : Type u_1} [MeasurableSpace Ω₀] {ι : Type u_2} [Fintype ι] {μ₀ : MeasureTheory.Measure Ω₀} [MeasureTheory.IsProbabilityMeasure μ₀] {g : Ω₀ → ENNReal} (hg : Measurable g) (s : ι → Set Ω₀) (hs : ∀ (i : ι), MeasurableSet (s i)) :

(∫⁻ (x : ι → Ω₀) in Set.univ.pi s, ∏ i : ι, g (x i) ∂MeasureTheory.Measure.pi fun (x : ι) => μ₀) = ∏ i : ι, ∫⁻ (ω : Ω₀) in s i, g ω ∂μ₀

Used by

theorem

InformationTheory.Shannon.Cramer.TiltedLLN.integral_exp_sum_pi_eq_pow_fintype

source

{Ω₀ : Type u_1} [MeasurableSpace Ω₀] {ι : Type u_2} [Fintype ι] {μ₀ : MeasureTheory.Measure Ω₀} [MeasureTheory.IsProbabilityMeasure μ₀] {Y : Ω₀ → ℝ} (lam : ℝ) :

(∫ (x : ι → Ω₀), Real.exp (∑ i : ι, lam * Y (x i)) ∂MeasureTheory.Measure.pi fun (x : ι) => μ₀) = (∫ (ω : Ω₀), Real.exp (lam * Y ω) ∂μ₀) ^ Fintype.card ι

Used by

theorem

InformationTheory.Shannon.Cramer.TiltedLLN.pi_tilted_sum_eq_pi_tilted_fintype

source

{Ω₀ : Type u_1} [MeasurableSpace Ω₀] {ι : Type u_2} [Fintype ι] {μ₀ : MeasureTheory.Measure Ω₀} [MeasureTheory.IsProbabilityMeasure μ₀] {Y : Ω₀ → ℝ} (hY : Measurable Y) (lam : ℝ) :

((MeasureTheory.Measure.pi fun (x : ι) => μ₀).tilted fun (ω : ι → Ω₀) => ∑ i : ι, lam * Y (ω i)) = MeasureTheory.Measure.pi fun (x : ι) => μ₀.tilted fun (ω : Ω₀) => lam * Y ω

The tilt of a finite (Fintype) product measure by the sum exponent factors as the product of per-coordinate tilts.

Used by

End-to-end Cramér lower bound #

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, end-to-end from the cgf-derivative and cobounded inputs: the liminf lower bound -(lam·a − Λ(lam)) ≤ liminf (1/n) log P[S_n ≥ a·n] from the optimal-tilt inputs (h_deriv : deriv (cgf …) lam = a, non-degeneracy hVar, and the cobounded-below regularity h_coboundedBelow). The hypotheses hVar and h_coboundedBelow are regularity preconditions, not part of the proof core.

The prime marks a restatement: this is cramer_lower_infinitePi republished as the change-of-measure module's own entry point, with the identical statement, and the body delegates to it.

@audit:ok

Used by

theorem

InformationTheory.Shannon.Cramer.TiltedLLN.tiltedWindow_eventually_large_of_cgfDeriv_interior

source

{Ω₀ : Type u_1} [MeasurableSpace Ω₀] {μ₀ : MeasureTheory.Measure Ω₀} [MeasureTheory.IsProbabilityMeasure μ₀] {Y : Ω₀ → ℝ} (hY : Measurable Y) (h_bdd : ∃ (M : ℝ), ∀ (ω : Ω₀), |Y ω| ≤ M) (lam : ℝ) {a ε : ℝ} (h_lo : a < deriv (ProbabilityTheory.cgf Y μ₀) lam) (h_hi : deriv (ProbabilityTheory.cgf Y μ₀) lam < a + ε) :

∀ᶠ (n : ℕ) in Filter.atTop , 1 / 2 ≤ (MeasureTheory.Measure.infinitePi fun (x : ℕ) => μ₀.tilted fun (ω : Ω₀) => lam * Y ω).real {ω : ℕ → Ω₀ | a * ↑n ≤ ∑ i ∈ Finset.range n, Y (ω i) ∧ ∑ i ∈ Finset.range n, Y (ω i) < (a + ε) * ↑n}

Per-instance tilted window mass ≥ 1/2 (cgf-derivative interior case).

Whenever the cgf derivative at lam lands strictly inside the window a < deriv (cgf Y μ₀) lam < a + ε, the tilted infinite-product window mass is eventually ≥ 1/2 (indeed → 1).

This covers the interior case; the boundary case a = deriv (cgf Y μ₀) lam (= tilted mean) requires a central-limit-theorem refinement rather than the law of large numbers.

See also tiltedWindow_eventually_large_of_interior.

Used by