noncomputable def logMGFVec {d : ℕ} {Ω : Type u_1} [MeasurableSpace Ω] (X : Ω → EuclideanSpace ℝ (Fin d)) (μ : MeasureTheory.Measure Ω) (t : EuclideanSpace ℝ (Fin d)) : ℝ

Vector-valued cumulant generating function Λ(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.

noncomputable def empiricalMeanMeasureVec {d : ℕ} {Ω : Type u_1} [MeasurableSpace Ω] (X : ℕ → Ω → EuclideanSpace ℝ (Fin d)) (μ : MeasureTheory.Measure Ω) (n : ℕ) : MeasureTheory.Measure (EuclideanSpace ℝ (Fin d))

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ᵢ(ω). Used to state Cramér's theorem as a large deviation principle for the sequence of empirical-mean laws.

noncomputable def cramerRateFunction {d : ℕ} {Ω : Type u_1} [MeasurableSpace Ω] (X : Ω → EuclideanSpace ℝ (Fin d)) (μ : MeasureTheory.Measure Ω) (x : EuclideanSpace ℝ (Fin d)) : ENNReal

Cramér rate function Λ*(x) = sup_λ {⟨λ, x⟩ − Λ(λ)} (Lecture 13).

The Legendre transform of the cumulant generating function Λ = logMGFVec X μ, viewed as an ℝ≥0∞-valued rate function for the large deviation principle of the empirical means of i.i.d. copies of X.

theorem cramer_theorem {d : ℕ} {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : ℕ → Ω → EuclideanSpace ℝ (Fin d)} (hIndep : ProbabilityTheory.iIndepFun X μ) (hIdent : ∀ (i : ℕ), ProbabilityTheory.IdentDistrib (X i) (X 0) μ μ) (hMeas : ∀ (i : ℕ), Measurable (X i)) (hMGF : ∃ (δ : ℝ), 0 < δ ∧ ∀ (t : EuclideanSpace ℝ (Fin d)), ‖t‖ < δ → MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (inner ℝ t (X 0 ω))) μ) : SatisfiesLDP (empiricalMeanMeasureVec X μ) (cramerRateFunction (X 0) μ) ∧ IsConvexRateFunction (cramerRateFunction (X 0) μ)

Cramér's theorem (Lecture 13).

Let X₁, X₂, … be i.i.d. random vectors in ℝᵈ with common law and suppose the moment generating function t ↦ E[exp ⟨t, X⟩] is finite in a neighborhood of 0. Then the laws μₙ of the empirical means Aₙ = (1/n) ∑_{j<n} Xⱼ satisfy the large deviation principle with the convex rate function Λ*(x) = sup_λ {⟨λ, x⟩ − log E[exp ⟨λ, X⟩]}.