InformationTheory.Shannon.CramerGeneralLower

Imports 3

Cramér lower bound — general i.i.d. #

The Cramér lower-bound chain (cramer_lower / cramer_lower_legendre / cramer_tendsto) for the general i.i.d. statement on an arbitrary bounded μ : Measure Ω, X : ℕ → Ω → ℝ, reduced to the CLT-boundary headline cramer_lower_boundary.

Main statements #

cramer_lower, cramer_lower_legendre — the liminf lower bound at threshold a and optimal tilt lam, in Chernoff-exponent and Legendre forms.
cramer_tendsto — the two-sided Tendsto form of Cramér's theorem.

Implementation notes #

The general i.i.d. statement transports to the canonical infinitePi specialization: the joint law of X equals an infinite product (iIndepFun_iff_map_fun_eq_infinitePi_map), the identical marginals unify to ν := μ.map (X 0) (IdentDistrib.map_eq), the partial-sum event masses agree by pullback through the two joint maps, and the cgf transports through the coordinate-evaluation bridge cgf_eval_eq_cgf_base.

The non-degeneracy variance precondition hVar excludes the degenerate constant-RV case (Var = 0), where the Cramér boundary argument genuinely breaks (Gaussian median 1/2 / window mass 1/4 lower bounds collapse).

References #

T. M. Cover and J. A. Thomas, Elements of Information Theory (2nd ed.), Wiley, 2006.

theorem

InformationTheory.Shannon.Cramer.cramer_lower

source

-(lam * a - ProbabilityTheory.cgf (X 0) μ lam) ≤ Filter.liminf (fun (n : ℕ) => 1 / ↑n * Real.log (μ.real {ω : Ω | a * ↑n ≤ ∑ i ∈ Finset.range n, X i ω})) Filter.atTop

Cramér's theorem (lower bound, general i.i.d.).

The optimal-tilt hypothesis h_deriv : deriv (cgf (X 0) μ) lam = a makes the per-lam Chernoff exponent -(lam·a − Λ(lam)) a genuine lower bound for the tail rate. hVar (non-degenerate variance) is a regularity precondition, not a load-bearing core — the window-mass core is supplied internally by the CLT inside the headline.

@audit:ok (Transport is a GENUINE reduction (not a false implication): both the general-iid joint law μ.map g and the canonical copy P.map g₀ push forward to the SAME infinitePi (μ.map (X 0)) — h_indep is genuinely consumed by iIndepFun_iff_map_fun_eq_infinitePi_map and h_ident by IdentDistrib.map_eq to factor the marginals; the partial-sum event masses then agree by double pullback (hpreB/hpre0 correct). h_bdd0 correctly specializes h_bdd to X 0 (i=0 instance); h_deriv' is a sound rewrite of h_deriv through the cgf bridge cgf_eval_eq_cgf_base; hVar is passed verbatim to the headline (matching form, no under-hypothesization) and is a precondition (non-degeneracy), not load-bearing.)

Used by

theorem

InformationTheory.Shannon.Cramer.cramer_lower_legendre

source

-cramerRate (X 0) μ a ≤ Filter.liminf (fun (n : ℕ) => 1 / ↑n * Real.log (μ.real {ω : Ω | a * ↑n ≤ ∑ i ∈ Finset.range n, X i ω})) Filter.atTop

Cramér's theorem (lower bound, Legendre form).

InformationTheory.Shannon.Cramer.cramer_tendsto

source

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

Filter.Tendsto (fun (n : ℕ) => 1 / ↑n * Real.log (μ.real {ω : Ω | a * ↑n ≤ ∑ i ∈ Finset.range n, X i ω})) Filter.atTop (nhds (-cramerRate (X 0) μ a))

Cramér's theorem (Tendsto form): the empirical log-tail rate converges to -cramerRate (X 0) μ a.

See also cramer_upper_legendre and cramer_lower_legendre.

@audit:ok (genuine sandwich of the constructive upper bound and the headline-backed lower bound. All hypotheses are regularity preconditions / cobounded-bounded side-conditions.)

Used by