InformationTheory.Shannon.Cramer.TiltedIID

Imports 7

Cramér lower-bound discharge: i.i.d. plumbing #

Independence, identical-distribution, and boundedness plumbing for the coordinate-evaluation family X i := Y ∘ eval i on the infinite product Measure.infinitePi (fun _ : ℕ => μ₀) (and its per-coordinate tilt), used to discharge the tilted-side lower-bound hypothesis of the Cramér lower bound.

Main statements #

cgf_eval_eq_cgf_base — the CGF bridge cgf (Y ∘ eval i) (infinitePi μ₀) = cgf Y μ₀, aligning the Cramér exponent across the two sides.
iIndepFun_tilted_ambient, identDistrib_tilted_ambient — independence and identical distribution of the coordinate-eval family under the tilted ambient.
iIndepFun_eval_under_infinitePi, identDistrib_eval_under_infinitePi, bounded_eval_family — the same plumbing under the un-tilted base product.

Tilted ambient and n-IID plumbing #

theorem

InformationTheory.Shannon.Cramer.TiltedLLN.cgf_eval_eq_cgf_base

source

{Ω₀ : Type u_1} [MeasurableSpace Ω₀] {μ₀ : MeasureTheory.Measure Ω₀} [MeasureTheory.IsProbabilityMeasure μ₀] {Y : Ω₀ → ℝ} (hY_meas : Measurable Y) (i : ℕ) (t : ℝ) :

ProbabilityTheory.cgf (fun (ω : ℕ → Ω₀) => Y (ω i)) (MeasureTheory.Measure.infinitePi fun (x : ℕ) => μ₀) t = ProbabilityTheory.cgf Y μ₀ t

The CGF bridge cgf (Y ∘ eval i) (infinitePi (fun _ => μ₀)) = cgf Y μ₀, aligning the Cramér exponent across the infinitePi side and the per-coordinate μ₀ side.

Used by

theorem

InformationTheory.Shannon.Cramer.TiltedLLN.iIndepFun_tilted_ambient

source

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

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

Under the tilted ambient, the coordinate-eval family is iIndepFun.

Used by

theorem

InformationTheory.Shannon.Cramer.TiltedLLN.identDistrib_tilted_ambient

source

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

Under the tilted ambient, each coordinate-eval Y ∘ eval i is identically distributed to Y ∘ eval 0.

Used by

Coordinate-eval family under the un-tilted base product #

theorem

InformationTheory.Shannon.Cramer.TiltedLLN.iIndepFun_eval_under_infinitePi

source

{Ω₀ : Type u_1} [MeasurableSpace Ω₀] {μ₀ : MeasureTheory.Measure Ω₀} [MeasureTheory.IsProbabilityMeasure μ₀] {Y : Ω₀ → ℝ} (hY_meas : Measurable Y) :

ProbabilityTheory.iIndepFun (fun (i : ℕ) (ω : ℕ → Ω₀) => Y (ω i)) (MeasureTheory.Measure.infinitePi fun (x : ℕ) => μ₀)

The coordinate-eval family X i ω := Y (ω i) is iIndepFun under infinitePi μ₀ (the un-tilted base product measure).

Used by

theorem

InformationTheory.Shannon.Cramer.TiltedLLN.identDistrib_eval_under_infinitePi

source

{Ω₀ : Type u_1} [MeasurableSpace Ω₀] {μ₀ : MeasureTheory.Measure Ω₀} [MeasureTheory.IsProbabilityMeasure μ₀] {Y : Ω₀ → ℝ} (hY_meas : Measurable Y) (i : ℕ) :

ProbabilityTheory.IdentDistrib (fun (ω : ℕ → Ω₀) => Y (ω i)) (fun (ω : ℕ → Ω₀) => Y (ω 0)) (MeasureTheory.Measure.infinitePi fun (x : ℕ) => μ₀) (MeasureTheory.Measure.infinitePi fun (x : ℕ) => μ₀)

The coordinate-eval family is identically distributed under infinitePi μ₀ (un-tilted).

Used by

theorem

InformationTheory.Shannon.Cramer.TiltedLLN.bounded_eval_family

source

{Ω₀ : Type u_1} {Y : Ω₀ → ℝ} (h_bdd : ∃ (M : ℝ), ∀ (ω : Ω₀), |Y ω| ≤ M) :

∃ (M : ℝ), ∀ (i : ℕ) (ω : ℕ → Ω₀), |Y (ω i)| ≤ M

The coordinate-eval family X i ω := Y (ω i) is bounded by the same M that bounds Y.

Used by