InformationTheory.Shannon.Cramer.TiltedLLN

Imports 7

Cramér lower-bound extension: tilted-side law of large numbers #

This file extends InformationTheory/Shannon/Cramer/TiltedIID.lean with the tilted-side law of large numbers for the coordinate-eval family on the infinite product measure.

Main statements #

isProbabilityMeasure_infinitePi_tilted_of_bounded — the tilted infinite product Measure.infinitePi (fun _ : ℕ => μ₀.tilted (lam * Y ·)) is a probability measure.
pairwise_indepFun_tilted_ambient, integrable_eval_under_infinitePi_tilted, integral_eval_under_infinitePi_tilted — the inputs to the strong law.
tilted_lln_ae — the almost-sure law of large numbers on the tilted ambient.
tilted_lln_in_probability, tilted_lln_in_probability_real — its in-measure (in-probability) upgrades.

Implementation notes #

isProbabilityMeasure_infinitePi_tilted_of_bounded is stated as an outward-facing lemma because Lean's typeclass synthesis does not consistently β-reduce the per-coordinate μ₀.tilted factor through the fun _ : ℕ => … wrapper when looking up IsProbabilityMeasure (Measure.infinitePi (fun _ : ℕ => μ₀.tilted ...)).

Probability-measure instance and strong-law inputs #

theorem

InformationTheory.Shannon.Cramer.TiltedLLN.isProbabilityMeasure_infinitePi_tilted_of_bounded

source

{Ω₀ : Type u_1} [MeasurableSpace Ω₀] {μ₀ : MeasureTheory.Measure Ω₀} [MeasureTheory.IsProbabilityMeasure μ₀] {Y : Ω₀ → ℝ} (hY_meas : Measurable Y) (h_bdd : ∃ (M : ℝ), ∀ (ω : Ω₀), |Y ω| ≤ M) (lam : ℝ) :

MeasureTheory.IsProbabilityMeasure (MeasureTheory.Measure.infinitePi fun (x : ℕ) => μ₀.tilted fun (ω : Ω₀) => lam * Y ω)

The infinite-product measure Measure.infinitePi (fun _ : ℕ => μ₀.tilted (lam * Y ·)) is a probability measure. Stated explicitly because the unifier does not β-reduce the per-coordinate factor through the fun _ : ℕ => ... wrapper consistently when synthesizing the standard Measure.infinitePi instance.

Used by

theorem

InformationTheory.Shannon.Cramer.TiltedLLN.pairwise_indepFun_tilted_ambient

source

Pairwise (Function.onFun (fun (X Z : (ℕ → Ω₀) → ℝ) => ProbabilityTheory.IndepFun X Z (MeasureTheory.Measure.infinitePi fun (x : ℕ) => μ₀.tilted fun (ω : Ω₀) => lam * Y ω)) fun (i : ℕ) (ω : ℕ → Ω₀) => Y (ω i))

Used by

theorem

InformationTheory.Shannon.Cramer.TiltedLLN.integrable_eval_under_infinitePi_tilted

source

MeasureTheory.Integrable (fun (ω : ℕ → Ω₀) => Y (ω 0)) (MeasureTheory.Measure.infinitePi fun (x : ℕ) => μ₀.tilted fun (ω : Ω₀) => lam * Y ω)

Used by

theorem

InformationTheory.Shannon.Cramer.TiltedLLN.integral_eval_under_infinitePi_tilted

source

(∫ (ω : ℕ → Ω₀), Y (ω 0) ∂MeasureTheory.Measure.infinitePi fun (x : ℕ) => μ₀.tilted fun (ω : Ω₀) => lam * Y ω) = ∫ (ω : Ω₀), Y ω ∂μ₀.tilted fun (ω : Ω₀) => lam * Y ω

The integral of Y ∘ eval 0 under the tilted infinite product equals the integral of Y under the tilted base.

Used by

Almost-sure LLN on the tilted ambient #

theorem

InformationTheory.Shannon.Cramer.TiltedLLN.tilted_lln_ae

source

∀ᵐ (ω : ℕ → Ω₀) ∂MeasureTheory.Measure.infinitePi fun (x : ℕ) => μ₀.tilted fun (ω : Ω₀) => lam * Y ω, Filter.Tendsto (fun (n : ℕ) => (∑ i ∈ Finset.range n, Y (ω i)) / ↑n) Filter.atTop (nhds (∫ (ω : Ω₀), Y ω ∂μ₀.tilted fun (ω : Ω₀) => lam * Y ω))

Under the tilted infinite product measure, the empirical mean of the coordinate-eval family converges almost surely to the base-tilted expectation of Y.

Used by

In-probability LLN on the tilted ambient #

theorem

InformationTheory.Shannon.Cramer.TiltedLLN.tilted_lln_in_probability

source

MeasureTheory.TendstoInMeasure (MeasureTheory.Measure.infinitePi fun (x : ℕ) => μ₀.tilted fun (ω : Ω₀) => lam * Y ω) (fun (n : ℕ) (ω : ℕ → Ω₀) => (∑ i ∈ Finset.range n, Y (ω i)) / ↑n) Filter.atTop fun (x : ℕ → Ω₀) => ∫ (ω : Ω₀), Y ω ∂μ₀.tilted fun (ω : Ω₀) => lam * Y ω

The almost-sure convergence from tilted_lln_ae upgrades to convergence in measure (= in probability on a probability space).

Used by

theorem

InformationTheory.Shannon.Cramer.TiltedLLN.tilted_lln_in_probability_real

source

Filter.Tendsto (fun (n : ℕ) => (MeasureTheory.Measure.infinitePi fun (x : ℕ) => μ₀.tilted fun (ω : Ω₀) => lam * Y ω).real {ω : ℕ → Ω₀ | ε ≤ |(∑ i ∈ Finset.range n, Y (ω i)) / ↑n - ∫ (ω : Ω₀), Y ω ∂μ₀.tilted fun (ω : Ω₀) => lam * Y ω|}) Filter.atTop (nhds 0)

The .real-form of tilted_lln_in_probability: for every ε > 0, the measure of the bad set {ω | ε ≤ |S̄_n - 𝔼[Y]|} tends to zero.

Used by