Mathlib.Information­Theory.Kl­Density­Tilt­Expansion

KL density-tilt expansion helpers: tilted measures, score moments, and second-order divergence expansions for local alternatives.

Basic 2 core · 3 supporting For a probability measure μ on a measurable space Z and a bounded, mean-zero "score" s : Z → ℝ, the linear density tilt at strength h : ℝ is the measure tiltMeasure μ s h := μ.withDensity (fun y => ENNReal.ofReal (1 + h ★ tiltMeasure★ isProbabilityMeasure_tiltMeasure

The linear density tilt and its probability-measure property

For a probability measure μ on a measurable space Z and a bounded, mean-zero "score" s : Z → ℝ, the linear density tilt at strength h : ℝ is the measure

tiltMeasure μ s h := μ.withDensity (fun y => ENNReal.ofReal (1 + h · s y)).

This file sets up that construction and proves the elementary facts needed for the second-order Kullback–Leibler expansion in KLExpansion.lean:

* tiltMeasure_absolutelyContinuous — the tilt is absolutely continuous wrt μ; * tiltDensity_nonneg — for |h| · C ≤ 1 the density 1 + h · s is ≥ 0 everywhere (bounded score |s| ≤ C); * MeasureTheory.Integrable.of_bound supplies the bounded-score integrability fact used below; * integral_tiltDensity — the density integrates to 1 (mean-zero score); * isProbabilityMeasure_tiltMeasure — hence for small |h| the tilt is a probability measure.

Reference: van der Vaart, Asymptotic Statistics, Ch. 5 (differentiability in quadratic mean / local asymptotic normality).

def tiltMeasure reviewed
Causalean.Mathlib.InformationTheory.KlDensityTiltExpansion

The linear density tilt of μ by the score s at strength h: tiltMeasure μ s h = μ.withDensity (y ↦ ENNReal.ofReal (1 + h · s y)). When 1 + h · s ≥ 0 a.e. and s is mean-zero this is again a probability measure (see isProbabilityMeasure_tiltMeasure).

Definition (Lean source)
noncomputable def tiltMeasure (μ : Measure Z) (s : Z → ℝ) (h : ℝ) : Measure Z := μ.withDensity (fun y => ofReal (1 + h * s y))
Causalean.Mathlib.InformationTheory.KlDensityTiltExpansion.tiltMeasure · Causalean/Mathlib/InformationTheory/KlDensityTiltExpansion/Basic.lean:42
lemma isProbabilityMeasure_tiltMeasure reviewed
Causalean.Mathlib.InformationTheory.KlDensityTiltExpansion

The linear tilt is a probability measure for small |h|. For a probability measure μ and a measurable score function s that is bounded by a constant C (|s y| ≤ C for every y) and has mean zero under μ, if the tilt strength satisfies |h| · C ≤ 1, then the linearly tilted measure tiltMeasure μ s h is again a probability measure.

Formal statement
hypotheses
μ :
Measure Z
IsProbabilityMeasure μ
s :
Z → ℝ
C h :
ℝ
hs_meas :
Measurable s
hsC :
∀ y, |s y| ≤ C
hs_mean :
∫ y, s y ∂μ = 0
hh :
|h| * C ≤ 1
conclusion
IsProbabilityMeasure (tiltMeasure μ s h)
Proof (Lean source)
lemma isProbabilityMeasure_tiltMeasure {μ : Measure Z} [IsProbabilityMeasure μ] {s : Z → ℝ} {C h : ℝ} (hs_meas : Measurable s) (hsC : ∀ y, |s y| ≤ C) (hs_mean : ∫ y, s y ∂μ = 0) (hh : |h| * C ≤ 1) : IsProbabilityMeasure (tiltMeasure μ s h) := by constructor have h_int : Integrable (fun y => (1 : ℝ) + h * s y) μ := (integrable_const 1).add ((Integrable.of_bound hs_meas.aestronglyMeasurable C (.of_forall hsC)).const_mul h) have h_nonneg : 0 ≤ᵐ[μ] fun y => (1 : ℝ) + h * s y := Filter.Eventually.of_forall fun y => tiltDensity_nonneg hsC hh y have hmass : (μ.withDensity (fun y => ofReal (1 + h * s y))) univ = ofReal (∫ y, (1 + h * s y) ∂μ) := by rw [withDensity_apply _ MeasurableSet.univ, Measure.restrict_univ, ← ofReal_integral_eq_lintegral_ofReal h_int h_nonneg] rw [tiltMeasure, hmass, integral_tiltDensity (Integrable.of_bound hs_meas.aestronglyMeasurable C (.of_forall hsC)) hs_mean] norm_num
Causalean.Mathlib.InformationTheory.KlDensityTiltExpansion.isProbabilityMeasure_tiltMeasure · Causalean/Mathlib/InformationTheory/KlDensityTiltExpansion/Basic.lean:94 · uses tiltMeasure
3 supporting declarations (lemmas, instances)
  • tiltMeasure_absolutelyContinuous lemma — The tilt is absolutely continuous with respect to the base measure μ (any withDensity measure is).
    hypotheses
    μ :
    Measure Z
    s :
    Z → ℝ
    h :
    ℝ
    conclusion
    tiltMeasure μ s h ≪ μ
    Proof (Lean source)
    lemma tiltMeasure_absolutelyContinuous (μ : Measure Z) (s : Z → ℝ) (h : ℝ) : tiltMeasure μ s h ≪ μ := withDensity_absolutelyContinuous _ _
    Causalean.Mathlib.InformationTheory.KlDensityTiltExpansion.tiltMeasure_absolutelyContinuous · Causalean/Mathlib/InformationTheory/KlDensityTiltExpansion/Basic.lean:49
  • tiltDensity_nonneg lemma — For a bounded score |s y| ≤ C and tilt strength with |h| · C ≤ 1, the tilt density 1 + h · s y is nonnegative: |h · s y| ≤ |h| · C ≤ 1.
    hypotheses
    s :
    Z → ℝ
    C h :
    ℝ
    hsC :
    ∀ y, |s y| ≤ C
    hh :
    |h| * C ≤ 1
    y :
    Z
    conclusion
    0 ≤ 1 + h * s y
    Proof (Lean source)
    lemma tiltDensity_nonneg {s : Z → ℝ} {C h : ℝ} (hsC : ∀ y, |s y| ≤ C) (hh : |h| * C ≤ 1) (y : Z) : 0 ≤ 1 + h * s y := by have h_abs : |h * s y| ≤ |h| * C := by rw [abs_mul] exact mul_le_mul_of_nonneg_left (hsC y) (abs_nonneg h) have h_lower : -1 ≤ h * s y := by have h_bound : -(|h| * C) ≤ h * s y := by have h_neg : -(|h| * C) ≤ -|h * s y| := by rw [neg_le_neg_iff] exact h_abs exact le_trans h_neg (neg_abs_le _) linarith linarith
    Causalean.Mathlib.InformationTheory.KlDensityTiltExpansion.tiltDensity_nonneg · Causalean/Mathlib/InformationTheory/KlDensityTiltExpansion/Basic.lean:56
  • integral_tiltDensity lemma — The tilt density integrates to 1: ∫ (1 + h · s) dμ = 1 + h · ∫ s = 1 for a probability measure μ and a mean-zero score s.
    hypotheses
    μ :
    Measure Z
    IsProbabilityMeasure μ
    s :
    Z → ℝ
    h :
    ℝ
    hs_int :
    Integrable s μ
    hs_mean :
    ∫ y, s y ∂μ = 0
    conclusion
    ∫ y, (1 + h * s y) ∂μ = 1
    Proof (Lean source)
    lemma integral_tiltDensity {μ : Measure Z} [IsProbabilityMeasure μ] {s : Z → ℝ} {h : ℝ} (hs_int : Integrable s μ) (hs_mean : ∫ y, s y ∂μ = 0) : ∫ y, (1 + h * s y) ∂μ = 1 := by calc ∫ y, (1 + h * s y) ∂μ = ∫ y, (1 : ℝ) + h * s y ∂μ := rfl _ = ∫ y, (1 : ℝ) ∂μ + ∫ y, h * s y ∂μ := by rw [integral_add (integrable_const 1) (hs_int.const_mul h)] _ = 1 + h * ∫ y, s y ∂μ := by rw [integral_const, probReal_univ, one_smul, integral_const_mul] _ = 1 := by simp [hs_mean]
    Causalean.Mathlib.InformationTheory.KlDensityTiltExpansion.integral_tiltDensity · Causalean/Mathlib/InformationTheory/KlDensityTiltExpansion/Basic.lean:75
Cubic­Remainder 1 core · 0 supporting The analytic core of the KL density-tilt expansion. ★ abs_tiltRemainder_le

Cubic Taylor remainder of (1 + x) · log (1 + x)

The analytic core of the KL density-tilt expansion. The function f x = (1 + x) · log (1 + x) has the second-order Taylor expansion f x = x + x² / 2 + O(x³) at 0, and on the band |x| ≤ 1/2 the remainder is controlled by |x|³.

Indeed f 0 = 0, f' x = log (1 + x) + 1 so f' 0 = 1, f'' x = 1 / (1 + x) so f'' 0 = 1, and f''' x = -1 / (1 + x)² with |f''' x| ≤ 1 / (1/2)² = 4 for x ≥ -1/2. The Lagrange form of Taylor's theorem then gives |f x - (x + x²/2)| ≤ (4 / 3!) · |x|³ = (2/3) · |x|³ ≤ |x|³.

This pointwise bound, applied with x = h · s y, yields the dominated o(h²) remainder in KLExpansion.lean.

lemma abs_tiltRemainder_le reviewed
Causalean.Mathlib.InformationTheory.KlDensityTiltExpansion

Cubic remainder bound for (1 + x) · log (1 + x). For a real number x with |x| ≤ 1/2, the second-order Taylor remainder of (1 + x) · log (1 + x) at 0 is bounded by |x|³:

Formal statement
hypotheses
x :
ℝ
hx :
|x| ≤ 1 / 2
conclusion
|(1 + x) * log (1 + x) - x - x ^ 2 / 2| ≤ |x| ^ 3
Proof (Lean source)
lemma abs_tiltRemainder_le {x : ℝ} (hx : |x| ≤ 1 / 2) : |(1 + x) * log (1 + x) - x - x ^ 2 / 2| ≤ |x| ^ 3 := by have hxlo : -(1 / 2 : ℝ) ≤ x := by have h := abs_le.mp hx linarith by_cases hxnonneg : 0 ≤ x · have hAmono := tiltAux_monotone_negR 0 x (by norm_num) have hBmono := tiltAux_monotone_R_add_cube 0 x (by norm_num) have hR_nonpos : (1 + x) * log (1 + x) - x - x ^ 2 / 2 ≤ 0 := by have hA : 0 ≤ x + x ^ 2 / 2 - (1 + x) * log (1 + x) := by have h := hAmono (by simp [hxnonneg]) (by simp [hxnonneg]) hxnonneg simpa using h linarith have hR_lower : -x ^ 3 ≤ (1 + x) * log (1 + x) - x - x ^ 2 / 2 := by have hB : 0 ≤ (1 + x) * log (1 + x) - x - x ^ 2 / 2 + x ^ 3 := by have h := hBmono (by simp [hxnonneg]) (by simp [hxnonneg]) hxnonneg simpa using h linarith rw [abs_of_nonpos hR_nonpos, abs_of_nonneg hxnonneg] nlinarith · have hxnonpos : x ≤ 0 := le_of_not_ge hxnonneg have hAmono := tiltAux_monotone_negR x 0 hxlo have hBmono := tiltAux_monotone_R_add_cube x 0 hxlo have hR_nonneg : 0 ≤ (1 + x) * log (1 + x) - x - x ^ 2 / 2 := by have hA : x + x ^ 2 / 2 - (1 + x) * log (1 + x) ≤ 0 := by have h := hAmono (by simp [hxnonpos]) (by simp [hxnonpos]) hxnonpos simpa using h linarith have hR_upper : (1 + x) * log (1 + x) - x - x ^ 2 / 2 ≤ -x ^ 3 := by have hB : (1 + x) * log (1 + x) - x - x ^ 2 / 2 + x ^ 3 ≤ 0 := by have h := hBmono (by simp [hxnonpos]) (by simp [hxnonpos]) hxnonpos simpa using h linarith rw [abs_of_nonneg hR_nonneg, abs_of_nonpos hxnonpos] have hpow : (-x) ^ 3 = -x ^ 3 := by ring rw [hpow] exact hR_upper
Causalean.Mathlib.InformationTheory.KlDensityTiltExpansion.abs_tiltRemainder_le · Causalean/Mathlib/InformationTheory/KlDensityTiltExpansion/CubicRemainder.lean:131
KLExpansion 3 core · 0 supporting For a probability measure μ and a bounded mean-zero score s : Z → ℝ (|s| ≤ C, ∫ s = 0), the linear tilt tiltMeasure μ s h (see Basic.lean) satisfies the local asymptotic normality / Fisher-information expansion KL(tiltMe ★ klDiv_tiltMeasure_toReal_eq★ abs_klRemainder_le★ klDiv_tilt_expansion

Second-order Kullback–Leibler expansion of the linear density tilt

For a probability measure μ and a bounded mean-zero score s : Z → ℝ (|s| ≤ C, ∫ s = 0), the linear tilt tiltMeasure μ s h (see Basic.lean) satisfies the local asymptotic normality / Fisher-information expansion

KL(tiltMeasure μ s h ‖ μ) = (h² / 2) · ∫ s² dμ + o(h²) as h → 0.

Main results

* klDiv_tiltMeasure_toReal_eq — the KL divergence is the μ-integral of the x log x density functional: (klDiv (tiltMeasure μ s h) μ).toReal = ∫ (1 + h·s) · log (1 + h·s) dμ. * abs_klRemainder_le — the dominated cubic remainder bound: for |h|·C ≤ 1/2, |KL.toReal - (h²/2)·∫ s²| ≤ C³ · |h|³. * klDiv_tilt_expansion — the headline o(h²) expansion, as an Asymptotics.IsLittleO statement.

Proof outline

1. klDiv_tiltMeasure_toReal_eq: tiltMeasure μ s h ≪ μ and both are probability measures, so toReal_klDiv_of_measure_eq gives KL.toReal = ∫ llr (tilt) μ ∂(tilt). The log-likelihood ratio llr (tilt) μ =ᵐ log (rnDeriv) =ᵐ log (1 + h·s) (rnDeriv_withDensity), and change of measure (integral_withDensity_eq_integral_toReal_smul) rewrites the tilt-integral of log (1 + h·s) as the μ-integral of (1 + h·s) · log (1 + h·s). 2. abs_klRemainder_le: write the integrand as (1 + h·s)·log(1 + h·s) = h·s + (h·s)²/2 + R(h·s) with R(x) = (1+x)log(1+x) - x - x²/2. Integrating, ∫ h·s = 0 and ∫ (h·s)²/2 = (h²/2)∫ s², so the difference equals ∫ R(h·s) dμ, bounded pointwise by abs_tiltRemainder_le (valid since |h·s| ≤ |h|·C ≤ 1/2): |∫ R(h·s)| ≤ ∫ |h·s|³ ≤ |h|³·C³ (probability measure, |s| ≤ C). 3. klDiv_tilt_expansion: from abs_klRemainder_le, `|remainder h| ≤ C³·|h|³ = (C³·|h|)·h² eventually, and C³·|h| → 0, so Asymptotics.isLittleO_iff` closes it.

lemma klDiv_tiltMeasure_toReal_eq reviewed
Causalean.Mathlib.InformationTheory.KlDensityTiltExpansion

KL of the linear tilt as an x log x density integral. For a probability measure μ and a measurable score function s that is bounded by a constant C and has mean zero under μ, if the tilt strength satisfies |h| · C ≤ 1, then the Kullback–Leibler divergence of the linearly tilted measure tiltMeasure μ s h from μ, as a real number, equals the μ-integral of (1 + h·s)·log(1 + h·s):

Formal statement
hypotheses
μ :
Measure Z
IsProbabilityMeasure μ
s :
Z → ℝ
C h :
ℝ
hs_meas :
Measurable s
hsC :
∀ y, |s y| ≤ C
hs_mean :
∫ y, s y ∂μ = 0
hh :
|h| * C ≤ 1
conclusion
(klDiv (tiltMeasure μ s h) μ).toReal
= ∫ y, (1 + h * s y) * log (1 + h * s y) ∂μ
Proof (Lean source)
lemma klDiv_tiltMeasure_toReal_eq {μ : Measure Z} [IsProbabilityMeasure μ] {s : Z → ℝ} {C h : ℝ} (hs_meas : Measurable s) (hsC : ∀ y, |s y| ≤ C) (hs_mean : ∫ y, s y ∂μ = 0) (hh : |h| * C ≤ 1) : (klDiv (tiltMeasure μ s h) μ).toReal = ∫ y, (1 + h * s y) * log (1 + h * s y) ∂μ := by let ν : Measure Z := tiltMeasure μ s h haveI : IsProbabilityMeasure ν := isProbabilityMeasure_tiltMeasure hs_meas hsC hs_mean hh have hac : ν ≪ μ := tiltMeasure_absolutelyContinuous μ s h have hf_meas : Measurable (fun y : Z => ofReal (1 + h * s y)) := by fun_prop have hf_lt_top : ∀ᵐ y ∂μ, ofReal (1 + h * s y) < ∞ := by simp have hllr : llr ν μ =ᵐ[ν] fun y => log (1 + h * s y) := by have hrnμ : ν.rnDeriv μ =ᵐ[μ] fun y => ofReal (1 + h * s y) := by simpa [ν, tiltMeasure] using (Measure.rnDeriv_withDensity μ hf_meas) filter_upwards [hrnμ.filter_mono hac.ae_le] with y hy simp [MeasureTheory.llr_def, hy, ENNReal.toReal_ofReal (tiltDensity_nonneg hsC hh y)] calc (klDiv (tiltMeasure μ s h) μ).toReal = (klDiv ν μ).toReal := rfl _ = ∫ y, llr ν μ y ∂ν := by exact InformationTheory.toReal_klDiv_of_measure_eq hac (by simp [ν]) _ = ∫ y, log (1 + h * s y) ∂ν := integral_congr_ae hllr _ = ∫ y, (ofReal (1 + h * s y)).toReal • log (1 + h * s y) ∂μ := by simpa [ν, tiltMeasure] using (integral_withDensity_eq_integral_toReal_smul hf_meas hf_lt_top (fun y : Z => log (1 + h * s y))) _ = ∫ y, (1 + h * s y) * log (1 + h * s y) ∂μ := by apply integral_congr_ae filter_upwards with y simp [ENNReal.toReal_ofReal (tiltDensity_nonneg hsC hh y), smul_eq_mul]
Causalean.Mathlib.InformationTheory.KlDensityTiltExpansion.klDiv_tiltMeasure_toReal_eq · Causalean/Mathlib/InformationTheory/KlDensityTiltExpansion/KLExpansion.lean:55 · uses tiltMeasure
lemma abs_klRemainder_le reviewed
Causalean.Mathlib.InformationTheory.KlDensityTiltExpansion

Dominated cubic remainder bound. For a probability measure μ and a measurable score function s that is bounded by a constant C and has mean zero under μ, if the tilt strength satisfies |h| · C ≤ 1, then the Kullback–Leibler divergence of the linearly tilted measure tiltMeasure μ s h from μ deviates from its second-order Taylor approximation (h²/2) · ∫ s² dμ by at most C³ · |h|³:

Formal statement
hypotheses
μ :
Measure Z
IsProbabilityMeasure μ
s :
Z → ℝ
C h :
ℝ
hs_meas :
Measurable s
hsC :
∀ y, |s y| ≤ C
hs_mean :
∫ y, s y ∂μ = 0
hh :
|h| * C ≤ 1 / 2
conclusion
|(klDiv (tiltMeasure μ s h) μ).toReal - (h ^ 2 / 2) * ∫ y, s y ^ 2 ∂μ|
≤ C ^ 3 * |h| ^ 3
Proof (Lean source)
lemma abs_klRemainder_le {μ : Measure Z} [IsProbabilityMeasure μ] {s : Z → ℝ} {C h : ℝ} (hs_meas : Measurable s) (hsC : ∀ y, |s y| ≤ C) (hs_mean : ∫ y, s y ∂μ = 0) (hh : |h| * C ≤ 1 / 2) : |(klDiv (tiltMeasure μ s h) μ).toReal - (h ^ 2 / 2) * ∫ y, s y ^ 2 ∂μ| ≤ C ^ 3 * |h| ^ 3 := by have hC : 0 ≤ C := by rcases (nonempty_of_isProbabilityMeasure μ : Nonempty Z) with ⟨z⟩ exact le_trans (abs_nonneg (s z)) (hsC z) have hh_one : |h| * C ≤ 1 := by linarith rw [klDiv_tiltMeasure_toReal_eq hs_meas hsC hs_mean hh_one] let R : Z → ℝ := fun y => (1 + h * s y) * log (1 + h * s y) - h * s y - (h * s y) ^ 2 / 2 have hR_bound : ∀ y, |R y| ≤ C ^ 3 * |h| ^ 3 := by intro y have hxs : |h * s y| ≤ |h| * C := by rw [abs_mul] exact mul_le_mul_of_nonneg_left (hsC y) (abs_nonneg h) have hsmall : |h * s y| ≤ 1 / 2 := le_trans hxs hh have hrem := abs_tiltRemainder_le (x := h * s y) hsmall have hpow : |h * s y| ^ 3 ≤ (|h| * C) ^ 3 := by exact pow_le_pow_left₀ (abs_nonneg _) hxs 3 have hprod_nonneg : 0 ≤ |h| * C := mul_nonneg (abs_nonneg h) hC have hconst_nonneg : 0 ≤ C ^ 3 * |h| ^ 3 := by positivity dsimp [R] calc |(1 + h * s y) * log (1 + h * s y) - h * s y - (h * s y) ^ 2 / 2| ≤ |h * s y| ^ 3 := hrem _ ≤ C ^ 3 * |h| ^ 3 := by nlinarith [hpow, hprod_nonneg, hconst_nonneg] have hs_int : Integrable s μ := Integrable.of_bound hs_meas.aestronglyMeasurable C (.of_forall hsC) have hs2_int : Integrable (fun y => s y ^ 2) μ := by refine Integrable.of_bound (μ := μ) (f := fun y => s y ^ 2) ?_ (C ^ 2) ?_ · fun_prop · refine .of_forall fun y => ?_ have hsq : |s y| ^ 2 ≤ C ^ 2 := pow_le_pow_left₀ (abs_nonneg _) (hsC y) 2 simpa [abs_pow, Real.norm_eq_abs] using hsq have hlin_int : Integrable (fun y => h * s y) μ := hs_int.const_mul h have hquad_int : Integrable (fun y => (h ^ 2 / 2) * s y ^ 2) μ := hs2_int.const_mul (h ^ 2 / 2) have hR_meas : Measurable R := by dsimp [R] fun_prop have hR_int : Integrable R μ := by refine Integrable.of_bound hR_meas.aestronglyMeasurable (C ^ 3 * |h| ^ 3) ?_ exact Eventually.of_forall fun y => by simpa [Real.norm_eq_abs] using hR_bound y have hmain_eq : ∫ y, (1 + h * s y) * log (1 + h * s y) ∂μ = ∫ y, h * s y ∂μ + ∫ y, (h ^ 2 / 2) * s y ^ 2 ∂μ + ∫ y, R y ∂μ := by calc ∫ y, (1 + h * s y) * log (1 + h * s y) ∂μ = ∫ y, (h * s y + (h ^ 2 / 2) * s y ^ 2) + R y ∂μ := by apply integral_congr_ae filter_upwards with y dsimp [R] ring _ = ∫ y, h * s y + (h ^ 2 / 2) * s y ^ 2 ∂μ + ∫ y, R y ∂μ := by simpa [Pi.add_apply, add_assoc] using (integral_add (hlin_int.add hquad_int) hR_int) _ = (∫ y, h * s y ∂μ) + (∫ y, (h ^ 2 / 2) * s y ^ 2 ∂μ) + ∫ y, R y ∂μ := by simpa [Pi.add_apply, add_assoc] using congrArg (fun t => t + ∫ y, R y ∂μ) (integral_add hlin_int hquad_int) have hlin_eq : ∫ y, h * s y ∂μ = 0 := by rw [integral_const_mul, hs_mean, mul_zero] have hquad_eq : ∫ y, (h ^ 2 / 2) * s y ^ 2 ∂μ = (h ^ 2 / 2) * ∫ y, s y ^ 2 ∂μ := by rw [integral_const_mul] have hrem_eq : ∫ y, (1 + h * s y) * log (1 + h * s y) ∂μ - (h ^ 2 / 2) * ∫ y, s y ^ 2 ∂μ = ∫ y, R y ∂μ := by rw [hmain_eq, hlin_eq, hquad_eq] ring calc |∫ y, (1 + h * s y) * log (1 + h * s y) ∂μ - (h ^ 2 / 2) * ∫ y, s y ^ 2 ∂μ| = |∫ y, R y ∂μ| := by rw [hrem_eq] _ = ‖∫ y, R y ∂μ‖ := by rw [Real.norm_eq_abs] _ ≤ ∫ _y, C ^ 3 * |h| ^ 3 ∂μ := by refine norm_integral_le_of_norm_le (integrable_const (C ^ 3 * |h| ^ 3)) ?_ exact Eventually.of_forall fun y => by simpa [Real.norm_eq_abs] using hR_bound y _ = C ^ 3 * |h| ^ 3 := by rw [integral_const, probReal_univ, smul_eq_mul, one_mul]
Causalean.Mathlib.InformationTheory.KlDensityTiltExpansion.abs_klRemainder_le · Causalean/Mathlib/InformationTheory/KlDensityTiltExpansion/KLExpansion.lean:105 · uses tiltMeasure
theorem klDiv_tilt_expansion reviewed
Causalean.Mathlib.InformationTheory.KlDensityTiltExpansion

Second-order KL expansion of the linear density tilt (headline result). For a probability measure μ and a measurable score function s that is bounded by a constant C and has mean zero under μ, the Kullback–Leibler divergence of the linearly tilted measure tiltMeasure μ s h from μ, as a function of the tilt strength h, agrees with the quadratic approximation (h²/2) · ∫ s² dμ up to an error that is little-o of h² as h → 0:

Formal statement
hypotheses
μ :
Measure Z
IsProbabilityMeasure μ
s :
Z → ℝ
C :
ℝ
hs_meas :
Measurable s
hsC :
∀ y, |s y| ≤ C
hs_mean :
∫ y, s y ∂μ = 0
conclusion
(fun h => (klDiv (tiltMeasure μ s h) μ).toReal - (h ^ 2 / 2) * ∫ y, s y ^ 2 ∂μ)
=o[𝓝 0] (fun h => h ^ 2)
Proof (Lean source)
theorem klDiv_tilt_expansion {μ : Measure Z} [IsProbabilityMeasure μ] {s : Z → ℝ} {C : ℝ} (hs_meas : Measurable s) (hsC : ∀ y, |s y| ≤ C) (hs_mean : ∫ y, s y ∂μ = 0) : (fun h => (klDiv (tiltMeasure μ s h) μ).toReal - (h ^ 2 / 2) * ∫ y, s y ^ 2 ∂μ) =o[𝓝 0] (fun h => h ^ 2) := by have hC : 0 ≤ C := by rcases (nonempty_of_isProbabilityMeasure μ : Nonempty Z) with ⟨z⟩ exact le_trans (abs_nonneg (s z)) (hsC z) rw [Asymptotics.isLittleO_iff] intro c hc have hsmall : ∀ᶠ h in 𝓝 (0 : ℝ), |h| * C ≤ 1 / 2 := by by_cases hC0 : C = 0 · filter_upwards with h simp [hC0] · have hCpos : 0 < C := lt_of_le_of_ne hC (Ne.symm hC0) refine Metric.eventually_nhds_iff.2 ⟨(1 / 2) / C, by positivity, ?_⟩ intro h hdist have habs : |h| < (1 / 2) / C := by simpa [Real.dist_eq, abs_sub_comm] using hdist have hmul : |h| * C < ((1 / 2) / C) * C := mul_lt_mul_of_pos_right habs hCpos have hdiv : ((1 / 2) / C) * C = 1 / 2 := by field_simp [hCpos.ne'] linarith have hcoef : ∀ᶠ h in 𝓝 (0 : ℝ), C ^ 3 * |h| ≤ c := by by_cases hC0 : C = 0 · filter_upwards with h simp [hC0, le_of_lt hc] · have hCpos : 0 < C := lt_of_le_of_ne hC (Ne.symm hC0) have hC3pos : 0 < C ^ 3 := by positivity refine Metric.eventually_nhds_iff.2 ⟨c / (C ^ 3), by positivity, ?_⟩ intro h hdist have habs : |h| < c / (C ^ 3) := by simpa [Real.dist_eq, abs_sub_comm] using hdist have hmul : |h| * C ^ 3 < (c / (C ^ 3)) * C ^ 3 := mul_lt_mul_of_pos_right habs hC3pos have hdiv : (c / (C ^ 3)) * C ^ 3 = c := by field_simp [hC3pos.ne'] have : C ^ 3 * |h| < c := by nlinarith exact le_of_lt this filter_upwards [hsmall, hcoef] with h hh_small hh_coef have hrem := abs_klRemainder_le (μ := μ) (s := s) (C := C) (h := h) hs_meas hsC hs_mean hh_small calc ‖(klDiv (tiltMeasure μ s h) μ).toReal - (h ^ 2 / 2) * ∫ y, s y ^ 2 ∂μ‖ = |(klDiv (tiltMeasure μ s h) μ).toReal - (h ^ 2 / 2) * ∫ y, s y ^ 2 ∂μ| := Real.norm_eq_abs _ _ ≤ C ^ 3 * |h| ^ 3 := hrem _ = (C ^ 3 * |h|) * |h| ^ 2 := by ring _ ≤ c * |h| ^ 2 := mul_le_mul_of_nonneg_right hh_coef (sq_nonneg |h|) _ = c * ‖h ^ 2‖ := by simp [Real.norm_eq_abs]
Causalean.Mathlib.InformationTheory.KlDensityTiltExpansion.klDiv_tilt_expansion · Causalean/Mathlib/InformationTheory/KlDensityTiltExpansion/KLExpansion.lean:210 · uses tiltMeasure