Cramér's theorem

DefinitionLaw of the empirical mean#✓fully proved

Law of the empirical mean Aₙ = (1/n) ∑_{i<n} Xᵢ for an ℝᵈ-valued sample.

Pushforward of μ under the map ω ↦ (1/n) ∑_{i<n} Xᵢ(ω). Ported verbatim from v1.

noncomputable def empiricalMeanMeasureVec {d : ℕ} (X : ℕ → Ω → EuclideanSpace ℝ (Fin d))
    (μ : Measure Ω) (n : ℕ) : Measure (EuclideanSpace ℝ (Fin d)) :=
  μ.map (fun ω => (n : ℝ)⁻¹ • (∑ i ∈ Finset.range n, X i ω))

Used by 2

Used byFixed-direction Chernoff bound · Fixed-direction Chernoff bound, rate form

DefinitionReal-valued log-MGF expression#✓fully proved

Real-valued log-MGF expression Λ(t) = log E[exp ⟪t, X⟫].

For a random vector X : Ω → ℝᵈ, this returns the logarithm of the moment generating function evaluated at the dual variable t ∈ ℝᵈ, using the Euclidean inner product. Under a probability measure it represents the cumulant generating function at directions where the exponential is integrable. For a nonintegrable exponential, the Bochner integral is 0 and Real.log 0 = 0, so this definition returns 0. The bounds below explicitly require exponential integrability. Ported from v1.

noncomputable def logMGFVec {d : ℕ} (X : Ω → EuclideanSpace ℝ (Fin d))
    (μ : Measure Ω) (t : EuclideanSpace ℝ (Fin d)) : ℝ :=
  Real.log (∫ ω, Real.exp ⟪t, X ω⟫_ℝ ∂μ)

Used by 10

Used byCramér rate function as a supremum when all moments are integrable · Cramér rate function as a real supremum under finite moments · Cramér rate function vanishes at the mean · Fixed-direction Chernoff bound · Fixed-direction Chernoff bound, rate form · Extended log moment of a constant vector · Extended log moment agrees with the real one at integrable directions · Fenchel–Young lower bound at integrable directions · Log moment generating function of a constant vector · Log moment generating function vanishes at zero

TheoremChernoff bound for the empirical mean of real-valued i.i.d. variables#✓fully proved

Chernoff bound for the empirical mean of real-valued i.i.d. variables, in event form: if on the event E the empirical mean (1/n) ∑_{i<n} Xᵢ satisfies the threshold inequality a ≤ t * (empirical mean) - log (mgf of X₁ at t), then μ(E) ≤ exp(-n * a).

Assume a probability measure, measurable independent identically distributed coordinates, and integrability of exp (t * X₀).

This is the one-dimensional core of the Cramér upper bound. The proof splits on the sign of t: for t > 0 it applies Mathlib's upper-tail Chernoff bound to the sum Sₙ, and for t < 0 the lower-tail Chernoff bound; in both cases the exponential moment of the sum factors as (mgf of X₁ at t)^n by independence and identical distribution.

theorem measure_empiricalMean_le_of_threshold {X : ℕ → Ω → ℝ}
    [IsProbabilityMeasure μ]
    (hXmeas : ∀ i, Measurable (X i)) (hXindep : iIndepFun X μ)
    (hXident : ∀ i, IdentDistrib (X i) (X 0) μ μ)
    {t a : ℝ} (hInt : Integrable (fun ω => Real.exp (t * X 0 ω)) μ)
    {n : ℕ} (hn : 0 < n) {E : Set Ω}
    (hEthr : ∀ ω ∈ E, a ≤ t * ((n : ℝ)⁻¹ * ∑ i ∈ Finset.range n, X i ω)
      - Real.log (mgf (X 0) μ t)) :
    (μ E).toReal ≤ Real.exp (-(n : ℝ) * a)

Used by 1

Used byFixed-direction Chernoff bound

TheoremFixed-direction Chernoff bound#✓fully proved

For i.i.d. random vectors in ℝᵈ, the law μₙ of the empirical mean satisfies μₙ(F) ≤ exp(-n * a) whenever a lower-bounds ⟪ξ, ·⟫ - Λ(ξ) on measurable F. Assume a probability measure, measurable coordinates and integrability of exp ⟪ξ, X₀⟫ at this direction.

theorem cramer_upper_bound {d : ℕ} {X : ℕ → Ω → EuclideanSpace ℝ (Fin d)}
    [IsProbabilityMeasure μ]
    (hXmeas : ∀ i, Measurable (X i)) (hXindep : iIndepFun X μ)
    (hXident : ∀ i, IdentDistrib (X i) (X 0) μ μ)
    {F : Set (EuclideanSpace ℝ (Fin d))} (hF : MeasurableSet F)
    {ξ : EuclideanSpace ℝ (Fin d)} {a : ℝ}
    (hInt : Integrable (fun ω => Real.exp ⟪ξ, X 0 ω⟫_ℝ) μ)
    (ha : ∀ x ∈ F, a ≤ ⟪ξ, x⟫_ℝ - logMGFVec (X 0) μ ξ) (n : ℕ) :
    ((empiricalMeanMeasureVec X μ n) F).toReal ≤ Real.exp (-(n : ℝ) * a)

Uses 3 · Used by 1

Statement usesLaw of the empirical mean · Real-valued log-MGF expression

Proof usesChernoff bound for the empirical mean of real-valued i.i.d. variables

Used byFixed-direction Chernoff bound, rate form

TheoremFixed-direction Chernoff bound, rate form#✓fully proved

For a fixed ξ and s = inf_{x ∈ F} (⟪ξ, x⟫ - Λ(ξ)), the n-th root of μₙ(F) has limsup at most exp(-s). Assume measurable i.i.d. coordinates under a probability measure, measurable F, exponential integrability at ξ, and a bounded-below rate image on F, with its real-valued sInf used for s. Optimizing over admissible ξ gives the supremum of these fixed-direction rates; the Legendre-rate Cramér upper bound requires further arguments.

theorem cramer_upper_bound_rate {d : ℕ} {X : ℕ → Ω → EuclideanSpace ℝ (Fin d)}
    [IsProbabilityMeasure μ]
    (hXmeas : ∀ i, Measurable (X i)) (hXindep : iIndepFun X μ)
    (hXident : ∀ i, IdentDistrib (X i) (X 0) μ μ)
    {F : Set (EuclideanSpace ℝ (Fin d))} (hF : MeasurableSet F)
    {ξ : EuclideanSpace ℝ (Fin d)}
    (hInt : Integrable (fun ω => Real.exp ⟪ξ, X 0 ω⟫_ℝ) μ)
    (hBdd : BddBelow ((fun x => ⟪ξ, x⟫_ℝ - logMGFVec (X 0) μ ξ) '' F)) :
    limsup (fun n : ℕ => ((empiricalMeanMeasureVec X μ n) F).toReal ^ (1 / (n : ℝ)))
        atTop ≤
      Real.exp (-sInf ((fun x => ⟪ξ, x⟫_ℝ - logMGFVec (X 0) μ ξ) '' F))

Uses 3

Statement usesLaw of the empirical mean · Real-valued log-MGF expression

Proof usesFixed-direction Chernoff bound

DefinitionExtended log moment generating function of a random vector#✓fully proved

Extended log moment: nonintegrable measurable exponential moments give ⊤.

noncomputable def extendedLogMGFVec {d : ℕ} (X : Ω → EuclideanSpace ℝ (Fin d))
    (μ : Measure Ω) (t : EuclideanSpace ℝ (Fin d)) : EReal :=
  ENNReal.log (∫⁻ ω, ENNReal.ofReal (Real.exp ⟪t, X ω⟫_ℝ) ∂μ)

Used by 14

Used byCramér rate function agrees with the extended conjugate · Cramér rate function · Cramér rate function of a constant law · Convexity of the Cramér rate function · Cramér rate function as a supremum · Cramér rate function as a supremum when all moments are integrable · Extended log moment of a constant vector · Extended log moment agrees with the real one at integrable directions · Extended log moment is infinite at non-integrable directions · Extended log moment vanishes at zero · Extended Fenchel–Young inequality for the Cramér rate function · Fenchel–Young lower bound at integrable directions · Nonnegativity of the Legendre transform of the log moment · Lower semicontinuity of the Cramér rate function

DefinitionCramér rate function#✓fully proved

The canonical extended conjugate, converted with top preserved.

noncomputable def cramerRateFunction {d : ℕ} (X : Ω → EuclideanSpace ℝ (Fin d))
    (μ : Measure Ω) (x : EuclideanSpace ℝ (Fin d)) : ℝ≥0∞ :=
  (MathlibExt.Probability.LegendreTransform.legendreTransform (extendedLogMGFVec X μ) x).toENNReal

Uses 2 · Used by 11

Statement usesExtended log moment generating function of a random vector · Legendre transform

Used byCramér rate function agrees with the extended conjugate · Cramér rate function of a constant law · Convexity of the Cramér rate function · Cramér rate function as a supremum · Cramér rate function as a supremum when all moments are integrable · Cramér rate function as a real supremum under finite moments · Cramér rate function vanishes at the mean · Cramér rate function is a convex rate function · Extended Fenchel–Young inequality for the Cramér rate function · Fenchel–Young lower bound at integrable directions · Lower semicontinuity of the Cramér rate function

TheoremLog moment generating function vanishes at zero#✓fully proved

The canonical real log moment is zero at the zero direction.

theorem logMGFVec_zero {d : ℕ} (X : Ω → EuclideanSpace ℝ (Fin d))
    [IsProbabilityMeasure μ] :
    MathlibExt.Probability.CramerUpperBound.logMGFVec X μ 0 = 0

Uses 1

Statement usesReal-valued log-MGF expression

TheoremLog moment generating function of a constant vector#✓fully proved

The canonical real log moment of a constant vector.

theorem logMGFVec_const {d : ℕ} (c : EuclideanSpace ℝ (Fin d))
    [IsProbabilityMeasure μ] (t : EuclideanSpace ℝ (Fin d)) :
    MathlibExt.Probability.CramerUpperBound.logMGFVec (fun _ => c) μ t = ⟪t, c⟫_ℝ

Uses 1 · Used by 1

Statement usesReal-valued log-MGF expression

Used byExtended log moment of a constant vector

TheoremExtended log moment agrees with the real one at integrable directions#✓fully proved

Finite directions compose with the existing fixed-direction Chernoff API.

theorem extendedLogMGFVec_eq_coe_logMGFVec {d : ℕ}
    (X : Ω → EuclideanSpace ℝ (Fin d)) [IsProbabilityMeasure μ]
    {t : EuclideanSpace ℝ (Fin d)}
    (hInt : Integrable (fun ω => Real.exp ⟪t, X ω⟫_ℝ) μ) :
    extendedLogMGFVec X μ t =
      ((MathlibExt.Probability.CramerUpperBound.logMGFVec X μ t : ℝ) : EReal)

Uses 2 · Used by 3

Statement usesExtended log moment generating function of a random vector · Real-valued log-MGF expression

Used byCramér rate function as a supremum when all moments are integrable · Extended log moment of a constant vector · Fenchel–Young lower bound at integrable directions

TheoremExtended log moment is infinite at non-integrable directions#✓fully proved

Measurability separates infinite moments from nonmeasurable totalized integrals.

theorem extendedLogMGFVec_eq_top_of_not_integrable {d : ℕ}
    (X : Ω → EuclideanSpace ℝ (Fin d)) (μ : Measure Ω)
    {t : EuclideanSpace ℝ (Fin d)}
    (hmeas : AEStronglyMeasurable (fun ω => Real.exp ⟪t, X ω⟫_ℝ) μ)
    (hInt : ¬ Integrable (fun ω => Real.exp ⟪t, X ω⟫_ℝ) μ) :
    extendedLogMGFVec X μ t = ⊤

Uses 1

Statement usesExtended log moment generating function of a random vector

TheoremExtended log moment vanishes at zero#✓fully proved

The zero direction has extended log moment zero under probability.

theorem extendedLogMGFVec_zero {d : ℕ} (X : Ω → EuclideanSpace ℝ (Fin d))
    [IsProbabilityMeasure μ] : extendedLogMGFVec X μ 0 = 0

Uses 1 · Used by 1

Statement usesExtended log moment generating function of a random vector

Used byNonnegativity of the Legendre transform of the log moment

TheoremExtended log moment of a constant vector#✓fully proved

Extended log moments of constant vectors retain the exact inner product.

theorem extendedLogMGFVec_const {d : ℕ} (c : EuclideanSpace ℝ (Fin d))
    [IsProbabilityMeasure μ] (t : EuclideanSpace ℝ (Fin d)) :
    extendedLogMGFVec (fun _ => c) μ t = ((⟪t, c⟫_ℝ : ℝ) : EReal)

Uses 4 · Used by 1

Statement usesExtended log moment generating function of a random vector

Proof usesExtended log moment agrees with the real one at integrable directions · Log moment generating function of a constant vector · Real-valued log-MGF expression

Used byCramér rate function of a constant law

TheoremCramér rate function as a supremum#✓fully proved

Supporting terms are obtained from the canonical conjugate, not a second transform.

theorem cramerRateFunction_eq_iSup {d : ℕ} (X : Ω → EuclideanSpace ℝ (Fin d))
    (μ : Measure Ω) (x : EuclideanSpace ℝ (Fin d)) :
    cramerRateFunction X μ x =
      ⨆ t, (((⟪t, x⟫_ℝ : ℝ) : EReal) - extendedLogMGFVec X μ t).toENNReal

Uses 4 · Used by 1

Statement usesCramér rate function · Extended log moment generating function of a random vector

Proof usesLegendre transform · Supremum formula for the Legendre transform

Used byCramér rate function as a supremum when all moments are integrable

TheoremExtended Fenchel–Young inequality for the Cramér rate function#✓fully proved

Extended Fenchel–Young, valid for every measure and every direction.

theorem le_cramerRateFunction {d : ℕ} (X : Ω → EuclideanSpace ℝ (Fin d))
    (μ : Measure Ω) (x t : EuclideanSpace ℝ (Fin d)) :
    (((⟪t, x⟫_ℝ : ℝ) : EReal) - extendedLogMGFVec X μ t).toENNReal ≤
      cramerRateFunction X μ x

Uses 4 · Used by 1

Statement usesCramér rate function · Extended log moment generating function of a random vector

Proof usesFenchel–Young inequality for the Legendre transform · Legendre transform

Used byFenchel–Young lower bound at integrable directions

TheoremFenchel–Young lower bound at integrable directions#✓fully proved

The original real supporting term remains valid at integrable directions.

theorem le_cramerRateFunction_of_integrable {d : ℕ}
    (X : Ω → EuclideanSpace ℝ (Fin d)) [IsProbabilityMeasure μ]
    (x t : EuclideanSpace ℝ (Fin d))
    (hInt : Integrable (fun ω => Real.exp ⟪t, X ω⟫_ℝ) μ) :
    ENNReal.ofReal (⟪t, x⟫_ℝ - MathlibExt.Probability.CramerUpperBound.logMGFVec X μ t) ≤
      cramerRateFunction X μ x

Uses 5

Statement usesCramér rate function · Real-valued log-MGF expression

Proof usesExtended log moment generating function of a random vector · Extended log moment agrees with the real one at integrable directions · Extended Fenchel–Young inequality for the Cramér rate function

TheoremNonnegativity of the Legendre transform of the log moment#✓fully proved

Probability makes the canonical conjugate nonnegative via the zero direction.

theorem legendreTransform_extendedLogMGFVec_nonneg {d : ℕ}
    (X : Ω → EuclideanSpace ℝ (Fin d)) [IsProbabilityMeasure μ]
    (x : EuclideanSpace ℝ (Fin d)) :
    0 ≤ MathlibExt.Probability.LegendreTransform.legendreTransform (extendedLogMGFVec X μ) x

Uses 4 · Used by 1

Statement usesExtended log moment generating function of a random vector · Legendre transform

Proof usesExtended log moment vanishes at zero · Fenchel–Young inequality for the Legendre transform

Used byCramér rate function agrees with the extended conjugate

TheoremCramér rate function agrees with the extended conjugate#✓fully proved

Under probability the conversion preserves the entire nonnegative conjugate.

theorem coe_cramerRateFunction {d : ℕ} (X : Ω → EuclideanSpace ℝ (Fin d))
    [IsProbabilityMeasure μ] (x : EuclideanSpace ℝ (Fin d)) :
    ((cramerRateFunction X μ x : ℝ≥0∞) : EReal) =
      MathlibExt.Probability.LegendreTransform.legendreTransform (extendedLogMGFVec X μ) x

Uses 4

Statement usesCramér rate function · Extended log moment generating function of a random vector · Legendre transform

Proof usesNonnegativity of the Legendre transform of the log moment

TheoremLower semicontinuity of the Cramér rate function#✓fully proved

Converted canonical conjugates are lower semicontinuous for arbitrary input data.

theorem lowerSemicontinuous_cramerRateFunction {d : ℕ}
    (X : Ω → EuclideanSpace ℝ (Fin d)) (μ : Measure Ω) :
    LowerSemicontinuous (cramerRateFunction X μ)

Uses 4 · Used by 1

Statement usesCramér rate function

Proof usesExtended log moment generating function of a random vector · Legendre transform · Supremum formula for the Legendre transform

Used byCramér rate function is a convex rate function

TheoremConvexity of the Cramér rate function#✓fully proved

Convexity is transported from the actual canonical conjugate epigraph.

theorem cramerRateFunction_convex {d : ℕ} (X : Ω → EuclideanSpace ℝ (Fin d))
    (μ : Measure Ω) {x y : EuclideanSpace ℝ (Fin d)} {a b : ℝ}
    (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) :
    cramerRateFunction X μ (a • x + b • y) ≤
      ENNReal.ofReal a * cramerRateFunction X μ x +
        ENNReal.ofReal b * cramerRateFunction X μ y

Uses 4 · Used by 1

Statement usesCramér rate function

Proof usesExtended log moment generating function of a random vector · The epigraph of the Legendre transform is convex · Legendre transform

Used byCramér rate function is a convex rate function

TheoremCramér rate function is a convex rate function#✓fully proved

The existing LDP convex-rate structure is available without global MGF finiteness.

theorem isConvexRateFunction_cramerRateFunction {d : ℕ}
    (X : Ω → EuclideanSpace ℝ (Fin d)) (μ : Measure Ω) :
    MathlibExt.Probability.LargeDeviationPrinciple.IsConvexRateFunction
      (cramerRateFunction X μ)

Uses 5

Statement usesCramér rate function · Convex rate function

Proof usesConvexity of the Cramér rate function · Lower semicontinuity of the Cramér rate function · Rate function

TheoremCramér rate function as a supremum when all moments are integrable#✓fully proved

With all moments integrable, the canonical real expression represents every direction.

theorem cramerRateFunction_eq_iSup_of_integrable {d : ℕ}
    (X : Ω → EuclideanSpace ℝ (Fin d)) [IsProbabilityMeasure μ]
    (hInt : ∀ t : EuclideanSpace ℝ (Fin d), Integrable (fun ω => Real.exp ⟪t, X ω⟫_ℝ) μ)
    (x : EuclideanSpace ℝ (Fin d)) :
    cramerRateFunction X μ x =
      ⨆ t, ENNReal.ofReal (⟪t, x⟫_ℝ - MathlibExt.Probability.CramerUpperBound.logMGFVec X μ t)

Uses 5 · Used by 2

Statement usesCramér rate function · Real-valued log-MGF expression

Proof usesCramér rate function as a supremum · Extended log moment generating function of a random vector · Extended log moment agrees with the real one at integrable directions

Used byCramér rate function as a real supremum under finite moments · Cramér rate function vanishes at the mean

TheoremCramér rate function as a real supremum under finite moments#✓fully proved

Physical finite-domain agreement: bounded real supporting values and integrable moments. The finiteness premise belongs to this corollary, not the corrected definitions.

theorem cramerRateFunction_eq_ofReal_iSup {d : ℕ} (X : Ω → EuclideanSpace ℝ (Fin d))
    (μ : Measure Ω) [IsProbabilityMeasure μ]
    (hInt : ∀ t : EuclideanSpace ℝ (Fin d), Integrable (fun ω => Real.exp ⟪t, X ω⟫_ℝ) μ)
    {x : EuclideanSpace ℝ (Fin d)}
    (hbdd : BddAbove (Set.range fun t =>
      ⟪t, x⟫_ℝ - MathlibExt.Probability.CramerUpperBound.logMGFVec X μ t)) :
    cramerRateFunction X μ x =
      ENNReal.ofReal (⨆ t, ⟪t, x⟫_ℝ - MathlibExt.Probability.CramerUpperBound.logMGFVec X μ t)

Uses 3

Statement usesCramér rate function · Real-valued log-MGF expression

Proof usesCramér rate function as a supremum when all moments are integrable

TheoremCramér rate function vanishes at the mean#✓fully proved

The original integrable-vector and moment premises imply zero rate at the mean.

theorem cramerRateFunction_eq_zero_at_mean {d : ℕ}
    (X : Ω → EuclideanSpace ℝ (Fin d)) [IsProbabilityMeasure μ]
    (hX : Integrable X μ)
    (hInt : ∀ t : EuclideanSpace ℝ (Fin d), Integrable (fun ω => Real.exp ⟪t, X ω⟫_ℝ) μ) :
    cramerRateFunction X μ (∫ ω, X ω ∂μ) = 0

Uses 3

Statement usesCramér rate function

Proof usesCramér rate function as a supremum when all moments are integrable · Real-valued log-MGF expression

TheoremCramér rate function of a constant law#✓fully proved

Constant laws retain zero at their center and top elsewhere, including dimension zero.

theorem cramerRateFunction_const {d : ℕ} (c : EuclideanSpace ℝ (Fin d))
    [IsProbabilityMeasure μ] :
    cramerRateFunction (fun _ => c) μ c = 0 ∧
    ∀ x : EuclideanSpace ℝ (Fin d),
      x ≠ c → cramerRateFunction (fun _ => c) μ x = ⊤

Uses 7

Statement usesCramér rate function

Proof usesExtended log moment generating function of a random vector · Extended log moment of a constant vector · Legendre transform · Supremum formula for the Legendre transform · Legendre transform of the zero function at the origin · Legendre transform of the zero function away from the origin

25 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.