Stat.Concentration.Entropy­Method

Entropy-method concentration: entropy tensorization, deletion-coordinate logarithmic-Sobolev bounds, and Bousquet-style empirical-supremum tails.

Basic 3 core · 2 supporting This file defines the entropy functional used by the entropy method and proves its Gibbs variational characterization for strictly positive integrable functions. ★ entropy_isGreatest_dual

Entropy of a nonnegative random variable

This file defines the entropy functional used by the entropy method and proves its Gibbs variational characterization for strictly positive integrable functions. The characterization is the elementary analytic input to entropy tensorization.

The formulation is real-valued. Later tensorization and Herbst results impose boundedness, which guarantees all the integrability hypotheses appearing here.

def entropy reviewed
Causalean.Stat.Concentration.EntropyMethod

Given a measure μ and a real-valued function f, the entropy of f under μ is its expected f log f minus its mean times the logarithm of its mean.

Definition (Lean source)
parameters
Ω :
Type*
MeasurableSpace Ω
μ :
Measure Ω
f :
Ω → ℝ
def
entropy μ f :
ℝ
given by
(∫ ω, f ω * log (f ω) ∂μ) - (∫ ω, f ω ∂μ) * log (∫ ω, f ω ∂μ)
Causalean.Stat.Concentration.EntropyMethod.entropy · Causalean/Stat/Concentration/EntropyMethod/Basic.lean:32
def entropyDualValues reviewed
Causalean.Stat.Concentration.EntropyMethod

Given a probability measure μ and a positive function f, the variational values associated with f are the integrals E[f g] over integrable test functions whose exponential has expectation at most one.

Definition (Lean source)
parameters
Ω :
Type*
MeasurableSpace Ω
μ :
Measure Ω
f :
Ω → ℝ
def
entropyDualValues μ f :
Set ℝ
given by
{r | ∃ g : Ω → ℝ, Integrable (fun ω => f ω * g ω) μ ∧ Integrable (fun ω => exp (g ω)) μ ∧ (∫ ω, exp (g ω) ∂μ) ≤ 1 ∧ r = ∫ ω, f ω * g ω ∂μ}
Causalean.Stat.Concentration.EntropyMethod.entropyDualValues · Causalean/Stat/Concentration/EntropyMethod/Basic.lean:39
theorem entropy_isGreatest_dual reviewed
Causalean.Stat.Concentration.EntropyMethod

If the function f is integrable, f log f is integrable, f is positive almost everywhere, and its mean is positive, then its entropy is the greatest Gibbs variational value.

Formal statement
hypotheses
Ω :
Type*
MeasurableSpace Ω
Measure Ω
IsProbabilityMeasure μ
f :
Ω → ℝ
hf :
Integrable f μ
hflog :
Integrable (fun ω => f ω * log (f ω)) μ
hfpos :
∀ᵐ ω ∂μ, 0 < f ω
hm :
0 < ∫ ω, f ω ∂μ
conclusion
IsGreatest (entropyDualValues μ f) (entropy μ f)
Proof (Lean source)
theorem entropy_isGreatest_dual {Ω : Type*} [MeasurableSpace Ω] {μ : Measure Ω} [IsProbabilityMeasure μ] {f : Ω → ℝ} (hf : Integrable f μ) (hflog : Integrable (fun ω => f ω * log (f ω)) μ) (hfpos : ∀ᵐ ω ∂μ, 0 < f ω) (hm : 0 < ∫ ω, f ω ∂μ) : IsGreatest (entropyDualValues μ f) (entropy μ f) := by let m := ∫ ω, f ω ∂μ let g : Ω → ℝ := fun ω => log (f ω / m) have hlogdiv : Integrable (fun ω => f ω * g ω) μ := integrable_mul_log_div hf hflog hfpos hm have hexp_eq : (fun ω => exp (g ω)) =ᵐ[μ] fun ω => f ω / m := by filter_upwards [hfpos] with ω hω exact Real.exp_log (div_pos hω hm) have hexp : Integrable (fun ω => exp (g ω)) μ := by rw [integrable_congr hexp_eq] exact hf.div_const m have hexp_mean : (∫ ω, exp (g ω) ∂μ) = 1 := by rw [integral_congr_ae hexp_eq, integral_div, show (∫ ω, f ω ∂μ) = m by rfl] exact div_self hm.ne' have hvalue : (∫ ω, f ω * g ω ∂μ) = entropy μ f := (entropy_eq_integral_mul_log_div hf hflog hfpos hm).symm refine ⟨?_, ?_⟩ · exact ⟨g, hlogdiv, hexp, hexp_mean.le, hvalue.symm⟩ · intro r hr rcases hr with ⟨g', hfg', hexp', hconstraint', rfl⟩ exact integral_mul_le_entropy hf hflog hfpos hm hfg' hexp' hconstraint'
Causalean.Stat.Concentration.EntropyMethod.entropy_isGreatest_dual · Causalean/Stat/Concentration/EntropyMethod/Basic.lean:157 · uses entropy , entropyDualValues
2 supporting declarations (lemmas, instances)
  • entropy_eq_integral_mul_log_div theorem — If the function f is integrable, f log f is integrable, f is positive almost everywhere, and its mean is positive, then its entropy is the integral of f log (f / E f).
    hypotheses
    Ω :
    Type*
    MeasurableSpace Ω
    Measure Ω
    Ω → ℝ
    hf :
    Integrable f μ
    hflog :
    Integrable (fun ω => f ω * log (f ω)) μ
    hfpos :
    ∀ᵐ ω ∂μ, 0 < f ω
    hm :
    0 < ∫ ω, f ω ∂μ
    conclusion
    entropy μ f = ∫ ω, f ω * log (f ω / ∫ x, f x ∂μ) ∂μ
    Proof (Lean source)
    theorem entropy_eq_integral_mul_log_div {Ω : Type*} [MeasurableSpace Ω] {μ : Measure Ω} {f : Ω → ℝ} (hf : Integrable f μ) (hflog : Integrable (fun ω => f ω * log (f ω)) μ) (hfpos : ∀ᵐ ω ∂μ, 0 < f ω) (hm : 0 < ∫ ω, f ω ∂μ) : entropy μ f = ∫ ω, f ω * log (f ω / ∫ x, f x ∂μ) ∂μ := by rw [entropy] have hEq : (fun ω => f ω * log (f ω / ∫ x, f x ∂μ)) =ᵐ[μ] fun ω => f ω * log (f ω) - f ω * log (∫ x, f x ∂μ) := by filter_upwards [hfpos] with ω hω rw [Real.log_div hω.ne' hm.ne'] ring rw [integral_congr_ae hEq] rw [integral_sub hflog (hf.mul_const _), integral_mul_const]
    Causalean.Stat.Concentration.EntropyMethod.entropy_eq_integral_mul_log_div · Causalean/Stat/Concentration/EntropyMethod/Basic.lean:89
  • integral_mul_le_entropy theorem — Under integrability of f, integrability of f log f, positivity of f almost everywhere, and positivity of its mean, every test function for which f g is integrable, exp g is integrable, and E[exp g] ≤ 1 satisfies E[f g] ≤ Ent(f).
    hypotheses
    Ω :
    Type*
    MeasurableSpace Ω
    Measure Ω
    IsProbabilityMeasure μ
    f g :
    Ω → ℝ
    hf :
    Integrable f μ
    hflog :
    Integrable (fun ω => f ω * log (f ω)) μ
    hfpos :
    ∀ᵐ ω ∂μ, 0 < f ω
    hm :
    0 < ∫ ω, f ω ∂μ
    hfg :
    Integrable (fun ω => f ω * g ω) μ
    hexp :
    Integrable (fun ω => exp (g ω)) μ
    hconstraint :
    (∫ ω, exp (g ω) ∂μ) ≤ 1
    conclusion
    (∫ ω, f ω * g ω ∂μ) ≤ entropy μ f
    Proof (Lean source)
    theorem integral_mul_le_entropy {Ω : Type*} [MeasurableSpace Ω] {μ : Measure Ω} [IsProbabilityMeasure μ] {f g : Ω → ℝ} (hf : Integrable f μ) (hflog : Integrable (fun ω => f ω * log (f ω)) μ) (hfpos : ∀ᵐ ω ∂μ, 0 < f ω) (hm : 0 < ∫ ω, f ω ∂μ) (hfg : Integrable (fun ω => f ω * g ω) μ) (hexp : Integrable (fun ω => exp (g ω)) μ) (hconstraint : (∫ ω, exp (g ω) ∂μ) ≤ 1) : (∫ ω, f ω * g ω ∂μ) ≤ entropy μ f := by let m := ∫ ω, f ω ∂μ have hlogdiv : Integrable (fun ω => f ω * log (f ω / m)) μ := integrable_mul_log_div hf hflog hfpos hm have hright : Integrable (fun ω => f ω * log (f ω / m) - f ω + m * exp (g ω)) μ := (hlogdiv.sub hf).add (hexp.const_mul m) have hpoint : (fun ω => f ω * g ω) ≤ᵐ[μ] fun ω => f ω * log (f ω / m) - f ω + m * exp (g ω) := by filter_upwards [hfpos] with ω hω exact scaledYoung hω hm have hInt := integral_mono_ae hfg hright hpoint have hent : entropy μ f = ∫ ω, f ω * log (f ω / m) ∂μ := entropy_eq_integral_mul_log_div hf hflog hfpos hm have hright_eq : (∫ ω, f ω * log (f ω / m) - f ω + m * exp (g ω) ∂μ) = (∫ ω, f ω * log (f ω / m) ∂μ) - (∫ ω, f ω ∂μ) + m * (∫ ω, exp (g ω) ∂μ) := by calc _ = (∫ ω, f ω * log (f ω / m) - f ω ∂μ) + (∫ ω, m * exp (g ω) ∂μ) := integral_add (hlogdiv.sub hf) (hexp.const_mul m) _ = _ := by rw [integral_sub hlogdiv hf, integral_const_mul] rw [hright_eq] at hInt have hm_nonneg : 0 ≤ m := hm.le have hmul : m * (∫ ω, exp (g ω) ∂μ) ≤ m := by simpa using mul_le_mul_of_nonneg_left hconstraint hm_nonneg calc (∫ ω, f ω * g ω ∂μ) ≤ ∫ ω, f ω * log (f ω / m) ∂μ := by dsimp [m] at hInt hmul ⊢ nlinarith _ = entropy μ f := hent.symm
    Causalean.Stat.Concentration.EntropyMethod.integral_mul_le_entropy · Causalean/Stat/Concentration/EntropyMethod/Basic.lean:109
Finite­Tensorization 3 core · 0 supporting This file iterates binary entropy tensorization over a finite product of independent probability laws. ★ entropy_pi_le_coordinateEntropySum

Finite-coordinate entropy tensorization

This file iterates binary entropy tensorization over a finite product of independent probability laws. The coordinate entropy sum is written recursively along Mathlib's measurable equivalence between a Fin (n + 1)-indexed tuple and its head--tail product decomposition.

The regularity predicate contains the positivity, integrability, and Fubini conditions needed by the real-valued binary theorem, together with the integrability needed to average the inductive tail inequality.

def coordinateEntropySum reviewed
Causalean.Stat.Concentration.EntropyMethod

Given a sequence of coordinate laws μ, a number of coordinates n, and a function f on the first n coordinates, the finite sum of expected one-coordinate entropies is zero with no coordinates, while at a positive number of coordinates it averages the head-coordinate entropy over the tail and the recursively defined tail-coordinate sum over the head.

Definition (Lean source)
parameters
X :
Type u
MeasurableSpace X
μ :
ℕ → Measure X
n :
ℕ
def
coordinateEntropySum μ n :
((Fin n → X) → ℝ) → ℝ
given by
clause 1
| 0, _ => 0
clause 2
| n + 1, f
=> let e := piFinSuccAbove (fun _ : Fin (n + 1) => X) 0 (∫ tail, entropy (μ 0) (fun x => f (e.symm (x, tail))) ∂Measure.pi (fun j : Fin n => μ (j.val + 1)))
+ ∫ x, coordinateEntropySum (fun i => μ (i + 1)) n (fun tail => f (e.symm (x, tail))) ∂μ 0
Causalean.Stat.Concentration.EntropyMethod.coordinateEntropySum · Causalean/Stat/Concentration/EntropyMethod/FiniteTensorization.lean:32
def FiniteTensorizationRegularity reviewed
Causalean.Stat.Concentration.EntropyMethod

Given coordinate laws μ, a finite coordinate count n, and a function f on that product, the regularity conditions for finite entropy tensorization recursively require the binary positivity and integrability bundle, the same conditions in every tail section, and integrability of both sides of the inductive tail comparison: the zero-coordinate condition is automatic, and the positive-coordinate condition contains the binary bundle, recursive tail regularity, and the two required integrability clauses.

Definition (Lean source)
parameters
X :
Type u
MeasurableSpace X
μ :
ℕ → Measure X
n :
ℕ
def
FiniteTensorizationRegularity μ n :
((Fin n → X) → ℝ) → Prop
given by
clause 1
| 0, _ => True
clause 2
| n + 1, f
=> let e := piFinSuccAbove (fun _ : Fin (n + 1) => X) 0 EntropyTensorizationIntegrable (μ 0) (Measure.pi (fun j : Fin n => μ (j.val + 1))) (fun p => f (e.symm p)) ∧
(∀ x, FiniteTensorizationRegularity (fun i => μ (i + 1)) n (fun tail => f (e.symm (x, tail)))) ∧
Integrable (fun x => entropy (Measure.pi (fun j : Fin n => μ (j.val + 1))) (fun tail => f (e.symm (x, tail)))) (μ 0) ∧
Integrable (fun x => coordinateEntropySum (fun i => μ (i + 1)) n (fun tail => f (e.symm (x, tail)))) (μ 0)
Causalean.Stat.Concentration.EntropyMethod.FiniteTensorizationRegularity · Causalean/Stat/Concentration/EntropyMethod/FiniteTensorization.lean:48
theorem entropy_pi_le_coordinateEntropySum reviewed
Causalean.Stat.Concentration.EntropyMethod

If the coordinate laws are probability laws, for a number of coordinates and a real-valued function of the whole coordinate vector satisfying the recursive positivity and integrability conditions, then the entropy under the independent product law is at most the sum of the expected one-coordinate entropies.

Formal statement
hypotheses
X :
Type u
MeasurableSpace X
μ :
ℕ → Measure X
∀ i, IsProbabilityMeasure (μ i)
n :
ℕ
f :
(Fin n → X) → ℝ
h :
FiniteTensorizationRegularity μ n f
conclusion
entropy (Measure.pi (fun i : Fin n => μ i.val)) f ≤ coordinateEntropySum μ n f
Proof (Lean source)
theorem entropy_pi_le_coordinateEntropySum {X : Type u} [MeasurableSpace X] (μ : ℕ → Measure X) [hprob : ∀ i, IsProbabilityMeasure (μ i)] (n : ℕ) (f : (Fin n → X) → ℝ) (h : FiniteTensorizationRegularity μ n f) : entropy (Measure.pi (fun i : Fin n => μ i.val)) f ≤ coordinateEntropySum μ n f := by induction n generalizing μ with | zero => have hf : f = fun _ => f default := by funext x exact congrArg f (Subsingleton.elim x default) rw [hf, entropy] simp [coordinateEntropySum] | succ n ih => let e := piFinSuccAbove (fun _ : Fin (n + 1) => X) 0 let ν : Measure (Fin n → X) := Measure.pi (fun j : Fin n => μ (j.val + 1)) let g : X × (Fin n → X) → ℝ := fun p => f (e.symm p) have hsplit : MeasurePreserving e (Measure.pi (fun i : Fin (n + 1) => μ i.val)) ((μ 0).prod ν) := by simpa [e, ν] using (MeasureTheory.measurePreserving_piFinSuccAbove (μ := fun i : Fin (n + 1) => μ i.val) 0) have hent : entropy (Measure.pi (fun i : Fin (n + 1) => μ i.val)) f = entropy ((μ 0).prod ν) g := by have hc := entropy_comp_measurableEquiv e hsplit g have hcomp : g ∘ e = f := by funext x change f (e.symm (e x)) = f x rw [e.symm_apply_apply] simpa [hcomp] using hc change EntropyTensorizationIntegrable (μ 0) ν g ∧ (∀ x, FiniteTensorizationRegularity (fun i => μ (i + 1)) n (fun tail => f (e.symm (x, tail)))) ∧ Integrable (fun x => entropy ν (fun tail => f (e.symm (x, tail)))) (μ 0) ∧ Integrable (fun x => coordinateEntropySum (fun i => μ (i + 1)) n (fun tail => f (e.symm (x, tail)))) (μ 0) at h rcases h with ⟨hbin, htail, hentInt, hsumInt⟩ have hbinary := entropy_prod_le (μ 0) ν g hbin have htailPoint : (fun x => entropy ν (fun tail => f (e.symm (x, tail)))) ≤ᵐ[μ 0] fun x => coordinateEntropySum (fun i => μ (i + 1)) n (fun tail => f (e.symm (x, tail))) := by filter_upwards with x exact ih (fun i => μ (i + 1)) (fun tail => f (e.symm (x, tail))) (htail x) have htailIntegral := integral_mono_ae hentInt hsumInt htailPoint have hsum : (∫ y, entropy (μ 0) (fun x => g (x, y)) ∂ν) + (∫ x, entropy ν (fun y => g (x, y)) ∂μ 0) ≤ (∫ y, entropy (μ 0) (fun x => g (x, y)) ∂ν) + ∫ x, coordinateEntropySum (fun i => μ (i + 1)) n (fun tail => f (e.symm (x, tail))) ∂μ 0 := by exact add_le_add_right (by simpa [g] using htailIntegral) _ rw [hent] apply hbinary.trans simpa [coordinateEntropySum, e, ν, g] using hsum
Causalean.Stat.Concentration.EntropyMethod.entropy_pi_le_coordinateEntropySum · Causalean/Stat/Concentration/EntropyMethod/FiniteTensorization.lean:81 · uses FiniteTensorizationRegularity , coordinateEntropySum , entropy
Bousquet 4 core · 0 supporting This file proves the signed-increment estimates at the heart of Bousquet's variance-sensitive concentration inequality for empirical-process suprema: Boucheron--Lugosi--Massart (2013), Lemma 12.6, the conditional half-sq ★ blm_phi_signed_increment_le★ blm_conditional_half_square_sub_le★ blm_conditional_phi_cost_le

Analytic ingredients for Bousquet's inequality

This file proves the signed-increment estimates at the heart of Bousquet's variance-sensitive concentration inequality for empirical-process suprema: Boucheron--Lugosi--Massart (2013), Lemma 12.6, the conditional half-square consequence of Lemma 11.11, and the resulting one-coordinate tilted Bennett-cost estimate used in Lemma 12.8.

def blmPhi reviewed
Causalean.Stat.Concentration.EntropyMethod

For a real argument x, the Bennett entropy function is exp x - x - 1.

Definition (Lean source)
parameters
x :
ℝ
def
blmPhi x :
ℝ
given by
exp x - x - 1
Causalean.Stat.Concentration.EntropyMethod.blmPhi · Causalean/Stat/Concentration/EntropyMethod/Bousquet.lean:34
theorem blm_phi_signed_increment_le reviewed
Causalean.Stat.Concentration.EntropyMethod

BLM Lemma 12.6. If the quadratic coefficient beta is nonnegative, the tilt lam is nonnegative, and the signed increment x is at most one, then the Bennett entropy ratio at -lam*x is bounded by the signed affine- quadratic exponential ratio.

Formal statement
hypotheses
beta lam x :
ℝ
hbeta :
0 ≤ beta
hlam :
0 ≤ lam
hx :
x ≤ 1
conclusion
blmPhi (-lam * x) / blmPhi (-lam)
≤ (x + (beta * x ^ 2 - x) * exp (-lam * x)) / (1 + (beta - 1) * exp (-lam))
Proof (Lean source)
theorem blm_phi_signed_increment_le {beta lam x : ℝ} (hbeta : 0 ≤ beta) (hlam : 0 ≤ lam) (hx : x ≤ 1) : blmPhi (-lam * x) / blmPhi (-lam) ≤ (x + (beta * x ^ 2 - x) * exp (-lam * x)) / (1 + (beta - 1) * exp (-lam)) := by rcases eq_or_lt_of_le hlam with rfl | hlam · by_cases hbzero : beta = 0 · simp [blmPhi, hbzero] · simp only [blmPhi, zero_mul, neg_zero, Real.exp_zero, sub_zero, sub_self, zero_div, one_mul, add_zero] rw [div_nonneg_iff] exact inl ⟨by nlinarith [mul_nonneg hbeta (sq_nonneg x)], by nlinarith⟩ let f : ℝ → ℝ := fun z => lam * z * exp (lam * z) - exp (lam * z) + 1 let g : ℝ → ℝ := fun z => z * exp (lam * z) + beta * z ^ 2 - z let fp : ℝ → ℝ := fun z => lam ^ 2 * z * exp (lam * z) let gp : ℝ → ℝ := fun z => exp (lam * z) * (1 + lam * z) + 2 * beta * z - 1 let fpp : ℝ → ℝ := fun z => lam ^ 2 * exp (lam * z) * (1 + lam * z) let gpp : ℝ → ℝ := fun z => lam * exp (lam * z) * (2 + lam * z) + 2 * beta let L : ℝ := lam ^ 2 / (2 * (beta + lam)) let rho : ℝ → ℝ := update (fun z => f z / g z) 0 L have hf_deriv (z : ℝ) : HasDerivAt f (fp z) z := by dsimp [f, fp] apply ((((hasDerivAt_const z lam).mul (hasDerivAt_id z)).mul ((Real.hasDerivAt_exp (lam * z)).comp z ((hasDerivAt_const z lam).mul (hasDerivAt_id z)))).sub ((Real.hasDerivAt_exp (lam * z)).comp z ((hasDerivAt_const z lam).mul (hasDerivAt_id z))) |>.add_const 1).congr_deriv simp only [Function.comp_apply, Pi.mul_apply, Pi.add_apply, id_eq] ring have hg_deriv (z : ℝ) : HasDerivAt g (gp z) z := by dsimp [g, gp] apply ((((hasDerivAt_id z).mul ((Real.hasDerivAt_exp (lam * z)).comp z ((hasDerivAt_const z lam).mul (hasDerivAt_id z)))).add ((hasDerivAt_const z beta).mul ((hasDerivAt_id z).pow 2))).sub (hasDerivAt_id z)).congr_deriv simp only [Function.comp_apply, Pi.mul_apply, Pi.add_apply, id_eq] ring have hfp_deriv (z : ℝ) : HasDerivAt fp (fpp z) z := by dsimp [fp, fpp] apply (((hasDerivAt_const z (lam ^ 2)).mul (hasDerivAt_id z)).mul ((Real.hasDerivAt_exp (lam * z)).comp z ((hasDerivAt_const z lam).mul (hasDerivAt_id z)))).congr_deriv simp only [Function.comp_apply, Pi.mul_apply, Pi.add_apply, id_eq] ring have hgp_deriv (z : ℝ) : HasDerivAt gp (gpp z) z := by dsimp [gp, gpp] apply (((((Real.hasDerivAt_exp (lam * z)).comp z ((hasDerivAt_const z lam).mul (hasDerivAt_id z))).mul ((hasDerivAt_const z 1).add ((hasDerivAt_const z lam).mul (hasDerivAt_id z)))).add ((hasDerivAt_const z (2 * beta)).mul (hasDerivAt_id z))).sub_const 1).congr_deriv simp only [Function.comp_apply, Pi.mul_apply, Pi.add_apply, id_eq] ring have hgp_ne (z : ℝ) (hz : z ≠ 0) : gp z ≠ 0 := by have h := blm_g_deriv_mul_pos hlam hbeta hz intro hzero dsimp [gp] at hzero rw [hzero] at h simp at h have hf0 : f 0 = 0 := by simp [f] have hg0 : g 0 = 0 := by simp [g] have hfp0 : fp 0 = 0 := by simp [fp] have hgp0 : gp 0 = 0 := by simp [gp] have hden : 0 < 2 * (beta + lam) := by positivity have hsecondLimit : Tendsto (fun z => fpp z / gpp z) (𝓝 0) (𝓝 L) := by have hfpp : Tendsto fpp (𝓝 0) (𝓝 (lam ^ 2)) := by have h : ContinuousAt fpp 0 := by dsimp [fpp]; fun_prop simpa [fpp] using h.tendsto have hgpp : Tendsto gpp (𝓝 0) (𝓝 (2 * (beta + lam))) := by have h : ContinuousAt gpp 0 := by dsimp [gpp]; fun_prop convert h.tendsto using 1 <;> simp [gpp] <;> ring change Tendsto (fpp / gpp) (𝓝 0) (𝓝 L) simpa only [L] using hfpp.div hgpp hden.ne' have hgpp_ne_event : ∀ᶠ z in 𝓝[≠] 0, gpp z ≠ 0 := by have hcont : ContinuousAt gpp 0 := by dsimp [gpp]; fun_prop have hgpp0 : 0 < gpp 0 := by simp [gpp]; positivity have hev : ∀ᶠ z in 𝓝 0, 0 < gpp z := hcont.tendsto.eventually (Ioi_mem_nhds hgpp0) exact (hev.filter_mono inf_le_left).mono fun z hz => hz.ne' have hfirstLimit : Tendsto (fun z => fp z / gp z) (𝓝[≠] 0) (𝓝 L) := by apply HasDerivAt.lhopital_zero_nhdsNE (f' := fpp) (g' := gpp) · exact eventually_nhdsWithin_of_forall fun z _ => hfp_deriv z · exact eventually_nhdsWithin_of_forall fun z _ => hgp_deriv z · exact hgpp_ne_event · have h := (hfp_deriv 0).continuousAt.tendsto rw [hfp0] at h exact h.mono_left inf_le_left · have h := (hgp_deriv 0).continuousAt.tendsto rw [hgp0] at h exact h.mono_left inf_le_left · exact hsecondLimit.mono_left inf_le_left have hratioLimit : Tendsto (fun z => f z / g z) (𝓝[≠] 0) (𝓝 L) := by apply HasDerivAt.lhopital_zero_nhdsNE (f' := fp) (g' := gp) · exact eventually_nhdsWithin_of_forall fun z _ => hf_deriv z · exact eventually_nhdsWithin_of_forall fun z _ => hg_deriv z · filter_upwards [self_mem_nhdsWithin] with z hz exact hgp_ne z hz · have h := (hf_deriv 0).continuousAt.tendsto rw [hf0] at h exact h.mono_left inf_le_left · have h := (hg_deriv 0).continuousAt.tendsto rw [hg0] at h exact h.mono_left inf_le_left · exact hfirstLimit have hrho_cont : Continuous rho := by rw [continuous_iff_continuousAt] intro z by_cases hz : z = 0 · subst z change ContinuousAt (update (fun z => f z / g z) 0 L) 0 rw [continuousAt_update_same] exact hratioLimit · have hbase : ContinuousAt (fun w => f w / g w) z := (hf_deriv z).continuousAt.div (hg_deriv z).continuousAt (blm_g_pos hlam hbeta hz).ne' apply hbase.congr_of_eventuallyEq filter_upwards [eventually_ne_nhds hz] with w hw simp [rho, hw] have hrho_deriv (z : ℝ) (hz : z ≠ 0) : HasDerivAt rho ((fp z * g z - f z * gp z) / g z ^ 2) z := by have hbase : HasDerivAt (fun w => f w / g w) ((fp z * g z - f z * gp z) / g z ^ 2) z := (hf_deriv z).div (hg_deriv z) (blm_g_pos hlam hbeta hz).ne' have heq : rho =ᶠ[𝓝 z] fun w => f w / g w := by filter_upwards [eventually_ne_nhds hz] with w hw simp [rho, hw] exact hbase.congr_of_eventuallyEq heq have hrho_deriv_nonneg (z : ℝ) (hz : z ≠ 0) : 0 ≤ deriv rho z := by rw [(hrho_deriv z hz).deriv] exact div_nonneg (by dsimp [fp, g, f, gp] exact ratio_deriv_numerator_nonneg hlam.le hbeta) (sq_nonneg _) have hmonoNeg : MonotoneOn rho (Iic 0) := by apply monotoneOn_of_deriv_nonneg (convex_Iic 0) hrho_cont.continuousOn · intro z hz exact (hrho_deriv z (ne_of_lt (by simpa using hz))).differentiableAt.differentiableWithinAt · intro z hz exact hrho_deriv_nonneg z (ne_of_lt (by simpa using hz)) have hmonoPos : MonotoneOn rho (Icc 0 1) := by apply monotoneOn_of_deriv_nonneg (convex_Icc 0 1) hrho_cont.continuousOn · intro z hz rw [interior_Icc] at hz exact (hrho_deriv z (ne_of_gt hz.1)).differentiableAt.differentiableWithinAt · intro z hz rw [interior_Icc] at hz exact hrho_deriv_nonneg z (ne_of_gt hz.1) have hrhole : rho x ≤ rho 1 := by rcases le_total x 0 with hx0 | h0x · exact (hmonoNeg (by exact hx0) (by simp) hx0).trans (hmonoPos (by simp) (by simp) (by norm_num)) · exact hmonoPos ⟨h0x, hx⟩ (by simp) hx have hrewrite (z : ℝ) (hz : z ≠ 0) : rho z = blmPhi (-lam * z) / (z + (beta * z ^ 2 - z) * exp (-lam * z)) := by simp only [rho] rw [Function.update_of_ne hz] dsimp [f, g, blmPhi] have hepos := Real.exp_pos (lam * z) have hscaled : z + (beta * z ^ 2 - z) * exp (-lam * z) = (z * exp (lam * z) + beta * z ^ 2 - z) * exp (-lam * z) := by rw [show -lam * z = -(lam * z) by ring, Real.exp_neg] field_simp [Real.exp_ne_zero] ring have hdenScaled : z + (beta * z ^ 2 - z) * exp (-lam * z) ≠ 0 := by rw [hscaled] exact mul_ne_zero (blm_g_pos hlam hbeta hz).ne' (Real.exp_ne_zero _) apply (div_eq_div_iff (blm_g_pos hlam hbeta hz).ne' hdenScaled).2 rw [hscaled] rw [show -lam * z = -(lam * z) by ring, Real.exp_neg] field_simp [Real.exp_ne_zero] ring by_cases hxzero : x = 0 · subst x simp [blmPhi] have hone : (1 : ℝ) ≠ 0 := one_ne_zero rw [hrewrite x hxzero, hrewrite 1 hone] at hrhole have hPhi : 0 < blmPhi (-lam) := by have h := Real.add_one_lt_exp (neg_ne_zero.mpr hlam.ne') dsimp [blmPhi] linarith have hD : 0 < 1 + (beta - 1) * exp (-lam) := by have he : exp (-lam) < 1 := Real.exp_lt_one_iff.mpr (neg_neg_of_pos hlam) have hbexp : 0 ≤ beta * exp (-lam) := mul_nonneg hbeta (Real.exp_pos _).le nlinarith have hC : 0 < x + (beta * x ^ 2 - x) * exp (-(lam * x)) := by have hgpos := blm_g_pos hlam hbeta hxzero have hepos := Real.exp_pos (-(lam * x)) have hid : x + (beta * x ^ 2 - x) * exp (-(lam * x)) = g x * exp (-(lam * x)) := by dsimp [g] rw [Real.exp_neg] field_simp [Real.exp_ne_zero] ring rw [hid] positivity apply (div_le_div_iff₀ hPhi hD).2 norm_num at hrhole have hcross := (div_le_div_iff₀ hC hD).mp hrhole convert hcross using 1 <;> ring
Causalean.Stat.Concentration.EntropyMethod.blm_phi_signed_increment_le · Causalean/Stat/Concentration/EntropyMethod/Bousquet.lean:143 · uses blmPhi
theorem blm_conditional_half_square_sub_le reviewed
Causalean.Stat.Concentration.EntropyMethod

Conditional estimate from BLM Lemma 11.11. For integrable increments Delta with integrable squares, and integrable lower comparators Y with integrable squares, if Y lies below Delta, Delta is at most one, Y is at most one, and Y has nonnegative conditional mean, then the conditional mean of Delta^2/2-Delta is at most half the conditional second moment of Y.

Formal statement
hypotheses
Omega :
Type*
MeasurableSpace Omega
Measure Omega
Omega → ℝ
hDelta :
Integrable Delta mu
hDeltaSq :
Integrable (fun omega => Delta omega ^ 2) mu
hY :
Integrable Y mu
hYSq :
Integrable (fun omega => Y omega ^ 2) mu
hLower :
∀ᵐ omega ∂mu, Y omega ≤ Delta omega
hDeltaUpper :
∀ᵐ omega ∂mu, Delta omega ≤ 1
hYUpper :
∀ᵐ omega ∂mu, Y omega ≤ 1
hYMean :
0 ≤ ∫ omega, Y omega ∂mu
conclusion
(∫ omega, Delta omega ^ 2 / 2 - Delta omega ∂mu) ≤ (∫ omega, Y omega ^ 2 ∂mu) / 2
Proof (Lean source)
theorem blm_conditional_half_square_sub_le {Omega : Type*} [MeasurableSpace Omega] {mu : Measure Omega} {Delta Y : Omega → ℝ} (hDelta : Integrable Delta mu) (hDeltaSq : Integrable (fun omega => Delta omega ^ 2) mu) (hY : Integrable Y mu) (hYSq : Integrable (fun omega => Y omega ^ 2) mu) (hLower : ∀ᵐ omega ∂mu, Y omega ≤ Delta omega) (hDeltaUpper : ∀ᵐ omega ∂mu, Delta omega ≤ 1) (hYUpper : ∀ᵐ omega ∂mu, Y omega ≤ 1) (hYMean : 0 ≤ ∫ omega, Y omega ∂mu) : (∫ omega, Delta omega ^ 2 / 2 - Delta omega ∂mu) ≤ (∫ omega, Y omega ^ 2 ∂mu) / 2 := by have hLeftInt : Integrable (fun omega => Delta omega ^ 2 / 2 - Delta omega) mu := (hDeltaSq.div_const 2).sub hDelta have hRightInt : Integrable (fun omega => Y omega ^ 2 / 2 - Y omega) mu := (hYSq.div_const 2).sub hY have hpoint : (fun omega => Delta omega ^ 2 / 2 - Delta omega) ≤ᵐ[mu] fun omega => Y omega ^ 2 / 2 - Y omega := by filter_upwards [hLower, hDeltaUpper, hYUpper] with omega hl hd hy have hnonneg : 0 ≤ Delta omega - Y omega := sub_nonneg.mpr hl have hnonpos : Delta omega + Y omega - 2 ≤ 0 := by linarith nlinarith [mul_nonpos_of_nonneg_of_nonpos hnonneg hnonpos] have hint := MeasureTheory.integral_mono_ae hLeftInt hRightInt hpoint have hright : (∫ omega, Y omega ^ 2 / 2 - Y omega ∂mu) = (∫ omega, Y omega ^ 2 ∂mu) / 2 - ∫ omega, Y omega ∂mu := by rw [MeasureTheory.integral_sub (hYSq.div_const 2) hY, MeasureTheory.integral_div] rw [hright] at hint linarith
Causalean.Stat.Concentration.EntropyMethod.blm_conditional_half_square_sub_le · Causalean/Stat/Concentration/EntropyMethod/Bousquet.lean:353
theorem blm_conditional_phi_cost_le reviewed
Causalean.Stat.Concentration.EntropyMethod

Conditional slice estimate in the proof of BLM Lemma 12.8. Fix a nonnegative tilt lam, a deletion value zi, and a nonnegative coordinate variance proxy sigma2. For an integrable deletion increment Delta with integrable square, an integrable leave-one-out maximizing coordinate Y with integrable square, integrability of the exponential tilt and its product with the increment, and integrability of the tilted Bennett cost, suppose Y lies below Delta, both variables are at most one, Y has nonnegative mean, Delta has nonnegative mean, and Y has second moment at most sigma2. Then the conditional tilted Bennett cost is at most the BLM factor times the tilted expectation of Delta + sigma2/2.

Formal statement
hypotheses
Omega :
Type*
MeasurableSpace Omega
Measure Omega
IsProbabilityMeasure mu
lam zi sigma2 :
ℝ
hlam :
0 ≤ lam
hsigma :
0 ≤ sigma2
Delta Y :
Omega → ℝ
hDelta :
Integrable Delta mu
hDeltaSq :
Integrable (fun omega => Delta omega ^ 2) mu
hY :
Integrable Y mu
hYSq :
Integrable (fun omega => Y omega ^ 2) mu
hExp :
Integrable (fun omega => exp (lam * (zi + Delta omega))) mu
hExpDelta :
Integrable (fun omega => exp (lam * (zi + Delta omega)) * Delta omega) mu
hPhi :
Integrable (fun omega => exp (lam * (zi + Delta omega)) * blmPhi (-lam * Delta omega)) mu
hLower :
∀ᵐ omega ∂mu, Y omega ≤ Delta omega
hDeltaUpper :
∀ᵐ omega ∂mu, Delta omega ≤ 1
hYUpper :
∀ᵐ omega ∂mu, Y omega ≤ 1
hYMean :
0 ≤ ∫ omega, Y omega ∂mu
hDeltaMean :
0 ≤ ∫ omega, Delta omega ∂mu
hYSecond :
(∫ omega, Y omega ^ 2 ∂mu) ≤ sigma2
conclusion
(∫ omega, exp (lam * (zi + Delta omega)) * blmPhi (-lam * Delta omega) ∂mu)
≤ (blmPhi (-lam) / (1 - exp (-lam) / 2)) * ∫ omega, exp (lam * (zi + Delta omega)) * (Delta omega + sigma2 / 2) ∂mu
Proof (Lean source)
theorem blm_conditional_phi_cost_le {Omega : Type*} [MeasurableSpace Omega] {mu : Measure Omega} [IsProbabilityMeasure mu] {lam zi sigma2 : ℝ} (hlam : 0 ≤ lam) (hsigma : 0 ≤ sigma2) {Delta Y : Omega → ℝ} (hDelta : Integrable Delta mu) (hDeltaSq : Integrable (fun omega => Delta omega ^ 2) mu) (hY : Integrable Y mu) (hYSq : Integrable (fun omega => Y omega ^ 2) mu) (hExp : Integrable (fun omega => exp (lam * (zi + Delta omega))) mu) (hExpDelta : Integrable (fun omega => exp (lam * (zi + Delta omega)) * Delta omega) mu) (hPhi : Integrable (fun omega => exp (lam * (zi + Delta omega)) * blmPhi (-lam * Delta omega)) mu) (hLower : ∀ᵐ omega ∂mu, Y omega ≤ Delta omega) (hDeltaUpper : ∀ᵐ omega ∂mu, Delta omega ≤ 1) (hYUpper : ∀ᵐ omega ∂mu, Y omega ≤ 1) (hYMean : 0 ≤ ∫ omega, Y omega ∂mu) (hDeltaMean : 0 ≤ ∫ omega, Delta omega ∂mu) (hYSecond : (∫ omega, Y omega ^ 2 ∂mu) ≤ sigma2) : (∫ omega, exp (lam * (zi + Delta omega)) * blmPhi (-lam * Delta omega) ∂mu) ≤ (blmPhi (-lam) / (1 - exp (-lam) / 2)) * ∫ omega, exp (lam * (zi + Delta omega)) * (Delta omega + sigma2 / 2) ∂mu := by rcases eq_or_lt_of_le hlam with rfl | hlam · simp [blmPhi] let den := 1 - exp (-lam) / 2 let theta := blmPhi (-lam) / den let q : Omega → ℝ := fun omega => Delta omega ^ 2 / 2 - Delta omega have hden : 0 < den := by have he : exp (-lam) < 1 := Real.exp_lt_one_iff.mpr (neg_neg_of_pos hlam) dsimp [den] linarith have hPhiLam : 0 < blmPhi (-lam) := by have h := Real.add_one_lt_exp (neg_ne_zero.mpr hlam.ne') dsimp [blmPhi] linarith have htheta : 0 ≤ theta := (div_pos hPhiLam hden).le have hq : Integrable q mu := hDeltaSq.div_const 2 |>.sub hDelta have hHalf := blm_conditional_half_square_sub_le hDelta hDeltaSq hY hYSq hLower hDeltaUpper hYUpper hYMean change (∫ omega, q omega ∂mu) ≤ (∫ omega, Y omega ^ 2 ∂mu) / 2 at hHalf have hqBound : (∫ omega, q omega ∂mu) ≤ sigma2 / 2 := by linarith have hExpOnly : Integrable (fun omega => exp (lam * Delta omega)) mu := by have h := hExp.const_mul (exp (-lam * zi)) convert h using 1 funext omega rw [← Real.exp_add] congr 1 ring have hExpMean : 1 ≤ ∫ omega, exp (lam * Delta omega) ∂mu := by have hLinear : Integrable (fun omega => 1 + lam * Delta omega) mu := MeasureTheory.integrable_const 1 |>.add (hDelta.const_mul lam) have hMono := MeasureTheory.integral_mono hLinear hExpOnly (fun omega => by simpa [add_comm] using Real.add_one_le_exp (lam * Delta omega)) have hLinearIntegral : (∫ omega, 1 + lam * Delta omega ∂mu) = 1 + lam * ∫ omega, Delta omega ∂mu := by integral_linearity simp rw [hLinearIntegral] at hMono nlinarith [mul_nonneg hlam.le hDeltaMean] have hExpFactor : (∫ omega, exp (lam * (zi + Delta omega)) ∂mu) = exp (lam * zi) * ∫ omega, exp (lam * Delta omega) ∂mu := by rw [← MeasureTheory.integral_const_mul] apply MeasureTheory.integral_congr_ae filter_upwards with omega rw [← Real.exp_add] congr 1 ring have hZiExp : exp (lam * zi) ≤ ∫ omega, exp (lam * (zi + Delta omega)) ∂mu := by rw [hExpFactor] simpa using mul_le_mul_of_nonneg_left hExpMean (Real.exp_pos (lam * zi)).le have hPoint : (fun omega => exp (lam * (zi + Delta omega)) * blmPhi (-lam * Delta omega)) ≤ᵐ[mu] fun omega => theta * (exp (lam * (zi + Delta omega)) * Delta omega + exp (lam * zi) * q omega) := by filter_upwards [hDeltaUpper] with omega hUpper have hRatio := blm_phi_signed_increment_le (beta := (1 / 2 : ℝ)) (lam := lam) (x := Delta omega) (by norm_num) hlam.le hUpper have hBase : blmPhi (-lam * Delta omega) ≤ theta * (Delta omega + q omega * exp (-lam * Delta omega)) := by have hRaw := (div_le_iff₀ hPhiLam).mp hRatio calc blmPhi (-lam * Delta omega) ≤ ((Delta omega + ((1 / 2 : ℝ) * Delta omega ^ 2 - Delta omega) * exp (-lam * Delta omega)) / (1 + ((1 / 2 : ℝ) - 1) * exp (-lam))) * blmPhi (-lam) := hRaw _ = theta * (Delta omega + q omega * exp (-lam * Delta omega)) := by dsimp [theta, den, q] field_simp [hden.ne'] ring have hMul := mul_le_mul_of_nonneg_left hBase (Real.exp_pos (lam * (zi + Delta omega))).le calc exp (lam * (zi + Delta omega)) * blmPhi (-lam * Delta omega) ≤ exp (lam * (zi + Delta omega)) * (theta * (Delta omega + q omega * exp (-lam * Delta omega))) := hMul _ = theta * (exp (lam * (zi + Delta omega)) * Delta omega + exp (lam * zi) * q omega) := by have hcancel : exp (lam * (zi + Delta omega)) * exp (-lam * Delta omega) = exp (lam * zi) := by rw [← Real.exp_add] congr 1 ring calc exp (lam * (zi + Delta omega)) * (theta * (Delta omega + q omega * exp (-lam * Delta omega))) = theta * (exp (lam * (zi + Delta omega)) * Delta omega + (exp (lam * (zi + Delta omega)) * exp (-lam * Delta omega)) * q omega) := by ring _ = _ := by rw [hcancel] have hMidInt : Integrable (fun omega => theta * (exp (lam * (zi + Delta omega)) * Delta omega + exp (lam * zi) * q omega)) mu := (hExpDelta.add (hq.const_mul (exp (lam * zi)))).const_mul theta have hIntegrated := MeasureTheory.integral_mono_ae hPhi hMidInt hPoint have hMidIntegral : (∫ omega, theta * (exp (lam * (zi + Delta omega)) * Delta omega + exp (lam * zi) * q omega) ∂mu) = theta * ((∫ omega, exp (lam * (zi + Delta omega)) * Delta omega ∂mu) + exp (lam * zi) * ∫ omega, q omega ∂mu) := by integral_linearity rw [hMidIntegral] at hIntegrated have hQTerm : exp (lam * zi) * (∫ omega, q omega ∂mu) ≤ sigma2 / 2 * ∫ omega, exp (lam * (zi + Delta omega)) ∂mu := by calc exp (lam * zi) * (∫ omega, q omega ∂mu) ≤ exp (lam * zi) * (sigma2 / 2) := mul_le_mul_of_nonneg_left hqBound (Real.exp_pos _).le _ ≤ sigma2 / 2 * ∫ omega, exp (lam * (zi + Delta omega)) ∂mu := by rw [mul_comm (exp (lam * zi))] exact mul_le_mul_of_nonneg_left hZiExp (div_nonneg hsigma (by norm_num)) have hRightIntegral : (∫ omega, exp (lam * (zi + Delta omega)) * (Delta omega + sigma2 / 2) ∂mu) = (∫ omega, exp (lam * (zi + Delta omega)) * Delta omega ∂mu) + sigma2 / 2 * ∫ omega, exp (lam * (zi + Delta omega)) ∂mu := by calc _ = ∫ omega, exp (lam * (zi + Delta omega)) * Delta omega + sigma2 / 2 * exp (lam * (zi + Delta omega)) ∂mu := by apply MeasureTheory.integral_congr_ae filter_upwards with omega ring _ = _ := by rw [MeasureTheory.integral_add hExpDelta (hExp.const_mul (sigma2 / 2)), MeasureTheory.integral_const_mul] change _ ≤ theta * _ rw [hRightIntegral] apply hIntegrated.trans apply mul_le_mul_of_nonneg_left _ htheta nlinarith [hQTerm]
Causalean.Stat.Concentration.EntropyMethod.blm_conditional_phi_cost_le · Causalean/Stat/Concentration/EntropyMethod/Bousquet.lean:393 · uses blmPhi
Deletion­Log­Sobolev 4 core · 2 supporting This file derives the deletion-coordinate form of the modified logarithmic-Sobolev inequality directly from finite entropy tensorization. ★ deletionModifiedLogSobolev_pi

Deletion-coordinate modified logarithmic-Sobolev inequality

This file derives the deletion-coordinate form of the modified logarithmic-Sobolev inequality directly from finite entropy tensorization. A recursive family records one comparison value for each coordinate while making its independence of the deleted coordinate true by construction. The resulting bound is the entropy input used in Bousquet's inequality.

inductive DeletionCoordinateFamily reviewed
Causalean.Stat.Concentration.EntropyMethod

For a sample type X and a coordinate count n (the family's index), a recursive family of deletion-coordinate comparison values is either empty at zero coordinates or a head comparison depending only on the tail together with recursive tail comparisons after fixing the head.

Definition (Lean source)
parameters
X :
Type u
inductive
DeletionCoordinateFamily X :
(n : ℕ) → Type u
constructors
nil :
DeletionCoordinateFamily X 0
cons :
{n : ℕ} (head : (Fin n → X) → ℝ) (tail : X → DeletionCoordinateFamily X n) : DeletionCoordinateFamily X (n + 1)
Causalean.Stat.Concentration.EntropyMethod.DeletionCoordinateFamily · Causalean/Stat/Concentration/EntropyMethod/DeletionLogSobolev.lean:80
def exponentialDeletionPhiSum reviewed
Causalean.Stat.Concentration.EntropyMethod

Given coordinate laws mu, a coordinate count n, a tilt lam, a statistic Z, and deletion-coordinate comparisons D, the sum of expected tilted Bennett deletion costs is zero with no coordinates, while at a positive coordinate count it adds the head-coordinate cost and the recursively averaged tail-coordinate costs.

Definition (Lean source)
parameters
X :
Type u
MeasurableSpace X
mu :
ℕ → Measure X
n :
ℕ
def
exponentialDeletionPhiSum mu n :
ℝ → ((Fin n → X) → ℝ) → DeletionCoordinateFamily X n → ℝ
given by
clause 1
| 0, _, _, .nil => 0
clause 2
| n + 1, lam, Z, .cons head tail
=> let e := piFinSuccAbove (fun _ : Fin (n + 1) => X) 0 let nu := Measure.pi (fun j : Fin n => mu (j.val + 1)) (∫ rest, ∫ x, exp (lam * Z (e.symm (x, rest))) * blmPhi (-lam * (Z (e.symm (x, rest)) - head rest)) ∂mu 0 ∂nu)
+ ∫ x, exponentialDeletionPhiSum (fun i => mu (i + 1)) n lam (fun rest => Z (e.symm (x, rest))) (tail x) ∂mu 0
Causalean.Stat.Concentration.EntropyMethod.exponentialDeletionPhiSum · Causalean/Stat/Concentration/EntropyMethod/DeletionLogSobolev.lean:89 · uses DeletionCoordinateFamily
def DeletionLogSobolevRegularity reviewed
Causalean.Stat.Concentration.EntropyMethod

Given coordinate laws mu, a coordinate count n, a tilt lam, a statistic Z, and deletion-coordinate comparisons D, the regularity conditions for deletion-coordinate tensorization are automatic with no coordinates, while at a positive coordinate count they require exponential slice integrability, recursive tail regularity, and the four Fubini integrability conditions used to average the head and tail comparisons.

Definition (Lean source)
parameters
X :
Type u
MeasurableSpace X
mu :
ℕ → Measure X
n :
ℕ
def
DeletionLogSobolevRegularity mu n :
ℝ → ((Fin n → X) → ℝ) → DeletionCoordinateFamily X n → Prop
given by
clause 1
| 0, _, _, .nil => True
clause 2
| n + 1, lam, Z, .cons head tail
=> let e := piFinSuccAbove (fun _ : Fin (n + 1) => X) 0 let nu := Measure.pi (fun j : Fin n => mu (j.val + 1)) (∀ rest, Integrable (fun x => exp (lam * Z (e.symm (x, rest)))) (mu 0) ∧ Integrable (fun x => exp (lam * Z (e.symm (x, rest))) * (lam * Z (e.symm (x, rest)))) (mu 0)) ∧
(∀ x, DeletionLogSobolevRegularity (fun i => mu (i + 1)) n lam (fun rest => Z (e.symm (x, rest))) (tail x)) ∧
Integrable (fun rest => entropy (mu 0) (fun x => exp (lam * Z (e.symm (x, rest))))) nu ∧
Integrable (fun rest => ∫ x, exp (lam * Z (e.symm (x, rest))) * blmPhi (-lam * (Z (e.symm (x, rest)) - head rest)) ∂mu 0) nu ∧
Integrable (fun x => coordinateEntropySum (fun i => mu (i + 1)) n (fun rest => exp (lam * Z (e.symm (x, rest))))) (mu 0) ∧
Integrable (fun x => exponentialDeletionPhiSum (fun i => mu (i + 1)) n lam (fun rest => Z (e.symm (x, rest))) (tail x)) (mu 0)
Causalean.Stat.Concentration.EntropyMethod.DeletionLogSobolevRegularity · Causalean/Stat/Concentration/EntropyMethod/DeletionLogSobolev.lean:108 · uses DeletionCoordinateFamily
theorem deletionModifiedLogSobolev_pi reviewed
Causalean.Stat.Concentration.EntropyMethod

If the coordinate laws mu are probability laws, the product has n coordinates, the tilt is lam, the statistic is Z, the deletion-coordinate comparisons are D, finite entropy tensorization applies to the exponential tilt, and the deletion-coordinate slice regularity holds, then the entropy of the exponential tilt is at most the sum of expected costs exp(lam*Z) * phi(-lam*(Z-Z_i)).

Formal statement
hypotheses
X :
Type u
MeasurableSpace X
mu :
ℕ → Measure X
∀ i, IsProbabilityMeasure (mu i)
n :
ℕ
lam :
ℝ
Z :
(Fin n → X) → ℝ
D :
DeletionCoordinateFamily X n
hTensor :
FiniteTensorizationRegularity mu n (fun s => exp (lam * Z s))
hDeletion :
DeletionLogSobolevRegularity mu n lam Z D
conclusion
entropy (Measure.pi (fun i : Fin n => mu i.val)) (fun s => exp (lam * Z s))
≤ exponentialDeletionPhiSum mu n lam Z D
Proof (Lean source)
theorem deletionModifiedLogSobolev_pi {X : Type u} [MeasurableSpace X] (mu : ℕ → Measure X) [hprob : ∀ i, IsProbabilityMeasure (mu i)] (n : ℕ) (lam : ℝ) (Z : (Fin n → X) → ℝ) (D : DeletionCoordinateFamily X n) (hTensor : FiniteTensorizationRegularity mu n (fun s => exp (lam * Z s))) (hDeletion : DeletionLogSobolevRegularity mu n lam Z D) : entropy (Measure.pi (fun i : Fin n => mu i.val)) (fun s => exp (lam * Z s)) ≤ exponentialDeletionPhiSum mu n lam Z D := (entropy_pi_le_coordinateEntropySum mu n _ hTensor).trans (coordinateEntropySum_exp_le_deletion mu n lam Z D hDeletion)
Causalean.Stat.Concentration.EntropyMethod.deletionModifiedLogSobolev_pi · Causalean/Stat/Concentration/EntropyMethod/DeletionLogSobolev.lean:210 · uses DeletionCoordinateFamily , DeletionLogSobolevRegularity , FiniteTensorizationRegularity , entropy , exponentialDeletionPhiSum
2 supporting declarations (lemmas, instances)
  • entropy_exp_le_phi_comparison theorem — Given a probability law mu, a real function g, a scalar comparison value c, integrability of its exponential, and integrability of its exponentially weighted value, the entropy of exp(g) is at most the expected Bennett entropy cost exp(g) * phi(c-g).
    hypotheses
    X :
    Type*
    MeasurableSpace X
    mu :
    Measure X
    IsProbabilityMeasure mu
    g :
    X → ℝ
    c :
    ℝ
    hExp :
    Integrable (fun x => exp (g x)) mu
    hExpG :
    Integrable (fun x => exp (g x) * g x) mu
    conclusion
    entropy mu (fun x => exp (g x)) ≤ ∫ x, exp (g x) * blmPhi (c - g x) ∂mu
    Proof (Lean source)
    theorem entropy_exp_le_phi_comparison {X : Type*} [MeasurableSpace X] (mu : Measure X) [IsProbabilityMeasure mu] (g : X → ℝ) (c : ℝ) (hExp : Integrable (fun x => exp (g x)) mu) (hExpG : Integrable (fun x => exp (g x) * g x) mu) : entropy mu (fun x => exp (g x)) ≤ ∫ x, exp (g x) * blmPhi (c - g x) ∂mu := by let m := ∫ x, exp (g x) ∂mu have hm : 0 < m := integral_exp_pos hExp have hmean : c * m + m - exp c ≤ m * log m := by have hlog := Real.log_le_sub_one_of_pos (div_pos (Real.exp_pos c) hm) rw [Real.log_div (Real.exp_ne_zero c) hm.ne', Real.log_exp] at hlog have hmul := mul_le_mul_of_nonneg_left hlog hm.le have hratio : m * (exp c / m) = exp c := by field_simp [hm.ne'] nlinarith [hmul, hratio] have hEq : (fun x => exp (g x) * blmPhi (c - g x)) = fun x => exp (g x) * g x - c * exp (g x) - exp (g x) + exp c := by funext x simp only [blmPhi] rw [show c - g x = c + -g x by ring, Real.exp_add, Real.exp_neg] field_simp [Real.exp_ne_zero] ring have hLeftLog : (∫ x, exp (g x) * log (exp (g x)) ∂mu) = ∫ x, exp (g x) * g x ∂mu := by apply integral_congr_ae filter_upwards with x rw [Real.log_exp] have hExpConst : Integrable (fun _ : X => exp c) mu := integrable_const _ have hRightInt : Integrable (fun x => exp (g x) * g x - c * exp (g x) - exp (g x)) mu := ((hExpG.sub (hExp.const_mul c)).sub hExp) have hRight : (∫ x, exp (g x) * g x - c * exp (g x) - exp (g x) + exp c ∂mu) = (∫ x, exp (g x) * g x ∂mu) - c * (∫ x, exp (g x) ∂mu) - (∫ x, exp (g x) ∂mu) + exp c := by integral_linearity simp rw [entropy, hLeftLog, hEq, hRight] dsimp [m] at hmean linarith
    Causalean.Stat.Concentration.EntropyMethod.entropy_exp_le_phi_comparison · Causalean/Stat/Concentration/EntropyMethod/DeletionLogSobolev.lean:29
  • coordinateEntropySum_exp_le_deletion theorem — If the coordinate laws mu are probability laws, the product has n coordinates, the tilt is lam, the statistic is Z, the deletion-coordinate comparisons are D, and the recursive slice and Fubini regularity conditions hold, then the finite sum of one-coordinate entropies is at most the sum of expected tilted Bennett deletion costs.
    hypotheses
    X :
    Type u
    MeasurableSpace X
    mu :
    ℕ → Measure X
    ∀ i, IsProbabilityMeasure (mu i)
    n :
    ℕ
    lam :
    ℝ
    Z :
    (Fin n → X) → ℝ
    D :
    DeletionCoordinateFamily X n
    h :
    DeletionLogSobolevRegularity mu n lam Z D
    conclusion
    coordinateEntropySum mu n (fun s => exp (lam * Z s))
    ≤ exponentialDeletionPhiSum mu n lam Z D
    Proof (Lean source)
    theorem coordinateEntropySum_exp_le_deletion {X : Type u} [MeasurableSpace X] (mu : ℕ → Measure X) [hprob : ∀ i, IsProbabilityMeasure (mu i)] (n : ℕ) (lam : ℝ) (Z : (Fin n → X) → ℝ) (D : DeletionCoordinateFamily X n) (h : DeletionLogSobolevRegularity mu n lam Z D) : coordinateEntropySum mu n (fun s => exp (lam * Z s)) ≤ exponentialDeletionPhiSum mu n lam Z D := by induction n generalizing mu with | zero => cases D simp [coordinateEntropySum, exponentialDeletionPhiSum] | succ n ih => cases D with | cons head tail => let e := piFinSuccAbove (fun _ : Fin (n + 1) => X) 0 let nu : Measure (Fin n → X) := Measure.pi (fun j : Fin n => mu (j.val + 1)) change (∀ rest, Integrable (fun x => exp (lam * Z (e.symm (x, rest)))) (mu 0) ∧ Integrable (fun x => exp (lam * Z (e.symm (x, rest))) * (lam * Z (e.symm (x, rest)))) (mu 0)) ∧ (∀ x, DeletionLogSobolevRegularity (fun i => mu (i + 1)) n lam (fun rest => Z (e.symm (x, rest))) (tail x)) ∧ Integrable (fun rest => entropy (mu 0) (fun x => exp (lam * Z (e.symm (x, rest))))) nu ∧ Integrable (fun rest => ∫ x, exp (lam * Z (e.symm (x, rest))) * blmPhi (-lam * (Z (e.symm (x, rest)) - head rest)) ∂mu 0) nu ∧ Integrable (fun x => coordinateEntropySum (fun i => mu (i + 1)) n (fun rest => exp (lam * Z (e.symm (x, rest))))) (mu 0) ∧ Integrable (fun x => exponentialDeletionPhiSum (fun i => mu (i + 1)) n lam (fun rest => Z (e.symm (x, rest))) (tail x)) (mu 0) at h rcases h with ⟨hHead, hTail, hHeadEntInt, hHeadBoundInt, hTailEntInt, hTailBoundInt⟩ let headEnt : (Fin n → X) → ℝ := fun rest => entropy (mu 0) (fun x => exp (lam * Z (e.symm (x, rest)))) let headBound : (Fin n → X) → ℝ := fun rest => ∫ x, exp (lam * Z (e.symm (x, rest))) * blmPhi (-lam * (Z (e.symm (x, rest)) - head rest)) ∂mu 0 let tailEnt : X → ℝ := fun x => coordinateEntropySum (fun i => mu (i + 1)) n (fun rest => exp (lam * Z (e.symm (x, rest)))) let tailBound : X → ℝ := fun x => exponentialDeletionPhiSum (fun i => mu (i + 1)) n lam (fun rest => Z (e.symm (x, rest))) (tail x) have hHeadPoint : headEnt ≤ᵐ[nu] headBound := by filter_upwards with rest have hOne := entropy_exp_le_phi_comparison (mu 0) (fun x => lam * Z (e.symm (x, rest))) (lam * head rest) (hHead rest).1 (hHead rest).2 change entropy (mu 0) (fun x => exp (lam * Z (e.symm (x, rest)))) ≤ _ convert hOne using 1 apply integral_congr_ae filter_upwards with x congr 2 ring have hHeadIntegral : (∫ rest, headEnt rest ∂nu) ≤ ∫ rest, headBound rest ∂nu := integral_mono_ae hHeadEntInt hHeadBoundInt hHeadPoint have hTailPoint : tailEnt ≤ᵐ[mu 0] tailBound := by filter_upwards with x exact ih (fun i => mu (i + 1)) (fun rest => Z (e.symm (x, rest))) (tail x) (hTail x) have hTailIntegral : (∫ x, tailEnt x ∂mu 0) ≤ ∫ x, tailBound x ∂mu 0 := integral_mono_ae hTailEntInt hTailBoundInt hTailPoint change (∫ rest, headEnt rest ∂nu) + (∫ x, tailEnt x ∂mu 0) ≤ (∫ rest, headBound rest ∂nu) + ∫ x, tailBound x ∂mu 0 exact add_le_add hHeadIntegral hTailIntegral
    Causalean.Stat.Concentration.EntropyMethod.coordinateEntropySum_exp_le_deletion · Causalean/Stat/Concentration/EntropyMethod/DeletionLogSobolev.lean:136
Finite­Empirical­Supremum 8 core · 24 supporting This file constructs the finite-class empirical supremum used in Bousquet's inequality in the same head--tail recursion as DeletionCoordinateFamily. ★ finiteEmpiricalDeletionIncrementSum_le_supremum

Finite empirical suprema and deletion coordinates

This file constructs the finite-class empirical supremum used in Bousquet's inequality in the same head--tail recursion as DeletionCoordinateFamily. An offset records the contributions of coordinates already fixed by the recursion. This makes every deletion comparison independent of the coordinate being deleted while retaining the ordinary maximum-of-sums statistic.

def finiteEmpiricalScore reviewed
Causalean.Stat.Concentration.EntropyMethod

Given a score class g, a coordinate count n, initial offsets offset, an index i, and a sample s, the recursive empirical score adds the n coordinate scores to the corresponding initial offset.

Definition (Lean source)
parameters
X :
Type u
I :
Type v
g :
I → X → ℝ
n :
ℕ
offset :
I → ℝ
i :
I
s :
Fin n → X
def
finiteEmpiricalScore g n offset i s :
ℝ
given by
offset i + ∑ j, g i (s j)
Causalean.Stat.Concentration.EntropyMethod.finiteEmpiricalScore · Causalean/Stat/Concentration/EntropyMethod/FiniteEmpiricalSupremum.lean:34
def finiteEmpiricalSupremum reviewed
Causalean.Stat.Concentration.EntropyMethod

Given a nonempty finite index type I, a score class g, a coordinate count n, initial offsets offset, and a sample s, the finite empirical supremum is the largest recursive empirical score in the class, with ties broken by finiteClassMaximizer.

Definition (Lean source)
parameters
X :
Type u
I :
Type v
Fintype I
Nonempty I
g :
I → X → ℝ
n :
ℕ
offset :
I → ℝ
s :
Fin n → X
def
finiteEmpiricalSupremum I g n offset s :
ℝ
given by
finiteEmpiricalScore g n offset (finiteClassMaximizer I (finiteEmpiricalScore g n offset) s) s
Causalean.Stat.Concentration.EntropyMethod.finiteEmpiricalSupremum · Causalean/Stat/Concentration/EntropyMethod/FiniteEmpiricalSupremum.lean:41
def finiteEmpiricalMaximizer reviewed
Causalean.Stat.Concentration.EntropyMethod

Given a nonempty finite index type I, a score class g, a coordinate count n, initial offsets offset, and a sample s, the selected finite empirical maximizer is the measurably tie-broken index attaining the supremum.

Definition (Lean source)
parameters
X :
Type u
I :
Type v
Fintype I
Nonempty I
g :
I → X → ℝ
n :
ℕ
offset :
I → ℝ
s :
Fin n → X
def
finiteEmpiricalMaximizer I g n offset s :
I
given by
finiteClassMaximizer I (finiteEmpiricalScore g n offset) s
Causalean.Stat.Concentration.EntropyMethod.finiteEmpiricalMaximizer · Causalean/Stat/Concentration/EntropyMethod/FiniteEmpiricalSupremum.lean:51
def finiteEmpiricalDeletionFamily reviewed
Causalean.Stat.Concentration.EntropyMethod

Given a nonempty finite index type I, a score class g, a coordinate count n, and initial offsets offset, the recursive leave-one-out family uses the supremum with the head coordinate omitted and then adds the fixed head score to the offset before recursing through the tail.

Definition (Lean source)
parameters
X :
Type u
I :
Type v
Fintype I
Nonempty I
g :
I → X → ℝ
n :
ℕ
def
finiteEmpiricalDeletionFamily I g n :
(I → ℝ) → DeletionCoordinateFamily X n
given by
clause 1
| 0, _ => .nil
clause 2
| n + 1, offset
=> .cons (finiteEmpiricalSupremum I g n offset) (fun x => finiteEmpiricalDeletionFamily I g n (fun i => offset i + g i x))
Causalean.Stat.Concentration.EntropyMethod.finiteEmpiricalDeletionFamily · Causalean/Stat/Concentration/EntropyMethod/FiniteEmpiricalSupremum.lean:59 · uses DeletionCoordinateFamily
def finiteEmpiricalSliceIncrement reviewed
Causalean.Stat.Concentration.EntropyMethod

Given a nonempty finite class, scores g, a remaining coordinate count n, offsets offset, a fixed remaining sample rest, and a deleted observation x, the head deletion increment is the new supremum after adding the head score minus the leave-one-out supremum.

Definition (Lean source)
parameters
X :
Type u
I :
Type v
Fintype I
Nonempty I
g :
I → X → ℝ
n :
ℕ
offset :
I → ℝ
rest :
Fin n → X
x :
X
def
finiteEmpiricalSliceIncrement I g n offset rest x :
ℝ
given by
finiteEmpiricalSupremum I g n (fun i => offset i + g i x) rest
- finiteEmpiricalSupremum I g n offset rest
Causalean.Stat.Concentration.EntropyMethod.finiteEmpiricalSliceIncrement · Causalean/Stat/Concentration/EntropyMethod/FiniteEmpiricalSupremum.lean:202
def finiteEmpiricalSliceWitness reviewed
Causalean.Stat.Concentration.EntropyMethod

Given a nonempty finite class, scores g, a remaining coordinate count n, offsets offset, a fixed remaining sample rest, and a deleted observation, the head deletion witness evaluates that observation at the maximizer of the leave-one-out score.

Definition (Lean source)
parameters
X :
Type u
I :
Type v
Fintype I
Nonempty I
g :
I → X → ℝ
n :
ℕ
offset :
I → ℝ
rest :
Fin n → X
x :
X
def
finiteEmpiricalSliceWitness I g n offset rest x :
ℝ
given by
g (finiteEmpiricalMaximizer I g n offset rest) x
Causalean.Stat.Concentration.EntropyMethod.finiteEmpiricalSliceWitness · Causalean/Stat/Concentration/EntropyMethod/FiniteEmpiricalSupremum.lean:212
def finiteEmpiricalDeletionIncrementSum reviewed
Causalean.Stat.Concentration.EntropyMethod

Given a nonempty finite class, scores g, a coordinate count n, initial offsets offset, and a sample s, the recursive sum of deletion increments is zero with no coordinates, while at positive length it adds the head deletion increment to the recursive tail sum after fixing the head coordinate.

Definition (Lean source)
parameters
X :
Type u
I :
Type v
MeasurableSpace X
Fintype I
Nonempty I
g :
I → X → ℝ
n :
ℕ
def
finiteEmpiricalDeletionIncrementSum I g n :
(I → ℝ) → (Fin n → X) → ℝ
given by
clause 1
| 0, _, _ => 0
clause 2
| n + 1, offset, s
=> let e := piFinSuccAbove (fun _ : Fin (n + 1) => X) 0 finiteEmpiricalSliceIncrement I g n offset (e s).2 (e s).1
+ finiteEmpiricalDeletionIncrementSum I g n (fun i => offset i + g i (e s).1) (e s).2
Causalean.Stat.Concentration.EntropyMethod.finiteEmpiricalDeletionIncrementSum · Causalean/Stat/Concentration/EntropyMethod/FiniteEmpiricalSupremum.lean:221
theorem finiteEmpiricalDeletionIncrementSum_le_supremum reviewed
Causalean.Stat.Concentration.EntropyMethod

For a nonempty finite class, scores g, coordinate count n, and sample s, the sum of all recursive deletion increments from zero offset is at most the finite empirical supremum.

Formal statement
hypotheses
X :
Type u
I :
Type v
MeasurableSpace X
Fintype I
Nonempty I
g :
I → X → ℝ
n :
ℕ
s :
Fin n → X
conclusion
finiteEmpiricalDeletionIncrementSum I g n (fun _ => 0) s
≤ finiteEmpiricalSupremum I g n (fun _ => 0) s
Proof (Lean source)
theorem finiteEmpiricalDeletionIncrementSum_le_supremum {X : Type u} {I : Type v} [MeasurableSpace X] [Fintype I] [Nonempty I] (g : I → X → ℝ) (n : ℕ) (s : Fin n → X) : finiteEmpiricalDeletionIncrementSum I g n (fun _ => 0) s ≤ finiteEmpiricalSupremum I g n (fun _ => 0) s := by let i := finiteEmpiricalMaximizer I g n (fun _ => 0) s have h := finiteEmpiricalDeletionIncrementSum_le_score_sub_offset g n (fun _ => 0) s i (finiteEmpiricalSupremum_eq_score g n (fun _ => 0) s) rw [finiteEmpiricalSupremum_eq_score] simpa [i] using h
Causalean.Stat.Concentration.EntropyMethod.finiteEmpiricalDeletionIncrementSum_le_supremum · Causalean/Stat/Concentration/EntropyMethod/FiniteEmpiricalSupremum.lean:331 · uses finiteEmpiricalDeletionIncrementSum , finiteEmpiricalSupremum
24 supporting declarations (lemmas, instances)
Modified­Log­Sobolev 4 core · 3 supporting This file proves the independent-replacement form of the modified logarithmic-Sobolev inequality. ★ modifiedLogSobolev_pi

Modified logarithmic-Sobolev inequality

This file proves the independent-replacement form of the modified logarithmic-Sobolev inequality. The one-coordinate estimate is obtained by symmetrizing the entropy against an independent copy and applying the elementary exponential increment inequality. Finite entropy tensorization then sums this estimate over all coordinates.

The resulting Boucheron--Lugosi--Massart variant has constant 1 multiplying the positive-part replacement square. This is the independent-copy form, rather than the deletion-coordinate form with constant 1 / 2.

structure ReplacementEntropyIntegrable reviewed
Causalean.Stat.Concentration.EntropyMethod

For a coordinate law μ, a tilt lam, and a random variable Z, the one-coordinate replacement conditions require integrability of Z, integrability of the exponential tilt, integrability of the tilted product, and integrability of the positive replacement square.

Definition (Lean source)
parameters
X :
Type u
MeasurableSpace X
μ :
Measure X
lam :
ℝ
Z :
X → ℝ
assumes
hZ :
Integrable Z μ
hexp :
Integrable (fun x => exp (lam * Z x)) μ
hexpZ :
Integrable (fun x => exp (lam * Z x) * Z x) μ
hplus :
Integrable (fun p : X × X => exp (lam * Z p.1) * (max (Z p.1 - Z p.2) 0) ^ 2) (μ.prod μ)
Causalean.Stat.Concentration.EntropyMethod.ReplacementEntropyIntegrable · Causalean/Stat/Concentration/EntropyMethod/ModifiedLogSobolev.lean:274
def exponentialReplacementSquareSum reviewed
Causalean.Stat.Concentration.EntropyMethod

Given coordinate laws μ, a coordinate count n, a tilt lam, and a statistic Z, the tilted sum of expected positive coordinate replacement squares is zero with no coordinates, while at a positive number of coordinates it adds the expected head replacement square and the recursively averaged tail sum.

Definition (Lean source)
parameters
X :
Type u
MeasurableSpace X
μ :
ℕ → Measure X
n :
ℕ
def
exponentialReplacementSquareSum μ n :
ℝ → ((Fin n → X) → ℝ) → ℝ
given by
clause 1
| 0, _, _ => 0
clause 2
| n + 1, lam, Z
=> let e := piFinSuccAbove (fun _ : Fin (n + 1) => X) 0 let ν := Measure.pi (fun j : Fin n => μ (j.val + 1)) (∫ tail, ∫ p : X × X, exp (lam * Z (e.symm (p.1, tail))) * (max (Z (e.symm (p.1, tail)) - Z (e.symm (p.2, tail))) 0) ^ 2 ∂(μ 0).prod (μ 0) ∂ν)
+ ∫ x, exponentialReplacementSquareSum (fun i => μ (i + 1)) n lam (fun tail => Z (e.symm (x, tail))) ∂μ 0
Causalean.Stat.Concentration.EntropyMethod.exponentialReplacementSquareSum · Causalean/Stat/Concentration/EntropyMethod/ModifiedLogSobolev.lean:286
def ModifiedLogSobolevRegularity reviewed
Causalean.Stat.Concentration.EntropyMethod

Given coordinate laws μ, a coordinate count n, a tilt lam, and a statistic Z, the regularity conditions for the finite modified logarithmic-Sobolev induction require the one-coordinate replacement conditions in every head section, recursive tail conditions, and integrability of the four functions compared by the two induction integrals: the zero-coordinate condition is automatic, and the positive-coordinate condition contains the head and tail regularity plus the four integrability clauses.

Definition (Lean source)
parameters
X :
Type u
MeasurableSpace X
μ :
ℕ → Measure X
n :
ℕ
def
ModifiedLogSobolevRegularity μ n :
ℝ → ((Fin n → X) → ℝ) → Prop
given by
clause 1
| 0, _, _ => True
clause 2
| n + 1, lam, Z
=> let e := piFinSuccAbove (fun _ : Fin (n + 1) => X) 0 let ν := Measure.pi (fun j : Fin n => μ (j.val + 1)) (∀ tail, ReplacementEntropyIntegrable (μ 0) lam (fun x => Z (e.symm (x, tail)))) ∧
(∀ x, ModifiedLogSobolevRegularity (fun i => μ (i + 1)) n lam (fun tail => Z (e.symm (x, tail)))) ∧
Integrable (fun tail => entropy (μ 0) (fun x => exp (lam * Z (e.symm (x, tail))))) ν ∧
Integrable (fun tail => ∫ p : X × X, exp (lam * Z (e.symm (p.1, tail))) * (max (Z (e.symm (p.1, tail)) - Z (e.symm (p.2, tail))) 0) ^ 2 ∂(μ 0).prod (μ 0)) ν ∧
Integrable (fun x => coordinateEntropySum (fun i => μ (i + 1)) n (fun tail => exp (lam * Z (e.symm (x, tail))))) (μ 0) ∧
Integrable (fun x => exponentialReplacementSquareSum (fun i => μ (i + 1)) n lam (fun tail => Z (e.symm (x, tail)))) (μ 0)
Causalean.Stat.Concentration.EntropyMethod.ModifiedLogSobolevRegularity · Causalean/Stat/Concentration/EntropyMethod/ModifiedLogSobolev.lean:305
theorem modifiedLogSobolev_pi reviewed
Causalean.Stat.Concentration.EntropyMethod

If the coordinate laws μ are probability laws, the tilt lam is nonnegative, the product has n coordinates, the statistic is Z, finite entropy tensorization applies to its exponential tilt, and the replacement integrability conditions hold recursively, then the entropy of the exponential tilt under the independent product law is at most lam² times the tilted sum of expected positive coordinate replacement squares.

Formal statement
hypotheses
X :
Type u
MeasurableSpace X
μ :
ℕ → Measure X
∀ i, IsProbabilityMeasure (μ i)
lam :
ℝ
hlam :
0 ≤ lam
n :
ℕ
Z :
(Fin n → X) → ℝ
hTensor :
FiniteTensorizationRegularity μ n (fun x => exp (lam * Z x))
hReplacement :
ModifiedLogSobolevRegularity μ n lam Z
conclusion
entropy (Measure.pi (fun i : Fin n => μ i.val)) (fun x => exp (lam * Z x))
≤ lam ^ 2 * exponentialReplacementSquareSum μ n lam Z
Proof (Lean source)
theorem modifiedLogSobolev_pi {X : Type u} [MeasurableSpace X] (μ : ℕ → Measure X) [hprob : ∀ i, IsProbabilityMeasure (μ i)] {lam : ℝ} (hlam : 0 ≤ lam) (n : ℕ) (Z : (Fin n → X) → ℝ) (hTensor : FiniteTensorizationRegularity μ n (fun x => exp (lam * Z x))) (hReplacement : ModifiedLogSobolevRegularity μ n lam Z) : entropy (Measure.pi (fun i : Fin n => μ i.val)) (fun x => exp (lam * Z x)) ≤ lam ^ 2 * exponentialReplacementSquareSum μ n lam Z := (entropy_pi_le_coordinateEntropySum μ n _ hTensor).trans (coordinateEntropySum_exp_le μ hlam n Z hReplacement)
Causalean.Stat.Concentration.EntropyMethod.modifiedLogSobolev_pi · Causalean/Stat/Concentration/EntropyMethod/ModifiedLogSobolev.lean:416 · uses FiniteTensorizationRegularity , ModifiedLogSobolevRegularity , entropy , exponentialReplacementSquareSum
3 supporting declarations (lemmas, instances)
  • entropy_exp_le_replacement theorem — Given a probability law μ, a real function g, integrability of g, its exponential, and their product, and integrability of the exponentially weighted positive replacement square, the entropy of exp g is at most the expected positive replacement square against an independent copy.
    hypotheses
    X :
    Type*
    MeasurableSpace X
    μ :
    Measure X
    IsProbabilityMeasure μ
    g :
    X → ℝ
    hg :
    Integrable g μ
    hexp :
    Integrable (fun x => exp (g x)) μ
    hexpg :
    Integrable (fun x => exp (g x) * g x) μ
    hplus :
    Integrable (fun p : X × X => exp (g p.1) * (max (g p.1 - g p.2) 0) ^ 2) (μ.prod μ)
    conclusion
    entropy μ (fun x => exp (g x))
    ≤ ∫ p : X × X, exp (g p.1) * (max (g p.1 - g p.2) 0) ^ 2 ∂(μ.prod μ)
    Proof (Lean source)
    theorem entropy_exp_le_replacement {X : Type*} [MeasurableSpace X] (μ : Measure X) [IsProbabilityMeasure μ] (g : X → ℝ) (hg : Integrable g μ) (hexp : Integrable (fun x => exp (g x)) μ) (hexpg : Integrable (fun x => exp (g x) * g x) μ) (hplus : Integrable (fun p : X × X => exp (g p.1) * (max (g p.1 - g p.2) 0) ^ 2) (μ.prod μ)) : entropy μ (fun x => exp (g x)) ≤ ∫ p : X × X, exp (g p.1) * (max (g p.1 - g p.2) 0) ^ 2 ∂(μ.prod μ) := by let M := ∫ x, exp (g x) ∂μ let m := ∫ x, g x ∂μ have hJ := integral_le_log_integral_exp hg hexp have hMnonneg : 0 ≤ M := integral_nonneg fun x => (Real.exp_pos _).le have hent_le : entropy μ (fun x => exp (g x)) ≤ (∫ x, exp (g x) * g x ∂μ) - M * m := by rw [entropy] simp_rw [Real.log_exp] dsimp [M, m] at hJ hMnonneg ⊢ nlinarith [mul_le_mul_of_nonneg_left hJ hMnonneg] let A : X × X → ℝ := fun p => (exp (g p.1) * g p.1) * 1 let B : X × X → ℝ := fun p => exp (g p.1) * g p.2 let C : X × X → ℝ := fun p => g p.1 * exp (g p.2) let D : X × X → ℝ := fun p => 1 * (exp (g p.2) * g p.2) have hA : Integrable A (μ.prod μ) := hexpg.mul_prod (integrable_const 1) have hB : Integrable B (μ.prod μ) := hexp.mul_prod hg have hC : Integrable C (μ.prod μ) := hg.mul_prod hexp have hD : Integrable D (μ.prod μ) := (integrable_const 1).mul_prod hexpg let s : X × X → ℝ := fun p => (exp (g p.1) - exp (g p.2)) * (g p.1 - g p.2) have hs : Integrable s (μ.prod μ) := by have heq : s = fun p => (A p - B p - C p) + D p := by funext p dsimp [s, A, B, C, D] ring rw [heq] exact ((hA.sub hB).sub hC).add hD have hsInt : (∫ p, s p ∂(μ.prod μ)) = 2 * ((∫ x, exp (g x) * g x ∂μ) - M * m) := by have hsub1 : (∫ p, A p - B p ∂(μ.prod μ)) = (∫ p, A p ∂(μ.prod μ)) - ∫ p, B p ∂(μ.prod μ) := by simpa only [Pi.sub_apply] using integral_sub hA hB have hsub2 : (∫ p, A p - B p - C p ∂(μ.prod μ)) = (∫ p, A p - B p ∂(μ.prod μ)) - ∫ p, C p ∂(μ.prod μ) := by simpa only [Pi.sub_apply] using integral_sub (hA.sub hB) hC have hAi : (∫ p, A p ∂(μ.prod μ)) = ∫ x, exp (g x) * g x ∂μ := by simpa [A] using (integral_prod_mul (μ := μ) (ν := μ) (fun x => exp (g x) * g x) (fun _ : X => (1 : ℝ))) have hBi : (∫ p, B p ∂(μ.prod μ)) = (∫ x, exp (g x) ∂μ) * ∫ x, g x ∂μ := by simpa [B] using (integral_prod_mul (μ := μ) (ν := μ) (fun x => exp (g x)) g) have hCi : (∫ p, C p ∂(μ.prod μ)) = (∫ x, g x ∂μ) * ∫ x, exp (g x) ∂μ := by simpa [C] using (integral_prod_mul (μ := μ) (ν := μ) g (fun x => exp (g x))) have hDi : (∫ p, D p ∂(μ.prod μ)) = ∫ x, exp (g x) * g x ∂μ := by simpa [D] using (integral_prod_mul (μ := μ) (ν := μ) (fun _ : X => (1 : ℝ)) (fun x => exp (g x) * g x)) calc (∫ p, s p ∂(μ.prod μ)) = ∫ p, (A p - B p - C p) + D p ∂(μ.prod μ) := by apply integral_congr_ae filter_upwards with p dsimp [s, A, B, C, D] ring _ = (∫ p, A p - B p - C p ∂(μ.prod μ)) + ∫ p, D p ∂(μ.prod μ) := integral_add ((hA.sub hB).sub hC) hD _ = ((∫ p, A p ∂(μ.prod μ)) - ∫ p, B p ∂(μ.prod μ)) - ∫ p, C p ∂(μ.prod μ) + ∫ p, D p ∂(μ.prod μ) := by rw [hsub2, hsub1] _ = 2 * ((∫ x, exp (g x) * g x ∂μ) - M * m) := by rw [hAi, hBi, hCi, hDi] dsimp [M, m] ring let q : X × X → ℝ := fun p => exp (g p.1) * (max (g p.1 - g p.2) 0) ^ 2 have hqswap : Integrable (fun p : X × X => q p.swap) (μ.prod μ) := by simpa [q, Function.comp_def] using hplus.swap have hsumInt : Integrable (fun p : X × X => q p + q p.swap) (μ.prod μ) := hplus.add hqswap have hsymBound : (∫ p, s p ∂(μ.prod μ)) ≤ ∫ p, q p + q p.swap ∂(μ.prod μ) := by apply integral_mono hs hsumInt intro p exact exp_sub_mul_sub_le_posSq (g p.1) (g p.2) have hswap : (∫ p : X × X, q p.swap ∂(μ.prod μ)) = ∫ p : X × X, q p ∂(μ.prod μ) := integral_prod_swap q have hsum : (∫ p, q p + q p.swap ∂(μ.prod μ)) = 2 * ∫ p, q p ∂(μ.prod μ) := by rw [integral_add hplus hqswap, hswap] ring rw [hsInt, hsum] at hsymBound exact hent_le.trans (by change (∫ x, exp (g x) * g x ∂μ) - M * m ≤ ∫ p, q p ∂(μ.prod μ) linarith)
    Causalean.Stat.Concentration.EntropyMethod.entropy_exp_le_replacement · Causalean/Stat/Concentration/EntropyMethod/ModifiedLogSobolev.lean:111
  • entropy_exp_mul_le_replacement theorem — Given a probability law μ, a random variable Z, a nonnegative tilt lam, integrability of Z, its exponential tilt, and their product, and integrability of the tilted positive replacement square, the entropy of the exponential tilt is bounded by lam² times the expected positive replacement square.
    hypotheses
    X :
    Type*
    MeasurableSpace X
    μ :
    Measure X
    IsProbabilityMeasure μ
    Z :
    X → ℝ
    lam :
    ℝ
    hlam :
    0 ≤ lam
    hZ :
    Integrable Z μ
    hexp :
    Integrable (fun x => exp (lam * Z x)) μ
    hexpZ :
    Integrable (fun x => exp (lam * Z x) * Z x) μ
    hplus :
    Integrable (fun p : X × X => exp (lam * Z p.1) * (max (Z p.1 - Z p.2) 0) ^ 2) (μ.prod μ)
    conclusion
    entropy μ (fun x => exp (lam * Z x))
    ≤ lam ^ 2 * ∫ p : X × X, exp (lam * Z p.1) * (max (Z p.1 - Z p.2) 0) ^ 2 ∂(μ.prod μ)
    Proof (Lean source)
    theorem entropy_exp_mul_le_replacement {X : Type*} [MeasurableSpace X] (μ : Measure X) [IsProbabilityMeasure μ] (Z : X → ℝ) {lam : ℝ} (hlam : 0 ≤ lam) (hZ : Integrable Z μ) (hexp : Integrable (fun x => exp (lam * Z x)) μ) (hexpZ : Integrable (fun x => exp (lam * Z x) * Z x) μ) (hplus : Integrable (fun p : X × X => exp (lam * Z p.1) * (max (Z p.1 - Z p.2) 0) ^ 2) (μ.prod μ)) : entropy μ (fun x => exp (lam * Z x)) ≤ lam ^ 2 * ∫ p : X × X, exp (lam * Z p.1) * (max (Z p.1 - Z p.2) 0) ^ 2 ∂(μ.prod μ) := by let g : X → ℝ := fun x => lam * Z x have hg : Integrable g μ := hZ.const_mul lam have hexpg : Integrable (fun x => exp (g x) * g x) μ := by have h := hexpZ.const_mul lam convert h using 1 funext x dsimp [g] ring have hplusg : Integrable (fun p : X × X => exp (g p.1) * (max (g p.1 - g p.2) 0) ^ 2) (μ.prod μ) := by have h := hplus.const_mul (lam ^ 2) convert h using 1 funext p dsimp [g] rw [max_mul_sub_zero hlam] ring have h := entropy_exp_le_replacement μ g hg (by simpa [g] using hexp) hexpg hplusg calc entropy μ (fun x => exp (lam * Z x)) = entropy μ (fun x => exp (g x)) := by rfl _ ≤ ∫ p : X × X, exp (g p.1) * (max (g p.1 - g p.2) 0) ^ 2 ∂(μ.prod μ) := h _ = lam ^ 2 * ∫ p : X × X, exp (lam * Z p.1) * (max (Z p.1 - Z p.2) 0) ^ 2 ∂(μ.prod μ) := by rw [← integral_const_mul] apply integral_congr_ae filter_upwards with p dsimp [g] rw [max_mul_sub_zero hlam] ring
    Causalean.Stat.Concentration.EntropyMethod.entropy_exp_mul_le_replacement · Causalean/Stat/Concentration/EntropyMethod/ModifiedLogSobolev.lean:227
  • coordinateEntropySum_exp_le theorem — If the coordinate laws μ are probability laws, the tilt lam is nonnegative, the product has n coordinates, the statistic is Z, and the replacement integrability conditions hold recursively, then the finite coordinate-entropy sum of the exponential tilt is at most lam² times the tilted sum of expected positive coordinate replacement squares.
    hypotheses
    X :
    Type u
    MeasurableSpace X
    μ :
    ℕ → Measure X
    ∀ i, IsProbabilityMeasure (μ i)
    lam :
    ℝ
    hlam :
    0 ≤ lam
    n :
    ℕ
    Z :
    (Fin n → X) → ℝ
    h :
    ModifiedLogSobolevRegularity μ n lam Z
    conclusion
    coordinateEntropySum μ n (fun x => exp (lam * Z x))
    ≤ lam ^ 2 * exponentialReplacementSquareSum μ n lam Z
    Proof (Lean source)
    theorem coordinateEntropySum_exp_le {X : Type u} [MeasurableSpace X] (μ : ℕ → Measure X) [hprob : ∀ i, IsProbabilityMeasure (μ i)] {lam : ℝ} (hlam : 0 ≤ lam) (n : ℕ) (Z : (Fin n → X) → ℝ) (h : ModifiedLogSobolevRegularity μ n lam Z) : coordinateEntropySum μ n (fun x => exp (lam * Z x)) ≤ lam ^ 2 * exponentialReplacementSquareSum μ n lam Z := by induction n generalizing μ with | zero => simp [coordinateEntropySum, exponentialReplacementSquareSum] | succ n ih => let e := piFinSuccAbove (fun _ : Fin (n + 1) => X) 0 let ν : Measure (Fin n → X) := Measure.pi (fun j : Fin n => μ (j.val + 1)) change (∀ tail, ReplacementEntropyIntegrable (μ 0) lam (fun x => Z (e.symm (x, tail)))) ∧ (∀ x, ModifiedLogSobolevRegularity (fun i => μ (i + 1)) n lam (fun tail => Z (e.symm (x, tail)))) ∧ Integrable (fun tail => entropy (μ 0) (fun x => exp (lam * Z (e.symm (x, tail))))) ν ∧ Integrable (fun tail => ∫ p : X × X, exp (lam * Z (e.symm (p.1, tail))) * (max (Z (e.symm (p.1, tail)) - Z (e.symm (p.2, tail))) 0) ^ 2 ∂(μ 0).prod (μ 0)) ν ∧ Integrable (fun x => coordinateEntropySum (fun i => μ (i + 1)) n (fun tail => exp (lam * Z (e.symm (x, tail))))) (μ 0) ∧ Integrable (fun x => exponentialReplacementSquareSum (fun i => μ (i + 1)) n lam (fun tail => Z (e.symm (x, tail)))) (μ 0) at h rcases h with ⟨hhead, htail, hHeadEntInt, hHeadBoundInt, hTailEntInt, hTailBoundInt⟩ let headBound : (Fin n → X) → ℝ := fun tail => ∫ p : X × X, exp (lam * Z (e.symm (p.1, tail))) * (max (Z (e.symm (p.1, tail)) - Z (e.symm (p.2, tail))) 0) ^ 2 ∂(μ 0).prod (μ 0) let tailEnt : X → ℝ := fun x => coordinateEntropySum (fun i => μ (i + 1)) n (fun tail => exp (lam * Z (e.symm (x, tail)))) let tailBound : X → ℝ := fun x => exponentialReplacementSquareSum (fun i => μ (i + 1)) n lam (fun tail => Z (e.symm (x, tail))) have hHeadPoint : (fun tail => entropy (μ 0) (fun x => exp (lam * Z (e.symm (x, tail))))) ≤ᵐ[ν] fun tail => lam ^ 2 * headBound tail := by filter_upwards with tail exact entropy_exp_mul_le_replacement (μ 0) (fun x => Z (e.symm (x, tail))) hlam (hhead tail).hZ (hhead tail).hexp (hhead tail).hexpZ (hhead tail).hplus have hHeadIntegral : (∫ tail, entropy (μ 0) (fun x => exp (lam * Z (e.symm (x, tail)))) ∂ν) ≤ ∫ tail, lam ^ 2 * headBound tail ∂ν := by exact integral_mono_ae hHeadEntInt (hHeadBoundInt.const_mul (lam ^ 2)) hHeadPoint have hTailPoint : tailEnt ≤ᵐ[μ 0] fun x => lam ^ 2 * tailBound x := by filter_upwards with x exact ih (fun i => μ (i + 1)) (fun tail => Z (e.symm (x, tail))) (htail x) have hTailIntegral : (∫ x, tailEnt x ∂μ 0) ≤ ∫ x, lam ^ 2 * tailBound x ∂μ 0 := by exact integral_mono_ae hTailEntInt (hTailBoundInt.const_mul (lam ^ 2)) hTailPoint have hHeadScale : (∫ tail, lam ^ 2 * headBound tail ∂ν) = lam ^ 2 * ∫ tail, headBound tail ∂ν := by rw [integral_const_mul] have hTailScale : (∫ x, lam ^ 2 * tailBound x ∂μ 0) = lam ^ 2 * ∫ x, tailBound x ∂μ 0 := by rw [integral_const_mul] change (∫ tail, entropy (μ 0) (fun x => exp (lam * Z (e.symm (x, tail)))) ∂ν) + (∫ x, tailEnt x ∂μ 0) ≤ lam ^ 2 * ((∫ tail, headBound tail ∂ν) + ∫ x, tailBound x ∂μ 0) rw [hHeadScale] at hHeadIntegral rw [hTailScale] at hTailIntegral linarith
    Causalean.Stat.Concentration.EntropyMethod.coordinateEntropySum_exp_le · Causalean/Stat/Concentration/EntropyMethod/ModifiedLogSobolev.lean:334
Tensorization 2 core · 0 supporting This file proves the two-coordinate case of sub-additivity of entropy (BLM, Theorem 4.10). ★ entropy_prod_le

Two-coordinate entropy tensorization

This file proves the two-coordinate case of sub-additivity of entropy (BLM, Theorem 4.10). The proof first establishes the entropy chain rule and then applies the Gibbs variational characterization to show that averaging over one coordinate cannot increase entropy beyond the average of the section entropies.

The regularity bundle records only measurability and integrability facts used by Fubini and the variational argument. Bounded strictly positive measurable functions satisfy these conditions.

structure EntropyTensorizationIntegrable reviewed
Causalean.Stat.Concentration.EntropyMethod

For probability laws μ and ν and a function f on their product, the tensorization regularity conditions require integrability of f, integrability of f log f, pointwise positivity, positive means in almost every second-coordinate section, integrability of the first-coordinate average times its logarithm, positivity of that average almost everywhere, positivity of the total mean, integrability of f times the logarithmic optimizer, and integrability of the second-coordinate section entropies.

Definition (Lean source)
parameters
X Y :
Type*
MeasurableSpace X
MeasurableSpace Y
μ :
Measure X
ν :
Measure Y
f :
X × Y → ℝ
assumes
hf :
Integrable f (μ.prod ν)
hflog :
Integrable (fun z => f z * log (f z)) (μ.prod ν)
hfpos :
∀ x y, 0 < f (x, y)
hsectionMeanPos :
∀ᵐ x ∂μ, 0 < ∫ y, f (x, y) ∂ν
hAlog :
Integrable (fun y => (∫ x, f (x, y) ∂μ) * log (∫ x, f (x, y) ∂μ)) ν
hApos :
∀ᵐ y ∂ν, 0 < ∫ x, f (x, y) ∂μ
hm :
0 < ∫ y, (∫ x, f (x, y) ∂μ) ∂ν
hfg :
Integrable (fun z => f z * log ((∫ x, f (x, z.2) ∂μ) / ∫ y, (∫ x, f (x, y) ∂μ) ∂ν)) (μ.prod ν)
hEntropy :
Integrable (fun x => entropy ν (fun y => f (x, y))) μ
Causalean.Stat.Concentration.EntropyMethod.EntropyTensorizationIntegrable · Causalean/Stat/Concentration/EntropyMethod/Tensorization.lean:30
theorem entropy_prod_le reviewed
Causalean.Stat.Concentration.EntropyMethod

Under the stated positivity and integrability conditions, the entropy of a function of two independent coordinates is at most the expected entropy in the first coordinate plus the expected entropy in the second coordinate.

Formal statement
hypotheses
X Y :
Type*
MeasurableSpace X
MeasurableSpace Y
μ :
Measure X
ν :
Measure Y
IsProbabilityMeasure μ
IsProbabilityMeasure ν
f :
X × Y → ℝ
h :
EntropyTensorizationIntegrable μ ν f
conclusion
entropy (μ.prod ν) f
≤ (∫ y, entropy μ (fun x => f (x, y)) ∂ν) + (∫ x, entropy ν (fun y => f (x, y)) ∂μ)
Proof (Lean source)
theorem entropy_prod_le {X Y : Type*} [MeasurableSpace X] [MeasurableSpace Y] (μ : Measure X) (ν : Measure Y) [IsProbabilityMeasure μ] [IsProbabilityMeasure ν] (f : X × Y → ℝ) (h : EntropyTensorizationIntegrable μ ν f) : entropy (μ.prod ν) f ≤ (∫ y, entropy μ (fun x => f (x, y)) ∂ν) + (∫ x, entropy ν (fun y => f (x, y)) ∂μ) := by rw [entropy_prod_chain μ ν f h.hf h.hflog h.hAlog] have hconvex := entropy_integral_le_integral_entropy μ ν f h have hadd := add_le_add_left hconvex (∫ y, entropy μ (fun x => f (x, y)) ∂ν) simpa [add_comm] using hadd
Causalean.Stat.Concentration.EntropyMethod.entropy_prod_le · Causalean/Stat/Concentration/EntropyMethod/Tensorization.lean:127 · uses EntropyTensorizationIntegrable , entropy
Bounded­Regularity 1 core · 3 supporting The real-valued entropy tensorization API records explicit Bochner and Fubini hypotheses. ★ finiteTensorizationRegularity_of_bounded_positive

Automatic entropy regularity for bounded positive functions

The real-valued entropy tensorization API records explicit Bochner and Fubini hypotheses. This file discharges those hypotheses for measurable functions bounded between two positive finite constants, the situation needed for exponential tilts of bounded empirical suprema. Measurability of the entropy section needs joint measurability alone; the bounds enter the entropy bound and the integrability statements.

theorem finiteTensorizationRegularity_of_bounded_positive reviewed
Causalean.Stat.Concentration.EntropyMethod

If the coordinate laws mu are probability laws, a measurable function f on an n-fold product is bounded below by a positive constant c and above by a finite constant C, then all finite entropy-tensorization regularity conditions hold.

Formal statement
hypotheses
X :
Type*
MeasurableSpace X
mu :
ℕ → Measure X
∀ i, IsProbabilityMeasure (mu i)
n :
ℕ
f :
(Fin n → X) → ℝ
hf :
Measurable f
c C :
ℝ
hc :
0 < c
hlower :
∀ s, c ≤ f s
hupper :
∀ s, f s ≤ C
conclusion
FiniteTensorizationRegularity mu n f
Proof (Lean source)
theorem finiteTensorizationRegularity_of_bounded_positive {X : Type*} [MeasurableSpace X] (mu : ℕ → Measure X) [hprob : ∀ i, IsProbabilityMeasure (mu i)] (n : ℕ) (f : (Fin n → X) → ℝ) (hf : Measurable f) {c C : ℝ} (hc : 0 < c) (hlower : ∀ s, c ≤ f s) (hupper : ∀ s, f s ≤ C) : FiniteTensorizationRegularity mu n f := by induction n generalizing mu with | zero => trivial | succ n ih => let e := piFinSuccAbove (fun _ : Fin (n + 1) => X) 0 let nu : Measure (Fin n → X) := Measure.pi (fun j : Fin n => mu (j.val + 1)) let g : X × (Fin n → X) → ℝ := fun p => f (e.symm p) have hg : Measurable g := hf.comp e.symm.measurable have hbin : EntropyTensorizationIntegrable (mu 0) nu g := entropyTensorizationIntegrable_of_bounded_positive (mu 0) nu g hg hc (fun z => hlower _) (fun z => hupper _) have htail : ∀ x, FiniteTensorizationRegularity (fun i => mu (i + 1)) n (fun rest => f (e.symm (x, rest))) := by intro x exact ih (fun i => mu (i + 1)) (fun rest => f (e.symm (x, rest))) (hf.comp (e.symm.measurable.comp (measurable_const.prodMk measurable_id))) (fun rest => hlower _) (fun rest => hupper _) let gswap : (Fin n → X) × X → ℝ := fun q => f (e.symm (q.2, q.1)) have hgswap : Measurable gswap := by dsimp [gswap] fun_prop have hEntropyMeas : Measurable (fun x => entropy nu (fun rest => f (e.symm (x, rest)))) := measurable_entropy_section nu hgswap have hEntropyInt : Integrable (fun x => entropy nu (fun rest => f (e.symm (x, rest)))) (mu 0) := by apply integrable_of_measurable_abs_le'' hEntropyMeas intro x exact abs_entropy_section_le nu hgswap hc (fun z => hlower _) (fun z => hupper _) x let tailParam : X × (Fin n → X) → ℝ := fun p => f (e.symm p) have hsum := measurable_coordinateEntropySum_param (fun i => mu (i + 1)) n tailParam hg hc (fun z => hlower _) (fun z => hupper _) have hsumInt : Integrable (fun x => coordinateEntropySum (fun i => mu (i + 1)) n (fun rest => f (e.symm (x, rest)))) (mu 0) := by exact integrable_of_measurable_abs_le'' hsum.1 hsum.2 exact ⟨hbin, htail, hEntropyInt, hsumInt⟩
Causalean.Stat.Concentration.EntropyMethod.finiteTensorizationRegularity_of_bounded_positive · Causalean/Stat/Concentration/EntropyMethod/BoundedRegularity.lean:345 · uses FiniteTensorizationRegularity
3 supporting declarations (lemmas, instances)
  • measurable_entropy_section theorem — For a jointly measurable function f, the entropy in the first coordinate is measurable as a function of the second coordinate under the probability law mu.
    hypotheses
    X Y :
    Type*
    MeasurableSpace X
    MeasurableSpace Y
    mu :
    Measure X
    IsProbabilityMeasure mu
    f :
    X × Y → ℝ
    hf :
    Measurable f
    conclusion
    Measurable (fun y => entropy mu (fun x => f (x, y)))
    Proof (Lean source)
    @[fun_prop] theorem measurable_entropy_section {X Y : Type*} [MeasurableSpace X] [MeasurableSpace Y] (mu : Measure X) [IsProbabilityMeasure mu] {f : X × Y → ℝ} (hf : Measurable f) : Measurable (fun y => entropy mu (fun x => f (x, y))) := by have hfStrong : StronglyMeasurable f := hf.stronglyMeasurable have hflogStrong : StronglyMeasurable (fun z => f z * log (f z)) := by fun_prop have hfirst : StronglyMeasurable (fun y => ∫ x, f (x, y) * log (f (x, y)) ∂mu) := hflogStrong.integral_prod_left' have hmean : StronglyMeasurable (fun y => ∫ x, f (x, y) ∂mu) := hfStrong.integral_prod_left' unfold entropy exact hfirst.measurable.sub (hmean.measurable.mul hmean.measurable.log)
    Causalean.Stat.Concentration.EntropyMethod.measurable_entropy_section · Causalean/Stat/Concentration/EntropyMethod/BoundedRegularity.lean:66
  • abs_entropy_section_le theorem — If a jointly measurable function f is bounded below by a positive constant c and above by C, then every first-coordinate entropy section is bounded by twice C times the maximum endpoint log-magnitude under the probability law mu, at each second-coordinate value y.
    hypotheses
    X Y :
    Type*
    MeasurableSpace X
    MeasurableSpace Y
    mu :
    Measure X
    IsProbabilityMeasure mu
    f :
    X × Y → ℝ
    c C :
    ℝ
    hf :
    Measurable f
    hc :
    0 < c
    hlower :
    ∀ z, c ≤ f z
    hupper :
    ∀ z, f z ≤ C
    y :
    Y
    conclusion
    |entropy mu (fun x => f (x, y))| ≤ 2 * C * max |log c| |log C|
    Proof (Lean source)
    theorem abs_entropy_section_le {X Y : Type*} [MeasurableSpace X] [MeasurableSpace Y] (mu : Measure X) [IsProbabilityMeasure mu] {f : X × Y → ℝ} {c C : ℝ} (hf : Measurable f) (hc : 0 < c) (hlower : ∀ z, c ≤ f z) (hupper : ∀ z, f z ≤ C) (y : Y) : |entropy mu (fun x => f (x, y))| ≤ 2 * C * max |log c| |log C| := by let L := max |log c| |log C| let x0 : X := choice (nonempty_of_isProbabilityMeasure mu) have hCpos : 0 < C := hc.trans_le ((hlower (x0, y)).trans (hupper _)) have hsecMeas : Measurable (fun x => f (x, y)) := hf.comp (measurable_id.prodMk measurable_const) have hsec : Integrable (fun x => f (x, y)) mu := integrable_of_measurable_abs_le'' hsecMeas (fun x => by rw [abs_of_pos (hc.trans_le (hlower (x, y)))] exact hupper (x, y)) have hflog : Integrable (fun x => f (x, y) * log (f (x, y))) mu := by apply integrable_of_measurable_abs_le'' (C := C * L) ((hf.mul hf.log).comp (measurable_id.prodMk measurable_const)) intro x change |f (x, y) * log (f (x, y))| ≤ C * L rw [abs_mul, abs_of_pos (hc.trans_le (hlower (x, y)))] exact mul_le_mul (hupper _) (abs_log_le_of_mem_Icc hc (hlower _) (hupper _)) (abs_nonneg _) hCpos.le have hmean := integral_section_mem_Icc mu (fun _ => hsec) (fun x _ => hlower (x, y)) (fun x _ => hupper (x, y)) y unfold entropy have hfirst : |∫ x, f (x, y) * log (f (x, y)) ∂mu| ≤ C * L := by calc _ ≤ ∫ x, |f (x, y) * log (f (x, y))| ∂mu := abs_integral_le_integral_abs _ ≤ ∫ _x, C * L ∂mu := integral_mono hflog.abs (integrable_const _) (fun x => by rw [abs_mul, abs_of_pos (hc.trans_le (hlower (x, y)))] exact mul_le_mul (hupper _) (abs_log_le_of_mem_Icc hc (hlower _) (hupper _)) (abs_nonneg _) hCpos.le) _ = C * L := by simp have hsecond : |(∫ x, f (x, y) ∂mu) * log (∫ x, f (x, y) ∂mu)| ≤ C * L := by rw [abs_mul, abs_of_pos (hc.trans_le hmean.1)] exact mul_le_mul hmean.2 (abs_log_le_of_mem_Icc hc hmean.1 hmean.2) (abs_nonneg _) hCpos.le exact (abs_sub _ _).trans (by dsimp [L] at hfirst hsecond ⊢; linarith)
    Causalean.Stat.Concentration.EntropyMethod.abs_entropy_section_le · Causalean/Stat/Concentration/EntropyMethod/BoundedRegularity.lean:90
  • entropyTensorizationIntegrable_of_bounded_positive theorem — If two probability laws mu,nu and a measurable product function f satisfy a strictly positive lower bound c and a finite upper bound C, then all regularity hypotheses for binary entropy tensorization hold.
    hypotheses
    X Y :
    Type*
    MeasurableSpace X
    MeasurableSpace Y
    mu :
    Measure X
    nu :
    Measure Y
    IsProbabilityMeasure mu
    IsProbabilityMeasure nu
    f :
    X × Y → ℝ
    hf :
    Measurable f
    c C :
    ℝ
    hc :
    0 < c
    hlower :
    ∀ z, c ≤ f z
    hupper :
    ∀ z, f z ≤ C
    conclusion
    EntropyTensorizationIntegrable mu nu f
    Proof (Lean source)
    theorem entropyTensorizationIntegrable_of_bounded_positive {X Y : Type*} [MeasurableSpace X] [MeasurableSpace Y] (mu : Measure X) (nu : Measure Y) [IsProbabilityMeasure mu] [IsProbabilityMeasure nu] (f : X × Y → ℝ) (hf : Measurable f) {c C : ℝ} (hc : 0 < c) (hlower : ∀ z, c ≤ f z) (hupper : ∀ z, f z ≤ C) : EntropyTensorizationIntegrable mu nu f := by have hCpos : 0 < C := by let x : X := choice (nonempty_of_isProbabilityMeasure mu) let y : Y := choice (nonempty_of_isProbabilityMeasure nu) exact hc.trans_le ((hlower (x, y)).trans (hupper (x, y))) let L := max |log c| |log C| have hfInt : Integrable f (mu.prod nu) := integrable_of_measurable_abs_le'' hf (fun z => by rw [abs_of_pos (hc.trans_le (hlower z))] exact hupper z) have hflog : Integrable (fun z => f z * log (f z)) (mu.prod nu) := by apply integrable_of_measurable_abs_le'' (by fun_prop) intro z rw [abs_mul, abs_of_pos (hc.trans_le (hlower z))] exact mul_le_mul (hupper z) (abs_log_le_of_mem_Icc hc (hlower z) (hupper z)) (abs_nonneg _) hCpos.le have hsectionX (x : X) : Integrable (fun y => f (x, y)) nu := integrable_of_measurable_abs_le'' (hf.comp (measurable_const.prodMk measurable_id)) (fun y => by rw [abs_of_pos (hc.trans_le (hlower (x, y)))]; exact hupper _) have hsectionY (y : Y) : Integrable (fun x => f (x, y)) mu := integrable_of_measurable_abs_le'' (hf.comp (measurable_id.prodMk measurable_const)) (fun x => by rw [abs_of_pos (hc.trans_le (hlower (x, y)))]; exact hupper _) let A : Y → ℝ := fun y => ∫ x, f (x, y) ∂mu have hAmeas : Measurable A := hf.stronglyMeasurable.integral_prod_left'.measurable have hAbounds : ∀ y, c ≤ A y ∧ A y ≤ C := integral_section_mem_Icc mu hsectionY (fun x y => hlower (x, y)) (fun x y => hupper (x, y)) have hAlog : Integrable (fun y => A y * log (A y)) nu := by apply integrable_of_measurable_abs_le'' (by fun_prop) intro y rw [abs_mul, abs_of_pos (hc.trans_le (hAbounds y).1)] exact mul_le_mul (hAbounds y).2 (abs_log_le_of_mem_Icc hc (hAbounds y).1 (hAbounds y).2) (abs_nonneg _) hCpos.le have hmBounds : c ≤ ∫ y, A y ∂nu ∧ (∫ y, A y ∂nu) ≤ C := integral_section_mem_Icc nu (fun _ => integrable_of_measurable_abs_le'' hAmeas (fun y => by rw [abs_of_pos (hc.trans_le (hAbounds y).1)]; exact (hAbounds y).2)) (fun y (_ : Unit) => (hAbounds y).1) (fun y (_ : Unit) => (hAbounds y).2) () let m := ∫ y, A y ∂nu let R := max |log (c / C)| |log (C / c)| have hratio (y : Y) : c / C ≤ A y / m ∧ A y / m ≤ C / c := by have hmpos : 0 < m := hc.trans_le hmBounds.1 constructor · apply (div_le_div_iff₀ hCpos hmpos).2 exact (mul_le_mul_of_nonneg_left hmBounds.2 hc.le).trans (mul_le_mul_of_nonneg_right (hAbounds y).1 hCpos.le) · apply (div_le_div_iff₀ hmpos hc).2 exact (mul_le_mul_of_nonneg_right (hAbounds y).2 hc.le).trans (mul_le_mul_of_nonneg_left hmBounds.1 hCpos.le) have hratioLower : 0 < c / C := div_pos hc hCpos have hfg : Integrable (fun z => f z * log (A z.2 / m)) (mu.prod nu) := by apply integrable_of_measurable_abs_le'' (by fun_prop) intro z rw [abs_mul, abs_of_pos (hc.trans_le (hlower z))] exact mul_le_mul (hupper z) (abs_log_le_of_mem_Icc hratioLower (hratio z.2).1 (hratio z.2).2) (abs_nonneg _) hCpos.le have hfswap : Measurable (fun z : Y × X => f z.swap) := hf.comp measurable_swap have hEntropyMeas := measurable_entropy_section nu hfswap have hEntropy : Integrable (fun x => entropy nu (fun y => f (x, y))) mu := by apply integrable_of_measurable_abs_le'' hEntropyMeas intro x exact abs_entropy_section_le nu hfswap hc (fun z => hlower z.swap) (fun z => hupper z.swap) x refine { hf := hfInt hflog := hflog hfpos := fun x y => hc.trans_le (hlower (x, y)) hsectionMeanPos := ae_of_all _ fun x => hc.trans_le (integral_section_mem_Icc nu hsectionX (fun y x => hlower (x, y)) (fun y x => hupper (x, y)) x).1 hAlog := hAlog hApos := ae_of_all _ fun y => hc.trans_le (hAbounds y).1 hm := hc.trans_le hmBounds.1 hfg := by simpa [A, m] using hfg hEntropy := hEntropy }
    Causalean.Stat.Concentration.EntropyMethod.entropyTensorizationIntegrable_of_bounded_positive · Causalean/Stat/Concentration/EntropyMethod/BoundedRegularity.lean:137
Bousquet­Differential 1 core · 3 supporting This file proves the global differential step following Boucheron--Lugosi--Massart Lemma 12.8. ★ blm_upper_tail

Differential comparison for Bousquet's entropy bound

This file proves the global differential step following Boucheron--Lugosi--Massart Lemma 12.8. On the small-tilt interval 2λ < 1, the exact Bennett coefficient is bounded by 2λ²; the generic differential comparison theorem then yields a centered sub-gamma MGF and an explicit Bernstein upper tail. The constants are conservative but preserve the variance-sensitive form.

theorem blm_upper_tail reviewed
Causalean.Stat.Concentration.EntropyMethod

Under the exponential-integrability and BLM entropy assumptions, with a nonnegative mean, a nonnegative variance half-proxy c, and positive combined scale E Z + c, every positive deviation t satisfies the conservative variance-sensitive Bousquet upper tail.

Formal statement
hypotheses
Omega :
Type*
MeasurableSpace Omega
Measure Omega
IsProbabilityMeasure mu
Z :
Omega → ℝ
c :
ℝ
hc :
0 ≤ c
hExp :
∀ t : ℝ, Integrable (fun omega => exp (t * Z omega)) mu
hEnt :
∀ t : ℝ
if
0 < t
and
2 * t < 1
then
entropy mu (fun omega => exp (t * Z omega))
≤ (blmPhi (-t) / (1 - exp (-t) / 2)) * ∫ omega, exp (t * Z omega) * (Z omega + c) ∂mu
hmean :
0 ≤ ∫ omega, Z omega ∂mu
hscale :
0 < (∫ omega, Z omega ∂mu) + c
t :
ℝ
ht :
0 < t
conclusion
mu.real {omega | t ≤ Z omega - ∫ x, Z x ∂mu}
≤ exp (-t ^ 2 / (8 * ((∫ omega, Z omega ∂mu) + c) + 4 * t))
Proof (Lean source)
theorem blm_upper_tail {Omega : Type*} [MeasurableSpace Omega] {mu : Measure Omega} [IsProbabilityMeasure mu] {Z : Omega → ℝ} {c : ℝ} (hc : 0 ≤ c) (hExp : ∀ t : ℝ, Integrable (fun omega => exp (t * Z omega)) mu) (hEnt : ∀ t : ℝ, 0 < t → 2 * t < 1 → entropy mu (fun omega => exp (t * Z omega)) ≤ (blmPhi (-t) / (1 - exp (-t) / 2)) * ∫ omega, exp (t * Z omega) * (Z omega + c) ∂mu) (hmean : 0 ≤ ∫ omega, Z omega ∂mu) (hscale : 0 < (∫ omega, Z omega ∂mu) + c) {t : ℝ} (ht : 0 < t) : mu.real {omega | t ≤ Z omega - ∫ x, Z x ∂mu} ≤ exp (-t ^ 2 / (8 * ((∫ omega, Z omega ∂mu) + c) + 4 * t)) := by let m := ∫ x, Z x ∂mu let C := 2 * (m + c) let lam := t / (2 * C + 2 * t) have hC : 0 < C := by dsimp [C, m]; positivity have hden : 0 < 2 * C + 2 * t := by positivity have hlam : 0 ≤ lam := (div_pos ht hden).le have hlamHalf : 2 * lam < 1 := by dsimp [lam] rw [show 2 * (t / (2 * C + 2 * t)) = (2 * t) / (2 * C + 2 * t) by ring] rw [div_lt_iff₀ hden] nlinarith have hint : Integrable (fun omega => exp (lam * (Z omega - m))) mu := by have h := (hExp lam).mul_const (exp (-lam * m)) convert h using 1 funext omega rw [← Real.exp_add] congr 1 ring have hchernoff := measure_ge_le_exp_mul_mgf t hlam hint have hmgf : mgf (fun omega => Z omega - m) mu lam ≤ exp (C * lam ^ 2 / (1 - 2 * lam)) := by simpa [C, m, mul_add, add_mul] using blm_mgf_centered_le hc hExp hEnt hmean hlam hlamHalf calc mu.real {omega | t ≤ Z omega - m} ≤ exp (-lam * t) * mgf (fun omega => Z omega - m) mu lam := hchernoff _ ≤ exp (-lam * t) * exp (C * lam ^ 2 / (1 - 2 * lam)) := mul_le_mul_of_nonneg_left hmgf (Real.exp_pos _).le _ = exp (-t ^ 2 / (4 * C + 4 * t)) := by rw [← Real.exp_add] congr 1 dsimp [lam] have hpole : 1 - 2 * (t / (2 * C + 2 * t)) ≠ 0 := ne_of_gt (sub_pos.mpr hlamHalf) field_simp [hden.ne', hpole, hC.ne'] ring _ = exp (-t ^ 2 / (8 * (m + c) + 4 * t)) := by congr 2 dsimp [C] ring
Causalean.Stat.Concentration.EntropyMethod.blm_upper_tail · Causalean/Stat/Concentration/EntropyMethod/BousquetDifferential.lean:211 · uses blmPhi , entropy
3 supporting declarations (lemmas, instances)
  • blm_bennett_coefficient_le_two_sq theorem — For a nonnegative tilt lam with lam at most one, the BLM Bennett coefficient is at most 2 lam².
    hypotheses
    lam :
    ℝ
    hlam :
    0 ≤ lam
    hlam_one :
    lam ≤ 1
    conclusion
    blmPhi (-lam) / (1 - exp (-lam) / 2) ≤ 2 * lam ^ 2
    Proof (Lean source)
    theorem blm_bennett_coefficient_le_two_sq {lam : ℝ} (hlam : 0 ≤ lam) (hlam_one : lam ≤ 1) : blmPhi (-lam) / (1 - exp (-lam) / 2) ≤ 2 * lam ^ 2 := by have hnorm : ‖-lam‖ ≤ 1 := by simpa [Real.norm_eq_abs, abs_of_nonneg hlam] using hlam_one have hphiAbs := Real.norm_exp_sub_one_sub_id_le hnorm have hphi : blmPhi (-lam) ≤ lam ^ 2 := by rw [Real.norm_eq_abs] at hphiAbs have hrewrite : exp (-lam) - 1 - (-lam) = blmPhi (-lam) := by dsimp [blmPhi] ring rw [hrewrite] at hphiAbs exact (le_abs_self _).trans (by simpa using hphiAbs) have hexp : exp (-lam) ≤ 1 := Real.exp_le_one_iff.mpr (neg_nonpos.mpr hlam) have hden : (1 : ℝ) / 2 ≤ 1 - exp (-lam) / 2 := by linarith have hdenpos : 0 < 1 - exp (-lam) / 2 := lt_of_lt_of_le (by norm_num) hden apply (div_le_iff₀ hdenpos).2 nlinarith [sq_nonneg lam]
    Causalean.Stat.Concentration.EntropyMethod.blm_bennett_coefficient_le_two_sq · Causalean/Stat/Concentration/EntropyMethod/BousquetDifferential.lean:33
  • blm_cgf_centered_le theorem — BLM Lemma 12.8, conservative differential form. Suppose all exponential tilts of Z are integrable, the exact BLM entropy comparison holds at every positive tilt below one half, the mean of Z is nonnegative, and the variance half-proxy c is nonnegative. Then at a nonnegative tilt lam below one half, the centered cumulant-generating function is at most 2 (E Z + c) lam² / (1 - 2 lam).
    hypotheses
    Omega :
    Type*
    MeasurableSpace Omega
    Measure Omega
    IsProbabilityMeasure mu
    Z :
    Omega → ℝ
    c :
    ℝ
    hc :
    0 ≤ c
    hExp :
    ∀ t : ℝ, Integrable (fun omega => exp (t * Z omega)) mu
    hEnt :
    ∀ t : ℝ
    if
    0 < t
    and
    2 * t < 1
    then
    entropy mu (fun omega => exp (t * Z omega))
    ≤ (blmPhi (-t) / (1 - exp (-t) / 2)) * ∫ omega, exp (t * Z omega) * (Z omega + c) ∂mu
    hmean :
    0 ≤ ∫ omega, Z omega ∂mu
    lam :
    ℝ
    hlam :
    0 ≤ lam
    hlam_half :
    2 * lam < 1
    conclusion
    cgf Z mu lam - lam * (∫ omega, Z omega ∂mu)
    ≤ (2 * (∫ omega, Z omega ∂mu) + 2 * c) * lam ^ 2 / (1 - 2 * lam)
    Proof (Lean source)
    theorem blm_cgf_centered_le {Omega : Type*} [MeasurableSpace Omega] {mu : Measure Omega} [IsProbabilityMeasure mu] {Z : Omega → ℝ} {c : ℝ} (hc : 0 ≤ c) (hExp : ∀ t : ℝ, Integrable (fun omega => exp (t * Z omega)) mu) (hEnt : ∀ t : ℝ, 0 < t → 2 * t < 1 → entropy mu (fun omega => exp (t * Z omega)) ≤ (blmPhi (-t) / (1 - exp (-t) / 2)) * ∫ omega, exp (t * Z omega) * (Z omega + c) ∂mu) (hmean : 0 ≤ ∫ omega, Z omega ∂mu) {lam : ℝ} (hlam : 0 ≤ lam) (hlam_half : 2 * lam < 1) : cgf Z mu lam - lam * (∫ omega, Z omega ∂mu) ≤ (2 * (∫ omega, Z omega ∂mu) + 2 * c) * lam ^ 2 / (1 - 2 * lam) := by have hset : interior (integrableExpSet Z mu) = univ := by rw [interior_eq_univ] ext t simpa [integrableExpSet] using hExp t have hdiff : Differentiable ℝ (cgf Z mu) := by intro t exact (analyticAt_cgf (by simp [hset])).differentiableAt have hderiv0 : deriv (cgf Z mu) 0 = ∫ omega, Z omega ∂mu := by simpa using deriv_cgf_zero (X := Z) (μ := mu) (by simp [hset]) have hdifferential : ∀ t, 0 < t → 2 * t < 1 → t * (1 - 2 * t) * deriv (cgf Z mu) t - cgf Z mu t ≤ 2 * c * t ^ 2 := by intro t ht htHalf have htOne : t ≤ 1 := by linarith have hmem : t ∈ interior (integrableExpSet Z mu) := by simp [hset] have hMpos : 0 < mgf Z mu t := mgf_pos (hExp t) have hidentity : entropy mu (fun omega => exp (t * Z omega)) = mgf Z mu t * (t * deriv (cgf Z mu) t - cgf Z mu t) := by rw [entropy] simp_rw [Real.log_exp] rw [show (∫ omega, exp (t * Z omega) * (t * Z omega) ∂mu) = t * ∫ omega, Z omega * exp (t * Z omega) ∂mu by rw [← integral_const_mul] congr with omega ring] rw [show (∫ omega, exp (t * Z omega) ∂mu) = mgf Z mu t by rfl] rw [deriv_cgf hmem] dsimp [cgf] field_simp [hMpos.ne'] have hweightedEq := integral_exp_mul_add_eq_mgf_mul hExp c t hmem have hweightedNonneg := integral_exp_mul_add_nonneg hc ht.le hmean hExp have hfactorNonneg : 0 ≤ deriv (cgf Z mu) t + c := by rw [hweightedEq] at hweightedNonneg exact (mul_nonneg_iff_of_pos_left hMpos).mp hweightedNonneg have hraw := hEnt t ht htHalf rw [hidentity, hweightedEq] at hraw have hdivided : t * deriv (cgf Z mu) t - cgf Z mu t ≤ (blmPhi (-t) / (1 - exp (-t) / 2)) * (deriv (cgf Z mu) t + c) := by exact (mul_le_mul_iff_of_pos_left hMpos).mp (by simpa [mul_assoc, mul_left_comm, mul_comm] using hraw) have htheta := blm_bennett_coefficient_le_two_sq ht.le htOne have hweakened : t * deriv (cgf Z mu) t - cgf Z mu t ≤ 2 * t ^ 2 * (deriv (cgf Z mu) t + c) := hdivided.trans (mul_le_mul_of_nonneg_right htheta hfactorNonneg) nlinarith have hcalc := centered_le_of_differential_inequality (hdiff 0) (fun t _ _ => hdiff t) cgf_zero (by norm_num : (0 : ℝ) ≤ 2) (mul_nonneg (by norm_num) hc) hdifferential hlam hlam_half simpa [hderiv0] using hcalc
    Causalean.Stat.Concentration.EntropyMethod.blm_cgf_centered_le · Causalean/Stat/Concentration/EntropyMethod/BousquetDifferential.lean:116
  • blm_mgf_centered_le theorem — Under the exponential-integrability and BLM entropy assumptions, with a nonnegative mean and a nonnegative variance half-proxy c, the centered MGF at a nonnegative tilt lam below one half obeys the conservative BLM bound, provided the tilt is nonnegative and below one half.
    hypotheses
    Omega :
    Type*
    MeasurableSpace Omega
    Measure Omega
    IsProbabilityMeasure mu
    Z :
    Omega → ℝ
    c :
    ℝ
    hc :
    0 ≤ c
    hExp :
    ∀ t : ℝ, Integrable (fun omega => exp (t * Z omega)) mu
    hEnt :
    ∀ t : ℝ
    if
    0 < t
    and
    2 * t < 1
    then
    entropy mu (fun omega => exp (t * Z omega))
    ≤ (blmPhi (-t) / (1 - exp (-t) / 2)) * ∫ omega, exp (t * Z omega) * (Z omega + c) ∂mu
    hmean :
    0 ≤ ∫ omega, Z omega ∂mu
    lam :
    ℝ
    hlam :
    0 ≤ lam
    hlam_half :
    2 * lam < 1
    conclusion
    mgf (fun omega => Z omega - ∫ x, Z x ∂mu) mu lam
    ≤ exp ((2 * (∫ omega, Z omega ∂mu) + 2 * c) * lam ^ 2 / (1 - 2 * lam))
    Proof (Lean source)
    theorem blm_mgf_centered_le {Omega : Type*} [MeasurableSpace Omega] {mu : Measure Omega} [IsProbabilityMeasure mu] {Z : Omega → ℝ} {c : ℝ} (hc : 0 ≤ c) (hExp : ∀ t : ℝ, Integrable (fun omega => exp (t * Z omega)) mu) (hEnt : ∀ t : ℝ, 0 < t → 2 * t < 1 → entropy mu (fun omega => exp (t * Z omega)) ≤ (blmPhi (-t) / (1 - exp (-t) / 2)) * ∫ omega, exp (t * Z omega) * (Z omega + c) ∂mu) (hmean : 0 ≤ ∫ omega, Z omega ∂mu) {lam : ℝ} (hlam : 0 ≤ lam) (hlam_half : 2 * lam < 1) : mgf (fun omega => Z omega - ∫ x, Z x ∂mu) mu lam ≤ exp ((2 * (∫ omega, Z omega ∂mu) + 2 * c) * lam ^ 2 / (1 - 2 * lam)) := by let m := ∫ x, Z x ∂mu have hcgf := blm_cgf_centered_le hc hExp hEnt hmean hlam hlam_half change mgf (fun omega => Z omega + -m) mu lam ≤ _ rw [mgf_add_const, ← exp_cgf (hExp lam), ← Real.exp_add, Real.exp_le_exp] dsimp [m] at hcgf ⊢ linarith
    Causalean.Stat.Concentration.EntropyMethod.blm_mgf_centered_le · Causalean/Stat/Concentration/EntropyMethod/BousquetDifferential.lean:186
Countable­Empirical­Bousquet 4 core · 10 supporting This file passes the finite empirical-supremum inequality to a countable class through an increasing sequence of finite prefixes. ★ countableEmpiricalSupremum_upper_tail

Bousquet's inequality for countable empirical classes

This file passes the finite empirical-supremum inequality to a countable class through an increasing sequence of finite prefixes. The full supremum is never equipped with a maximizing index: a countable supremum need not be attained. Bounded dominated convergence supplies the expectation limit, while strict upper-tail events are the increasing union of their finite-prefix counterparts.

def countableClassEnumeration reviewed
Causalean.Stat.Concentration.EntropyMethod

For a nonempty countable type I, the canonical countable-class enumeration is a chosen surjection from the natural numbers onto I.

Definition (Lean source)
parameters
I :
Type v
Nonempty I
Countable I
def
countableClassEnumeration I :
ℕ → I
given by
choose (exists_surjective_nat I)
Causalean.Stat.Concentration.EntropyMethod.countableClassEnumeration · Causalean/Stat/Concentration/EntropyMethod/CountableEmpiricalBousquet.lean:24
def countableEmpiricalSupremumTruncation reviewed
Causalean.Stat.Concentration.EntropyMethod

Given a nonempty countable score class g, a sample size n, a finite-prefix length m + 1, and a sample s, the finite-truncation empirical supremum is the maximum of the first m + 1 enumerated zero-offset scores.

Definition (Lean source)
parameters
X :
Type u
I :
Type v
Nonempty I
Countable I
g :
I → X → ℝ
n m :
ℕ
s :
Fin n → X
def
countableEmpiricalSupremumTruncation I g n m s :
ℝ
given by
finiteEmpiricalSupremum (Fin (m + 1)) (fun j => g (countableClassEnumeration I j)) n (fun _ => 0) s
Causalean.Stat.Concentration.EntropyMethod.countableEmpiricalSupremumTruncation · Causalean/Stat/Concentration/EntropyMethod/CountableEmpiricalBousquet.lean:34
def countableEmpiricalSupremum reviewed
Causalean.Stat.Concentration.EntropyMethod

Given a nonempty countable score class g, a sample size n, and a sample s, the countable empirical supremum is the supremum of all zero-offset empirical scores; it does not choose or assume a maximizing index.

Definition (Lean source)
parameters
X :
Type u
I :
Type v
Nonempty I
Countable I
g :
I → X → ℝ
n :
ℕ
s :
Fin n → X
def
countableEmpiricalSupremum I g n s :
ℝ
given by
⨆ i : I, finiteEmpiricalScore g n (fun _ => 0) i s
Causalean.Stat.Concentration.EntropyMethod.countableEmpiricalSupremum · Causalean/Stat/Concentration/EntropyMethod/CountableEmpiricalBousquet.lean:42
theorem countableEmpiricalSupremum_upper_tail reviewed
Causalean.Stat.Concentration.EntropyMethod

Countable-class Bousquet upper tail, with conservative constants. Under an i.i.d. probability law mu, a nonempty countable measurable centered score class g whose scores are bounded in absolute value by the nonnegative constant B, at most one, and have second moments at most the nonnegative proxy sigma2, every positive deviation t obeys the stated variance-sensitive upper tail for the countable n-coordinate empirical supremum, provided its mean plus half the total variance proxy is positive. The denominator is the explicit conservative value 8 E Z + 4 n sigma2 + 4 t.

Formal statement
hypotheses
X :
Type u
I :
Type v
MeasurableSpace X
Nonempty I
Countable I
mu :
Measure X
IsProbabilityMeasure mu
g :
I → X → ℝ
hg :
∀ i, Measurable (g i)
B sigma2 :
ℝ
hB :
0 ≤ B
hbound :
∀ i x, |g i x| ≤ B
hupper :
∀ i x, g i x ≤ 1
hmean :
∀ i, ∫ x, g i x ∂mu = 0
hsigma :
0 ≤ sigma2
hsecond :
∀ i, (∫ x, (g i x) ^ 2 ∂mu) ≤ sigma2
n :
ℕ
hscale :
0 < (∫ s, countableEmpiricalSupremum I g n s ∂Measure.pi (fun _ : Fin n => mu))
+ (n : ℝ) * sigma2 / 2
t :
ℝ
ht :
0 < t
conclusion
(Measure.pi (fun _ : Fin n => mu)).real {s | t ≤ countableEmpiricalSupremum I g n s - ∫ r, countableEmpiricalSupremum I g n r ∂Measure.pi (fun _ : Fin n => mu)}
≤ exp (-t ^ 2 / (8 * ((∫ s, countableEmpiricalSupremum I g n s ∂Measure.pi (fun _ : Fin n => mu)) + (n : ℝ) * sigma2 / 2) + 4 * t))
Proof (Lean source)
theorem countableEmpiricalSupremum_upper_tail {X : Type u} {I : Type v} [MeasurableSpace X] [Nonempty I] [Countable I] (mu : Measure X) [IsProbabilityMeasure mu] (g : I → X → ℝ) (hg : ∀ i, Measurable (g i)) {B sigma2 : ℝ} (hB : 0 ≤ B) (hbound : ∀ i x, |g i x| ≤ B) (hupper : ∀ i x, g i x ≤ 1) (hmean : ∀ i, ∫ x, g i x ∂mu = 0) (hsigma : 0 ≤ sigma2) (hsecond : ∀ i, (∫ x, (g i x) ^ 2 ∂mu) ≤ sigma2) (n : ℕ) (hscale : 0 < (∫ s, countableEmpiricalSupremum I g n s ∂Measure.pi (fun _ : Fin n => mu)) + (n : ℝ) * sigma2 / 2) {t : ℝ} (ht : 0 < t) : (Measure.pi (fun _ : Fin n => mu)).real {s | t ≤ countableEmpiricalSupremum I g n s - ∫ r, countableEmpiricalSupremum I g n r ∂Measure.pi (fun _ : Fin n => mu)} ≤ exp (-t ^ 2 / (8 * ((∫ s, countableEmpiricalSupremum I g n s ∂Measure.pi (fun _ : Fin n => mu)) + (n : ℝ) * sigma2 / 2) + 4 * t)) := by let productMeasure : Measure (Fin n → X) := Measure.pi (fun _ : Fin n => mu) let Z := countableEmpiricalSupremum I g n let meanZ := ∫ s, Z s ∂productMeasure let C := 2 * (meanZ + (n : ℝ) * sigma2 / 2) let lam := t / (2 * C + 2 * t) have hC : 0 < C := by dsimp [C, meanZ, Z, productMeasure]; positivity have hden : 0 < 2 * C + 2 * t := by positivity have hlam : 0 ≤ lam := (div_pos ht hden).le have hlamHalf : 2 * lam < 1 := by dsimp [lam] rw [show 2 * (t / (2 * C + 2 * t)) = (2 * t) / (2 * C + 2 * t) by ring] rw [div_lt_iff₀ hden] nlinarith have hZInt : Integrable Z productMeasure := Integrable.of_bound (measurable_countableEmpiricalSupremum I g hg n).aestronglyMeasurable ((n : ℝ) * B) (ae_of_all _ fun s => by simpa [Z, Real.norm_eq_abs] using abs_countableEmpiricalSupremum_le I g hbound n s) have hmeanZ_abs : |meanZ| ≤ (n : ℝ) * B := by dsimp [meanZ] calc |∫ s, Z s ∂productMeasure| ≤ ∫ s, |Z s| ∂productMeasure := abs_integral_le_integral_abs _ ≤ ∫ _s, (n : ℝ) * B ∂productMeasure := by exact integral_mono hZInt.abs (integrable_const _) (fun s => abs_countableEmpiricalSupremum_le I g hbound n s) _ = (n : ℝ) * B := by simp [productMeasure] have hint : Integrable (fun s => exp (lam * (Z s - meanZ))) productMeasure := by apply Integrable.of_bound (((measurable_countableEmpiricalSupremum I g hg n).sub measurable_const).const_mul lam |>.exp.aestronglyMeasurable) (exp (|lam| * (2 * ((n : ℝ) * B)))) filter_upwards with s rw [Real.norm_eq_abs, abs_of_pos (Real.exp_pos _)] apply Real.exp_le_exp.mpr calc lam * (Z s - meanZ) ≤ |lam * (Z s - meanZ)| := le_abs_self _ _ = |lam| * |Z s - meanZ| := abs_mul _ _ _ ≤ |lam| * (2 * ((n : ℝ) * B)) := by apply mul_le_mul_of_nonneg_left _ (abs_nonneg lam) exact (abs_sub _ _).trans (by linarith [abs_countableEmpiricalSupremum_le I g hbound n s, hmeanZ_abs]) have hchernoff := measure_ge_le_exp_mul_mgf t hlam hint have hmgf : mgf (fun s => Z s - meanZ) productMeasure lam ≤ exp (C * lam ^ 2 / (1 - 2 * lam)) := by have h := countableEmpiricalSupremum_mgf_centered_le mu g hg hB hbound hupper hmean hsigma hsecond n hlam hlamHalf dsimp [C, meanZ, Z, productMeasure] at h ⊢ convert h using 1 <;> ring_nf calc productMeasure.real {s | t ≤ Z s - meanZ} ≤ exp (-lam * t) * mgf (fun s => Z s - meanZ) productMeasure lam := hchernoff _ ≤ exp (-lam * t) * exp (C * lam ^ 2 / (1 - 2 * lam)) := mul_le_mul_of_nonneg_left hmgf (Real.exp_pos _).le _ = exp (-t ^ 2 / (4 * C + 4 * t)) := by rw [← Real.exp_add] congr 1 dsimp [lam] have hpole : 1 - 2 * (t / (2 * C + 2 * t)) ≠ 0 := ne_of_gt (sub_pos.mpr hlamHalf) field_simp [hden.ne', hpole, hC.ne'] ring _ = exp (-t ^ 2 / (8 * (meanZ + (n : ℝ) * sigma2 / 2) + 4 * t)) := by congr 2 dsimp [C] ring
Causalean.Stat.Concentration.EntropyMethod.countableEmpiricalSupremum_upper_tail · Causalean/Stat/Concentration/EntropyMethod/CountableEmpiricalBousquet.lean:341 · uses countableEmpiricalSupremum
10 supporting declarations (lemmas, instances)
Finite­Empirical­Bousquet 3 core · 1 supporting This file sums the conditional Boucheron--Lugosi--Massart slice estimates along the recursive deletion family. ★ finiteEmpiricalDeletionPhiSum_le★ entropy_exp_finiteEmpiricalSupremum_le★ finiteEmpiricalSupremum_upper_tail

Bousquet entropy comparison for finite empirical suprema

This file sums the conditional Boucheron--Lugosi--Massart slice estimates along the recursive deletion family. The head--tail product integrals are then transported back to the ordinary finite product law.

theorem finiteEmpiricalDeletionPhiSum_le reviewed
Causalean.Stat.Concentration.EntropyMethod

Finite-class global form of BLM Lemma 12.8. Under an i.i.d. probability law mu, a nonempty finite measurable score class g with nonnegative offset and score bounds, bounded offsets, scores bounded in absolute value and above by one, centered scores, and second moments at most the nonnegative proxy sigma2, the recursive sum of tilted Bennett deletion costs is at most the BLM factor times the expected tilted recursive deletion budget at every nonnegative tilt lam and coordinate count n.

Formal statement
hypotheses
X :
Type u
I :
Type v
MeasurableSpace X
Fintype I
Nonempty I
mu :
Measure X
IsProbabilityMeasure mu
g :
I → X → ℝ
hg :
∀ i, Measurable (g i)
A B sigma2 lam :
ℝ
hA :
0 ≤ A
hB :
0 ≤ B
hbound :
∀ i x, |g i x| ≤ B
hupper :
∀ i x, g i x ≤ 1
hmean :
∀ i, ∫ x, g i x ∂mu = 0
hsigma :
0 ≤ sigma2
hsecond :
∀ i, (∫ x, (g i x) ^ 2 ∂mu) ≤ sigma2
hlam :
0 ≤ lam
n :
ℕ
offset :
I → ℝ
hoffset :
∀ i, |offset i| ≤ A
conclusion
exponentialDeletionPhiSum (fun _ => mu) n lam (finiteEmpiricalSupremum I g n offset) (finiteEmpiricalDeletionFamily I g n offset)
≤ (blmPhi (-lam) / (1 - exp (-lam) / 2)) * ∫ s, exp (lam * finiteEmpiricalSupremum I g n offset s) * (finiteEmpiricalDeletionIncrementSum I g n offset s + (n : ℝ) * sigma2 / 2) ∂Measure.pi (fun _ : Fin n => mu)
Proof (Lean source)
theorem finiteEmpiricalDeletionPhiSum_le {X : Type u} {I : Type v} [MeasurableSpace X] [Fintype I] [Nonempty I] (mu : Measure X) [IsProbabilityMeasure mu] (g : I → X → ℝ) (hg : ∀ i, Measurable (g i)) {A B sigma2 lam : ℝ} (hA : 0 ≤ A) (hB : 0 ≤ B) (hbound : ∀ i x, |g i x| ≤ B) (hupper : ∀ i x, g i x ≤ 1) (hmean : ∀ i, ∫ x, g i x ∂mu = 0) (hsigma : 0 ≤ sigma2) (hsecond : ∀ i, (∫ x, (g i x) ^ 2 ∂mu) ≤ sigma2) (hlam : 0 ≤ lam) (n : ℕ) (offset : I → ℝ) (hoffset : ∀ i, |offset i| ≤ A) : exponentialDeletionPhiSum (fun _ => mu) n lam (finiteEmpiricalSupremum I g n offset) (finiteEmpiricalDeletionFamily I g n offset) ≤ (blmPhi (-lam) / (1 - exp (-lam) / 2)) * ∫ s, exp (lam * finiteEmpiricalSupremum I g n offset s) * (finiteEmpiricalDeletionIncrementSum I g n offset s + (n : ℝ) * sigma2 / 2) ∂Measure.pi (fun _ : Fin n => mu) := by induction n generalizing A offset with | zero => simp [exponentialDeletionPhiSum, finiteEmpiricalDeletionFamily, finiteEmpiricalDeletionIncrementSum] | succ n ih => let theta := blmPhi (-lam) / (1 - exp (-lam) / 2) let e := piFinSuccAbove (fun _ : Fin (n + 1) => X) 0 let nu : Measure (Fin n → X) := Measure.pi (fun _ : Fin n => mu) let updated : X → I → ℝ := fun x i => offset i + g i x let Z : (Fin (n + 1) → X) → ℝ := finiteEmpiricalSupremum I g (n + 1) offset let headPart : X × (Fin n → X) → ℝ := fun q => exp (lam * Z (e.symm q)) * (finiteEmpiricalSliceIncrement I g n offset q.2 q.1 + sigma2 / 2) let tailPart : X × (Fin n → X) → ℝ := fun q => exp (lam * Z (e.symm q)) * (finiteEmpiricalDeletionIncrementSum I g n (updated q.1) q.2 + (n : ℝ) * sigma2 / 2) have hupdatedBound : ∀ x i, |updated x i| ≤ A + B := by intro x i exact (abs_add_le _ _).trans (add_le_add (hoffset i) (hbound i x)) have hHeadPoint : ∀ rest, (∫ x, exp (lam * Z (e.symm (x, rest))) * blmPhi (-lam * (Z (e.symm (x, rest)) - finiteEmpiricalSupremum I g n offset rest)) ∂mu) ≤ theta * ∫ x, headPart (x, rest) ∂mu := by intro rest have hslice := finiteEmpiricalSlice_phi_cost_le mu g hg hA hB hbound hupper hmean hsigma hsecond hlam n offset hoffset rest simpa [theta, Z, headPart, e, finiteEmpiricalSupremum_succ, finiteEmpiricalSliceIncrement] using hslice have hreg := finiteEmpiricalDeletionLogSobolevRegularity (fun _ => mu) g hg hA hB hbound hupper lam (n + 1) offset hoffset change _ ∧ _ ∧ _ ∧ _ ∧ _ ∧ _ at hreg rcases hreg with ⟨_hHeadExp, _hTailReg, _hHeadEntropyInt, hHeadCostInt, _hTailEntropyInt, hTailCostInt⟩ have hHeadPartJoint : Integrable headPart (mu.prod nu) := by apply integrable_of_measurable_abs_le''' (by have hZmeas : Measurable (fun q : X × (Fin n → X) => Z (e.symm q)) := (measurable_finiteEmpiricalSupremum g hg (n + 1) offset).comp e.symm.measurable let newOffset : X → I → ℝ := fun x i => offset i + g i x have hnew : Measurable (fun q : X × (Fin n → X) => finiteEmpiricalSupremum I g n (newOffset q.1) q.2) := measurable_finiteEmpiricalSupremum_param g hg n newOffset (fun i => by dsimp [newOffset]; fun_prop) have hold : Measurable (fun q : X × (Fin n → X) => finiteEmpiricalSupremum I g n offset q.2) := (measurable_finiteEmpiricalSupremum g hg n offset).comp measurable_snd dsimp [headPart] exact (measurable_const.mul hZmeas).exp.mul ((hnew.sub hold).add measurable_const)) (C := exp (|lam| * (A + ((n : ℝ) + 1) * B)) * (max B 1 + sigma2 / 2)) intro q rw [abs_mul, abs_of_pos (Real.exp_pos _)] have hZ := abs_finiteEmpiricalSupremum_le g hbound (n + 1) offset hoffset (e.symm q) have hDelta := abs_sliceIncrement_le''' g hbound hupper n offset q.2 q.1 have he : exp (lam * Z (e.symm q)) ≤ exp (|lam| * (A + ((n : ℝ) + 1) * B)) := by apply Real.exp_le_exp.mpr calc _ ≤ |lam * Z (e.symm q)| := le_abs_self _ _ = |lam| * |Z (e.symm q)| := abs_mul _ _ _ ≤ _ := mul_le_mul_of_nonneg_left (by simpa [Z] using hZ) (abs_nonneg lam) have ha : |finiteEmpiricalSliceIncrement I g n offset q.2 q.1 + sigma2 / 2| ≤ max B 1 + sigma2 / 2 := by calc _ ≤ |finiteEmpiricalSliceIncrement I g n offset q.2 q.1| + |sigma2 / 2| := abs_add_le _ _ _ ≤ _ := by rw [abs_of_nonneg (by positivity : 0 ≤ sigma2 / 2)] exact add_le_add hDelta le_rfl exact mul_le_mul he ha (abs_nonneg _) (Real.exp_pos _).le have hHeadPartInt : Integrable (fun rest => ∫ x, headPart (x, rest) ∂mu) nu := hHeadPartJoint.integral_prod_right have hHead : (∫ rest, ∫ x, exp (lam * Z (e.symm (x, rest))) * blmPhi (-lam * (Z (e.symm (x, rest)) - finiteEmpiricalSupremum I g n offset rest)) ∂mu ∂nu) ≤ theta * ∫ rest, ∫ x, headPart (x, rest) ∂mu ∂nu := by rw [← integral_const_mul] exact integral_mono hHeadCostInt (hHeadPartInt.const_mul theta) hHeadPoint have hTailPoint : ∀ x, exponentialDeletionPhiSum (fun _ => mu) n lam (finiteEmpiricalSupremum I g n (updated x)) (finiteEmpiricalDeletionFamily I g n (updated x)) ≤ theta * ∫ rest, tailPart (x, rest) ∂nu := by intro x simpa [theta, tailPart, Z, e, updated, finiteEmpiricalSupremum_succ] using ih (A := A + B) (by positivity) (updated x) (hupdatedBound x) have hTailPartJoint : Integrable tailPart (mu.prod nu) := by apply integrable_of_measurable_abs_le''' (by have hZmeas : Measurable (fun q : X × (Fin n → X) => Z (e.symm q)) := (measurable_finiteEmpiricalSupremum g hg (n + 1) offset).comp e.symm.measurable have hsumMeas : Measurable (fun q : X × (Fin n → X) => finiteEmpiricalDeletionIncrementSum I g n (updated q.1) q.2) := measurable_finiteEmpiricalDeletionIncrementSum_param g hg n updated (fun i => by dsimp [updated]; fun_prop) dsimp [tailPart] exact (measurable_const.mul hZmeas).exp.mul (hsumMeas.add measurable_const)) (C := exp (|lam| * (A + ((n : ℝ) + 1) * B)) * ((n : ℝ) * max B 1 + (n : ℝ) * sigma2 / 2)) intro q rw [abs_mul, abs_of_pos (Real.exp_pos _)] have hZ := abs_finiteEmpiricalSupremum_le g hbound (n + 1) offset hoffset (e.symm q) have hsum := abs_finiteEmpiricalDeletionIncrementSum_le g hbound hupper n (updated q.1) q.2 have he : exp (lam * Z (e.symm q)) ≤ exp (|lam| * (A + ((n : ℝ) + 1) * B)) := by apply Real.exp_le_exp.mpr calc _ ≤ |lam * Z (e.symm q)| := le_abs_self _ _ = |lam| * |Z (e.symm q)| := abs_mul _ _ _ ≤ _ := mul_le_mul_of_nonneg_left (by simpa [Z] using hZ) (abs_nonneg lam) have ha : |finiteEmpiricalDeletionIncrementSum I g n (updated q.1) q.2 + (n : ℝ) * sigma2 / 2| ≤ (n : ℝ) * max B 1 + (n : ℝ) * sigma2 / 2 := by calc _ ≤ |finiteEmpiricalDeletionIncrementSum I g n (updated q.1) q.2| + |(n : ℝ) * sigma2 / 2| := abs_add_le _ _ _ ≤ _ := by rw [abs_of_nonneg (by positivity : 0 ≤ (n : ℝ) * sigma2 / 2)] exact add_le_add hsum le_rfl exact mul_le_mul he ha (abs_nonneg _) (Real.exp_pos _).le have hTailPartInt : Integrable (fun x => ∫ rest, tailPart (x, rest) ∂nu) mu := hTailPartJoint.integral_prod_left have hTail : (∫ x, exponentialDeletionPhiSum (fun _ => mu) n lam (finiteEmpiricalSupremum I g n (updated x)) (finiteEmpiricalDeletionFamily I g n (updated x)) ∂mu) ≤ theta * ∫ x, ∫ rest, tailPart (x, rest) ∂nu ∂mu := by have hTailCostInt' : Integrable (fun x => exponentialDeletionPhiSum (fun _ => mu) n lam (finiteEmpiricalSupremum I g n (updated x)) (finiteEmpiricalDeletionFamily I g n (updated x))) mu := by simpa [updated, e, finiteEmpiricalSupremum_succ] using hTailCostInt rw [← integral_const_mul] exact integral_mono hTailCostInt' (hTailPartInt.const_mul theta) hTailPoint have hsplit : MeasurePreserving e (Measure.pi (fun _ : Fin (n + 1) => mu)) (mu.prod nu) := by simpa [e, nu] using (MeasureTheory.measurePreserving_piFinSuccAbove (μ := fun _ : Fin (n + 1) => mu) 0) have hBudget : (∫ rest, ∫ x, headPart (x, rest) ∂mu ∂nu) + (∫ x, ∫ rest, tailPart (x, rest) ∂nu ∂mu) = ∫ s, exp (lam * finiteEmpiricalSupremum I g (n + 1) offset s) * (finiteEmpiricalDeletionIncrementSum I g (n + 1) offset s + ((n + 1 : ℕ) : ℝ) * sigma2 / 2) ∂Measure.pi (fun _ : Fin (n + 1) => mu) := by have hheadSwap : (∫ rest, ∫ x, headPart (x, rest) ∂mu ∂nu) = ∫ p, headPart p ∂(mu.prod nu) := (integral_prod_symm headPart hHeadPartJoint).symm have htailProd : (∫ x, ∫ rest, tailPart (x, rest) ∂nu ∂mu) = ∫ p, tailPart p ∂(mu.prod nu) := (integral_prod tailPart hTailPartJoint).symm rw [hheadSwap, htailProd, ← integral_add hHeadPartJoint hTailPartJoint] let budget : (Fin (n + 1) → X) → ℝ := fun s => exp (lam * finiteEmpiricalSupremum I g (n + 1) offset s) * (finiteEmpiricalDeletionIncrementSum I g (n + 1) offset s + ((n + 1 : ℕ) : ℝ) * sigma2 / 2) have htransport := hsplit.integral_comp' (headPart + tailPart) have hpoint : (headPart + tailPart) ∘ e = budget := by funext s dsimp [headPart, tailPart, budget, Z, updated] rw [e.symm_apply_apply] change exp _ * (_ + sigma2 / 2) + exp _ * (_ + (n : ℝ) * sigma2 / 2) = exp _ * (_ + ((n + 1 : ℕ) : ℝ) * sigma2 / 2) rw [finiteEmpiricalDeletionIncrementSum] dsimp [e] push_cast ring calc (∫ p, headPart p + tailPart p ∂(mu.prod nu)) = ∫ s, (headPart + tailPart) (e s) ∂Measure.pi (fun _ : Fin (n + 1) => mu) := htransport.symm _ = ∫ s, budget s ∂Measure.pi (fun _ : Fin (n + 1) => mu) := by apply integral_congr_ae filter_upwards with s exact congrFun hpoint s _ = _ := rfl have htotal : (∫ rest, ∫ x, exp (lam * Z (e.symm (x, rest))) * blmPhi (-lam * (Z (e.symm (x, rest)) - finiteEmpiricalSupremum I g n offset rest)) ∂mu ∂nu) + (∫ x, exponentialDeletionPhiSum (fun _ => mu) n lam (finiteEmpiricalSupremum I g n (updated x)) (finiteEmpiricalDeletionFamily I g n (updated x)) ∂mu) ≤ theta * ∫ s, exp (lam * finiteEmpiricalSupremum I g (n + 1) offset s) * (finiteEmpiricalDeletionIncrementSum I g (n + 1) offset s + ((n + 1 : ℕ) : ℝ) * sigma2 / 2) ∂Measure.pi (fun _ : Fin (n + 1) => mu) := by calc _ ≤ theta * (∫ rest, ∫ x, headPart (x, rest) ∂mu ∂nu) + theta * (∫ x, ∫ rest, tailPart (x, rest) ∂nu ∂mu) := add_le_add hHead hTail _ = theta * ((∫ rest, ∫ x, headPart (x, rest) ∂mu ∂nu) + (∫ x, ∫ rest, tailPart (x, rest) ∂nu ∂mu)) := by ring _ = _ := by rw [hBudget] simpa [exponentialDeletionPhiSum, finiteEmpiricalDeletionFamily, theta, Z, e, nu, updated, finiteEmpiricalSupremum_succ] using htotal
Causalean.Stat.Concentration.EntropyMethod.finiteEmpiricalDeletionPhiSum_le · Causalean/Stat/Concentration/EntropyMethod/FiniteEmpiricalBousquet.lean:59 · uses blmPhi , exponentialDeletionPhiSum , finiteEmpiricalDeletionFamily , finiteEmpiricalDeletionIncrementSum , finiteEmpiricalSupremum
theorem entropy_exp_finiteEmpiricalSupremum_le reviewed
Causalean.Stat.Concentration.EntropyMethod

Finite-class entropy form of BLM Lemma 12.8. Under an i.i.d. probability law mu, a nonempty finite measurable centered score class g whose scores are bounded in absolute value by the nonnegative constant B, at most one, and have second moments at most the nonnegative proxy sigma2, the entropy of the exponentially tilted zero-offset empirical supremum is bounded by the BLM factor times its tilted affine variance budget at every nonnegative tilt lam and coordinate count n.

Formal statement
hypotheses
X :
Type u
I :
Type v
MeasurableSpace X
Fintype I
Nonempty I
mu :
Measure X
IsProbabilityMeasure mu
g :
I → X → ℝ
hg :
∀ i, Measurable (g i)
B sigma2 lam :
ℝ
hB :
0 ≤ B
hbound :
∀ i x, |g i x| ≤ B
hupper :
∀ i x, g i x ≤ 1
hmean :
∀ i, ∫ x, g i x ∂mu = 0
hsigma :
0 ≤ sigma2
hsecond :
∀ i, (∫ x, (g i x) ^ 2 ∂mu) ≤ sigma2
hlam :
0 ≤ lam
n :
ℕ
conclusion
entropy (Measure.pi (fun _ : Fin n => mu)) (fun s => exp (lam * finiteEmpiricalSupremum I g n (fun _ => 0) s))
≤ (blmPhi (-lam) / (1 - exp (-lam) / 2)) * ∫ s, exp (lam * finiteEmpiricalSupremum I g n (fun _ => 0) s) * (finiteEmpiricalSupremum I g n (fun _ => 0) s + (n : ℝ) * sigma2 / 2) ∂Measure.pi (fun _ : Fin n => mu)
Proof (Lean source)
theorem entropy_exp_finiteEmpiricalSupremum_le {X : Type u} {I : Type v} [MeasurableSpace X] [Fintype I] [Nonempty I] (mu : Measure X) [IsProbabilityMeasure mu] (g : I → X → ℝ) (hg : ∀ i, Measurable (g i)) {B sigma2 lam : ℝ} (hB : 0 ≤ B) (hbound : ∀ i x, |g i x| ≤ B) (hupper : ∀ i x, g i x ≤ 1) (hmean : ∀ i, ∫ x, g i x ∂mu = 0) (hsigma : 0 ≤ sigma2) (hsecond : ∀ i, (∫ x, (g i x) ^ 2 ∂mu) ≤ sigma2) (hlam : 0 ≤ lam) (n : ℕ) : entropy (Measure.pi (fun _ : Fin n => mu)) (fun s => exp (lam * finiteEmpiricalSupremum I g n (fun _ => 0) s)) ≤ (blmPhi (-lam) / (1 - exp (-lam) / 2)) * ∫ s, exp (lam * finiteEmpiricalSupremum I g n (fun _ => 0) s) * (finiteEmpiricalSupremum I g n (fun _ => 0) s + (n : ℝ) * sigma2 / 2) ∂Measure.pi (fun _ : Fin n => mu) := by let productMeasure : Measure (Fin n → X) := Measure.pi (fun _ : Fin n => mu) let Z := finiteEmpiricalSupremum I g n (fun _ => 0) let D := finiteEmpiricalDeletionIncrementSum I g n (fun _ => 0) let theta := blmPhi (-lam) / (1 - exp (-lam) / 2) have hEntropy := entropy_exp_finiteEmpiricalSupremum_le_deletion (fun _ => mu) g hg (A := 0) (B := B) (by norm_num) hB hbound hupper lam n (fun _ => 0) (fun _ => by simp) have hCost := finiteEmpiricalDeletionPhiSum_le mu g hg (A := 0) (B := B) (sigma2 := sigma2) (lam := lam) (by norm_num) hB hbound hupper hmean hsigma hsecond hlam n (fun _ => 0) (fun _ => by simp) have hDInt : Integrable (fun s => exp (lam * Z s) * (D s + (n : ℝ) * sigma2 / 2)) productMeasure := by apply integrable_of_measurable_abs_le''' (by dsimp [Z, D] fun_prop) (C := exp (|lam| * ((n : ℝ) * B)) * ((n : ℝ) * max B 1 + (n : ℝ) * sigma2 / 2)) intro s rw [abs_mul, abs_of_pos (Real.exp_pos _)] have hZ := abs_finiteEmpiricalSupremum_le g (A := 0) (B := B) hbound n (fun _ => 0) (fun _ => by simp) s have hD := abs_finiteEmpiricalDeletionIncrementSum_le g hbound hupper n (fun _ => 0) s have he : exp (lam * Z s) ≤ exp (|lam| * ((n : ℝ) * B)) := by apply Real.exp_le_exp.mpr calc _ ≤ |lam * Z s| := le_abs_self _ _ = |lam| * |Z s| := abs_mul _ _ _ ≤ _ := mul_le_mul_of_nonneg_left (by simpa [Z] using hZ) (abs_nonneg lam) have ha : |D s + (n : ℝ) * sigma2 / 2| ≤ (n : ℝ) * max B 1 + (n : ℝ) * sigma2 / 2 := by calc _ ≤ |D s| + |(n : ℝ) * sigma2 / 2| := abs_add_le _ _ _ ≤ _ := by rw [abs_of_nonneg (by positivity : 0 ≤ (n : ℝ) * sigma2 / 2)] exact add_le_add (by simpa [D] using hD) le_rfl exact mul_le_mul he ha (abs_nonneg _) (Real.exp_pos _).le have hZInt : Integrable (fun s => exp (lam * Z s) * (Z s + (n : ℝ) * sigma2 / 2)) productMeasure := by apply integrable_of_measurable_abs_le''' (by dsimp [Z] fun_prop) (C := exp (|lam| * ((n : ℝ) * B)) * ((n : ℝ) * B + (n : ℝ) * sigma2 / 2)) intro s rw [abs_mul, abs_of_pos (Real.exp_pos _)] have hZ := abs_finiteEmpiricalSupremum_le g (A := 0) (B := B) hbound n (fun _ => 0) (fun _ => by simp) s have he : exp (lam * Z s) ≤ exp (|lam| * ((n : ℝ) * B)) := by apply Real.exp_le_exp.mpr calc _ ≤ |lam * Z s| := le_abs_self _ _ = |lam| * |Z s| := abs_mul _ _ _ ≤ _ := mul_le_mul_of_nonneg_left (by simpa [Z] using hZ) (abs_nonneg lam) have ha : |Z s + (n : ℝ) * sigma2 / 2| ≤ (n : ℝ) * B + (n : ℝ) * sigma2 / 2 := by calc _ ≤ |Z s| + |(n : ℝ) * sigma2 / 2| := abs_add_le _ _ _ ≤ _ := by rw [abs_of_nonneg (by positivity : 0 ≤ (n : ℝ) * sigma2 / 2)] exact add_le_add (by simpa [Z] using hZ) le_rfl exact mul_le_mul he ha (abs_nonneg _) (Real.exp_pos _).le have hIntegral : (∫ s, exp (lam * Z s) * (D s + (n : ℝ) * sigma2 / 2) ∂productMeasure) ≤ ∫ s, exp (lam * Z s) * (Z s + (n : ℝ) * sigma2 / 2) ∂productMeasure := by apply integral_mono hDInt hZInt intro s exact mul_le_mul_of_nonneg_left (by dsimp [D, Z] exact add_le_add (finiteEmpiricalDeletionIncrementSum_le_supremum g n s) le_rfl) (Real.exp_pos _).le calc _ ≤ exponentialDeletionPhiSum (fun _ => mu) n lam Z (finiteEmpiricalDeletionFamily I g n (fun _ => 0)) := by simpa [Z, productMeasure] using hEntropy _ ≤ theta * ∫ s, exp (lam * Z s) * (D s + (n : ℝ) * sigma2 / 2) ∂productMeasure := by simpa [theta, Z, D, productMeasure] using hCost _ ≤ theta * ∫ s, exp (lam * Z s) * (Z s + (n : ℝ) * sigma2 / 2) ∂productMeasure := mul_le_mul_of_nonneg_left hIntegral (blmFactor_nonneg hlam)
Causalean.Stat.Concentration.EntropyMethod.entropy_exp_finiteEmpiricalSupremum_le · Causalean/Stat/Concentration/EntropyMethod/FiniteEmpiricalBousquet.lean:295 · uses blmPhi , entropy , finiteEmpiricalSupremum
theorem finiteEmpiricalSupremum_upper_tail reviewed
Causalean.Stat.Concentration.EntropyMethod

Finite-class Bousquet upper tail, with conservative constants. Under an i.i.d. probability law mu, a nonempty finite measurable centered score class g whose scores are bounded in absolute value by the nonnegative constant B, at most one, and have second moments at most the nonnegative proxy sigma2, every positive deviation t obeys the stated variance-sensitive upper tail for the zero-offset n-coordinate empirical supremum, provided its mean plus half the total variance proxy is positive. The denominator is the explicit conservative value 8 E Z + 4 n sigma2 + 4 t.

Formal statement
hypotheses
X :
Type u
I :
Type v
MeasurableSpace X
Fintype I
Nonempty I
mu :
Measure X
IsProbabilityMeasure mu
g :
I → X → ℝ
hg :
∀ i, Measurable (g i)
B sigma2 :
ℝ
hB :
0 ≤ B
hbound :
∀ i x, |g i x| ≤ B
hupper :
∀ i x, g i x ≤ 1
hmean :
∀ i, ∫ x, g i x ∂mu = 0
hsigma :
0 ≤ sigma2
hsecond :
∀ i, (∫ x, (g i x) ^ 2 ∂mu) ≤ sigma2
n :
ℕ
hscale :
0 < (∫ s, finiteEmpiricalSupremum I g n (fun _ => 0) s ∂Measure.pi (fun _ : Fin n => mu))
+ (n : ℝ) * sigma2 / 2
t :
ℝ
ht :
0 < t
conclusion
(Measure.pi (fun _ : Fin n => mu)).real {s | t ≤ finiteEmpiricalSupremum I g n (fun _ => 0) s - ∫ r, finiteEmpiricalSupremum I g n (fun _ => 0) r ∂Measure.pi (fun _ : Fin n => mu)}
≤ exp (-t ^ 2 / (8 * ((∫ s, finiteEmpiricalSupremum I g n (fun _ => 0) s ∂Measure.pi (fun _ : Fin n => mu)) + (n : ℝ) * sigma2 / 2) + 4 * t))
Proof (Lean source)
theorem finiteEmpiricalSupremum_upper_tail {X : Type u} {I : Type v} [MeasurableSpace X] [Fintype I] [Nonempty I] (mu : Measure X) [IsProbabilityMeasure mu] (g : I → X → ℝ) (hg : ∀ i, Measurable (g i)) {B sigma2 : ℝ} (hB : 0 ≤ B) (hbound : ∀ i x, |g i x| ≤ B) (hupper : ∀ i x, g i x ≤ 1) (hmean : ∀ i, ∫ x, g i x ∂mu = 0) (hsigma : 0 ≤ sigma2) (hsecond : ∀ i, (∫ x, (g i x) ^ 2 ∂mu) ≤ sigma2) (n : ℕ) (hscale : 0 < (∫ s, finiteEmpiricalSupremum I g n (fun _ => 0) s ∂Measure.pi (fun _ : Fin n => mu)) + (n : ℝ) * sigma2 / 2) {t : ℝ} (ht : 0 < t) : (Measure.pi (fun _ : Fin n => mu)).real {s | t ≤ finiteEmpiricalSupremum I g n (fun _ => 0) s - ∫ r, finiteEmpiricalSupremum I g n (fun _ => 0) r ∂Measure.pi (fun _ : Fin n => mu)} ≤ exp (-t ^ 2 / (8 * ((∫ s, finiteEmpiricalSupremum I g n (fun _ => 0) s ∂Measure.pi (fun _ : Fin n => mu)) + (n : ℝ) * sigma2 / 2) + 4 * t)) := by let productMeasure : Measure (Fin n → X) := Measure.pi (fun _ : Fin n => mu) let Z := finiteEmpiricalSupremum I g n (fun _ => 0) have hExp : ∀ lam : ℝ, Integrable (fun s => exp (lam * Z s)) productMeasure := by intro lam simpa [Z, productMeasure] using integrable_exp_finiteEmpiricalSupremum mu g hg hbound n lam have hEnt : ∀ lam : ℝ, 0 < lam → 2 * lam < 1 → entropy productMeasure (fun s => exp (lam * Z s)) ≤ (blmPhi (-lam) / (1 - exp (-lam) / 2)) * ∫ s, exp (lam * Z s) * (Z s + (n : ℝ) * sigma2 / 2) ∂productMeasure := by intro lam hlam _hlamHalf simpa [Z, productMeasure] using entropy_exp_finiteEmpiricalSupremum_le mu g hg hB hbound hupper hmean hsigma hsecond hlam.le n have hZMean : 0 ≤ ∫ s, Z s ∂productMeasure := by simpa [Z, productMeasure] using integral_finiteEmpiricalSupremum_nonneg mu g hg hbound hmean n simpa [Z, productMeasure] using blm_upper_tail (Z := Z) (c := (n : ℝ) * sigma2 / 2) (by positivity) hExp hEnt hZMean (by simpa [Z, productMeasure] using hscale) ht
Causalean.Stat.Concentration.EntropyMethod.finiteEmpiricalSupremum_upper_tail · Causalean/Stat/Concentration/EntropyMethod/FiniteEmpiricalBousquet.lean:450 · uses finiteEmpiricalSupremum
1 supporting declaration (lemmas, instances)
  • finiteEmpiricalSupremum_mgf_centered_le theorem — Finite-class centered MGF bound, with conservative constants. Under an i.i.d. probability law mu, a nonempty finite measurable centered score class g whose scores are bounded in absolute value by the nonnegative constant B, at most one, and have second moments at most the nonnegative proxy sigma2, the centered MGF of the zero-offset n-coordinate empirical supremum obeys the displayed BLM bound at a nonnegative tilt below one half.
    hypotheses
    X :
    Type u
    I :
    Type v
    MeasurableSpace X
    Fintype I
    Nonempty I
    mu :
    Measure X
    IsProbabilityMeasure mu
    g :
    I → X → ℝ
    hg :
    ∀ i, Measurable (g i)
    B sigma2 :
    ℝ
    hB :
    0 ≤ B
    hbound :
    ∀ i x, |g i x| ≤ B
    hupper :
    ∀ i x, g i x ≤ 1
    hmean :
    ∀ i, ∫ x, g i x ∂mu = 0
    hsigma :
    0 ≤ sigma2
    hsecond :
    ∀ i, (∫ x, (g i x) ^ 2 ∂mu) ≤ sigma2
    n :
    ℕ
    lam :
    ℝ
    hlam :
    0 ≤ lam
    hlam_half :
    2 * lam < 1
    conclusion
    mgf (fun s => finiteEmpiricalSupremum I g n (fun _ => 0) s - ∫ r, finiteEmpiricalSupremum I g n (fun _ => 0) r ∂Measure.pi (fun _ : Fin n => mu)) (Measure.pi (fun _ : Fin n => mu)) lam
    ≤ exp ((2 * (∫ s, finiteEmpiricalSupremum I g n (fun _ => 0) s ∂Measure.pi (fun _ : Fin n => mu)) + (n : ℝ) * sigma2) * lam ^ 2 / (1 - 2 * lam))
    Proof (Lean source)
    theorem finiteEmpiricalSupremum_mgf_centered_le {X : Type u} {I : Type v} [MeasurableSpace X] [Fintype I] [Nonempty I] (mu : Measure X) [IsProbabilityMeasure mu] (g : I → X → ℝ) (hg : ∀ i, Measurable (g i)) {B sigma2 : ℝ} (hB : 0 ≤ B) (hbound : ∀ i x, |g i x| ≤ B) (hupper : ∀ i x, g i x ≤ 1) (hmean : ∀ i, ∫ x, g i x ∂mu = 0) (hsigma : 0 ≤ sigma2) (hsecond : ∀ i, (∫ x, (g i x) ^ 2 ∂mu) ≤ sigma2) (n : ℕ) {lam : ℝ} (hlam : 0 ≤ lam) (hlam_half : 2 * lam < 1) : mgf (fun s => finiteEmpiricalSupremum I g n (fun _ => 0) s - ∫ r, finiteEmpiricalSupremum I g n (fun _ => 0) r ∂Measure.pi (fun _ : Fin n => mu)) (Measure.pi (fun _ : Fin n => mu)) lam ≤ exp ((2 * (∫ s, finiteEmpiricalSupremum I g n (fun _ => 0) s ∂Measure.pi (fun _ : Fin n => mu)) + (n : ℝ) * sigma2) * lam ^ 2 / (1 - 2 * lam)) := by let productMeasure : Measure (Fin n → X) := Measure.pi (fun _ : Fin n => mu) let Z := finiteEmpiricalSupremum I g n (fun _ => 0) have hExp : ∀ t : ℝ, Integrable (fun s => exp (t * Z s)) productMeasure := by intro t simpa [Z, productMeasure] using integrable_exp_finiteEmpiricalSupremum mu g hg hbound n t have hEnt : ∀ t : ℝ, 0 < t → 2 * t < 1 → entropy productMeasure (fun s => exp (t * Z s)) ≤ (blmPhi (-t) / (1 - exp (-t) / 2)) * ∫ s, exp (t * Z s) * (Z s + (n : ℝ) * sigma2 / 2) ∂productMeasure := by intro t ht _htHalf simpa [Z, productMeasure] using entropy_exp_finiteEmpiricalSupremum_le mu g hg hB hbound hupper hmean hsigma hsecond ht.le n have hZMean : 0 ≤ ∫ s, Z s ∂productMeasure := by simpa [Z, productMeasure] using integral_finiteEmpiricalSupremum_nonneg mu g hg hbound hmean n have hmgf := blm_mgf_centered_le (Z := Z) (c := (n : ℝ) * sigma2 / 2) (by positivity) hExp hEnt hZMean hlam hlam_half dsimp [Z, productMeasure] at hmgf ⊢ convert hmgf using 1 <;> ring
    Causalean.Stat.Concentration.EntropyMethod.finiteEmpiricalSupremum_mgf_centered_le · Causalean/Stat/Concentration/EntropyMethod/FiniteEmpiricalBousquet.lean:403
Finite­Empirical­Deletion 1 core · 1 supporting This file proves the parameter-measurability and boundedness induction needed to integrate the recursive deletion cost for a finite empirical supremum. ★ entropy_exp_finiteEmpiricalSupremum_le_deletion

Regularity of finite empirical deletion costs

This file proves the parameter-measurability and boundedness induction needed to integrate the recursive deletion cost for a finite empirical supremum. It is the remaining Fubini component of the deletion-coordinate modified logarithmic-Sobolev assembly.

theorem entropy_exp_finiteEmpiricalSupremum_le_deletion reviewed
Causalean.Stat.Concentration.EntropyMethod

Under coordinate probability laws mu, a nonempty finite measurable score class g whose scores are bounded by B and at most one, and offsets bounded by the nonnegative constant A, the entropy of the exponential finite empirical supremum is at most its recursive sum of deletion-coordinate Bennett costs at tilt lam and coordinate count n, provided the score bound is nonnegative.

Formal statement
hypotheses
X :
Type u
I :
Type v
MeasurableSpace X
Fintype I
Nonempty I
mu :
ℕ → Measure X
∀ i, IsProbabilityMeasure (mu i)
g :
I → X → ℝ
hg :
∀ i, Measurable (g i)
A B :
ℝ
hA :
0 ≤ A
hB :
0 ≤ B
hbound :
∀ i x, |g i x| ≤ B
hupper :
∀ i x, g i x ≤ 1
lam :
ℝ
n :
ℕ
offset :
I → ℝ
hoffset :
∀ i, |offset i| ≤ A
conclusion
entropy (Measure.pi (fun i : Fin n => mu i.val)) (fun s => exp (lam * finiteEmpiricalSupremum I g n offset s))
≤ exponentialDeletionPhiSum mu n lam (finiteEmpiricalSupremum I g n offset) (finiteEmpiricalDeletionFamily I g n offset)
Proof (Lean source)
theorem entropy_exp_finiteEmpiricalSupremum_le_deletion {X : Type u} {I : Type v} [MeasurableSpace X] [Fintype I] [Nonempty I] (mu : ℕ → Measure X) [hprob : ∀ i, IsProbabilityMeasure (mu i)] (g : I → X → ℝ) (hg : ∀ i, Measurable (g i)) {A B : ℝ} (hA : 0 ≤ A) (hB : 0 ≤ B) (hbound : ∀ i x, |g i x| ≤ B) (hupper : ∀ i x, g i x ≤ 1) (lam : ℝ) (n : ℕ) (offset : I → ℝ) (hoffset : ∀ i, |offset i| ≤ A) : entropy (Measure.pi (fun i : Fin n => mu i.val)) (fun s => exp (lam * finiteEmpiricalSupremum I g n offset s)) ≤ exponentialDeletionPhiSum mu n lam (finiteEmpiricalSupremum I g n offset) (finiteEmpiricalDeletionFamily I g n offset) := by apply deletionModifiedLogSobolev_pi mu n lam (finiteEmpiricalSupremum I g n offset) (finiteEmpiricalDeletionFamily I g n offset) · exact finiteEmpiricalTensorizationRegularity mu g hg hA hB hbound n offset hoffset lam · exact finiteEmpiricalDeletionLogSobolevRegularity mu g hg hA hB hbound hupper lam n offset hoffset
Causalean.Stat.Concentration.EntropyMethod.entropy_exp_finiteEmpiricalSupremum_le_deletion · Causalean/Stat/Concentration/EntropyMethod/FiniteEmpiricalDeletion.lean:426 · uses entropy , exponentialDeletionPhiSum , finiteEmpiricalDeletionFamily , finiteEmpiricalSupremum
1 supporting declaration (lemmas, instances)
Finite­Empirical­Entropy 1 core · 3 supporting This file applies the one-coordinate Boucheron--Lugosi--Massart estimate to every slice of the recursive finite empirical supremum. ★ finiteEmpiricalSlice_phi_cost_le

Entropy bound for finite empirical suprema

This file applies the one-coordinate Boucheron--Lugosi--Massart estimate to every slice of the recursive finite empirical supremum. Boundedness supplies all Bochner-integrability hypotheses; the recursive deletion family then feeds the resulting costs into deletion-coordinate modified log-Sobolev tensorization.

theorem finiteEmpiricalSlice_phi_cost_le reviewed
Causalean.Stat.Concentration.EntropyMethod

Finite-slice input to BLM Lemma 12.8. Under a probability law mu, fix a nonempty finite class of measurable scores g, nonnegative offset and score bounds A,B, bounded offsets, and scores bounded in absolute value and above by one. If the scores are centered, have second moment at most the nonnegative proxy sigma2, and the tilt lam is nonnegative, then for every remaining coordinate count n and remaining sample rest, the conditional tilted Bennett deletion cost is at most the BLM factor times the tilted deletion increment plus half the variance proxy.

Formal statement
hypotheses
X :
Type u
I :
Type v
MeasurableSpace X
Fintype I
Nonempty I
mu :
Measure X
IsProbabilityMeasure mu
g :
I → X → ℝ
hg :
∀ i, Measurable (g i)
A B sigma2 lam :
ℝ
hA :
0 ≤ A
hB :
0 ≤ B
hbound :
∀ i x, |g i x| ≤ B
hupper :
∀ i x, g i x ≤ 1
hmean :
∀ i, ∫ x, g i x ∂mu = 0
hsigma :
0 ≤ sigma2
hsecond :
∀ i, (∫ x, (g i x) ^ 2 ∂mu) ≤ sigma2
hlam :
0 ≤ lam
n :
ℕ
offset :
I → ℝ
hoffset :
∀ i, |offset i| ≤ A
rest :
Fin n → X
conclusion
(∫ x, exp (lam * (finiteEmpiricalSupremum I g n offset rest + finiteEmpiricalSliceIncrement I g n offset rest x)) * blmPhi (-lam * finiteEmpiricalSliceIncrement I g n offset rest x) ∂mu)
≤ (blmPhi (-lam) / (1 - exp (-lam) / 2)) * ∫ x, exp (lam * (finiteEmpiricalSupremum I g n offset rest + finiteEmpiricalSliceIncrement I g n offset rest x)) * (finiteEmpiricalSliceIncrement I g n offset rest x + sigma2 / 2) ∂mu
Proof (Lean source)
theorem finiteEmpiricalSlice_phi_cost_le {X : Type u} {I : Type v} [MeasurableSpace X] [Fintype I] [Nonempty I] (mu : Measure X) [IsProbabilityMeasure mu] (g : I → X → ℝ) (hg : ∀ i, Measurable (g i)) {A B sigma2 lam : ℝ} (hA : 0 ≤ A) (hB : 0 ≤ B) (hbound : ∀ i x, |g i x| ≤ B) (hupper : ∀ i x, g i x ≤ 1) (hmean : ∀ i, ∫ x, g i x ∂mu = 0) (hsigma : 0 ≤ sigma2) (hsecond : ∀ i, (∫ x, (g i x) ^ 2 ∂mu) ≤ sigma2) (hlam : 0 ≤ lam) (n : ℕ) (offset : I → ℝ) (hoffset : ∀ i, |offset i| ≤ A) (rest : Fin n → X) : (∫ x, exp (lam * (finiteEmpiricalSupremum I g n offset rest + finiteEmpiricalSliceIncrement I g n offset rest x)) * blmPhi (-lam * finiteEmpiricalSliceIncrement I g n offset rest x) ∂mu) ≤ (blmPhi (-lam) / (1 - exp (-lam) / 2)) * ∫ x, exp (lam * (finiteEmpiricalSupremum I g n offset rest + finiteEmpiricalSliceIncrement I g n offset rest x)) * (finiteEmpiricalSliceIncrement I g n offset rest x + sigma2 / 2) ∂mu := by let zi := finiteEmpiricalSupremum I g n offset rest let Delta := finiteEmpiricalSliceIncrement I g n offset rest let Y := finiteEmpiricalSliceWitness I g n offset rest let CDelta := max B 1 let CZ := A + ((n : ℝ) + 1) * B have hDeltaMeas : Measurable Delta := measurable_finiteEmpiricalSliceIncrement g hg n offset rest have hYMeas : Measurable Y := measurable_finiteEmpiricalSliceWitness g hg n offset rest have hDeltaBound : ∀ x, |Delta x| ≤ CDelta := abs_sliceIncrement_le g hbound hupper n offset rest have hYBound : ∀ x, |Y x| ≤ B := fun x => hbound _ x have hDelta : Integrable Delta mu := integrable_of_measurable_abs_le' hDeltaMeas hDeltaBound have hY : Integrable Y mu := integrable_of_measurable_abs_le' hYMeas hYBound have hDeltaSq : Integrable (fun x => Delta x ^ 2) mu := by apply integrable_of_measurable_abs_le' (hDeltaMeas.pow_const 2) intro x rw [abs_pow] exact pow_le_pow_left₀ (abs_nonneg _) (hDeltaBound x) 2 have hYSq : Integrable (fun x => Y x ^ 2) mu := by apply integrable_of_measurable_abs_le' (hYMeas.pow_const 2) intro x rw [abs_pow] exact pow_le_pow_left₀ (abs_nonneg _) (hYBound x) 2 have hupdated (x : X) : ∀ i, |offset i + g i x| ≤ A + B := by intro i exact (abs_add_le _ _).trans (add_le_add (hoffset i) (hbound i x)) have hZBound (x : X) : |zi + Delta x| ≤ CZ := by have hsup := abs_finiteEmpiricalSupremum_le g hbound n (fun i => offset i + g i x) (hupdated x) rest have hid : zi + Delta x = finiteEmpiricalSupremum I g n (fun i => offset i + g i x) rest := by dsimp [zi, Delta, finiteEmpiricalSliceIncrement] ring rw [hid] dsimp [CZ] nlinarith have hCZ : 0 ≤ CZ := by dsimp [CZ]; positivity have hExpMeas : Measurable (fun x => exp (lam * (zi + Delta x))) := by fun_prop have hExp : Integrable (fun x => exp (lam * (zi + Delta x))) mu := by apply integrable_of_measurable_abs_le' hExpMeas intro x rw [abs_of_pos (Real.exp_pos _)] apply Real.exp_le_exp.mpr calc lam * (zi + Delta x) ≤ |lam * (zi + Delta x)| := le_abs_self _ _ = |lam| * |zi + Delta x| := abs_mul _ _ _ ≤ |lam| * CZ := mul_le_mul_of_nonneg_left (hZBound x) (abs_nonneg lam) have hExpDelta : Integrable (fun x => exp (lam * (zi + Delta x)) * Delta x) mu := by apply integrable_of_measurable_abs_le' (C := exp (|lam| * CZ) * CDelta) (hExpMeas.mul hDeltaMeas) intro x change |exp (lam * (zi + Delta x)) * Delta x| ≤ _ rw [abs_mul, abs_of_pos (Real.exp_pos _)] have he : exp (lam * (zi + Delta x)) ≤ exp (|lam| * CZ) := by apply Real.exp_le_exp.mpr calc lam * (zi + Delta x) ≤ |lam * (zi + Delta x)| := le_abs_self _ _ = |lam| * |zi + Delta x| := abs_mul _ _ _ ≤ |lam| * CZ := mul_le_mul_of_nonneg_left (hZBound x) (abs_nonneg lam) exact mul_le_mul he (hDeltaBound x) (abs_nonneg _) (Real.exp_pos _).le have hPhiMeas : Measurable (fun x => exp (lam * (zi + Delta x)) * blmPhi (-lam * Delta x)) := by dsimp [blmPhi] fun_prop have hPhi : Integrable (fun x => exp (lam * (zi + Delta x)) * blmPhi (-lam * Delta x)) mu := by apply integrable_of_measurable_abs_le' (C := exp (|lam| * CZ) * (exp (|lam| * CDelta) + |lam| * CDelta + 1)) hPhiMeas intro x let E := exp (|lam| * CZ) let P := exp (|lam| * CDelta) + |lam| * CDelta + 1 have he : exp (lam * (zi + Delta x)) ≤ E := by apply Real.exp_le_exp.mpr exact (show lam * (zi + Delta x) ≤ |lam| * CZ by calc _ ≤ |lam * (zi + Delta x)| := le_abs_self _ _ = |lam| * |zi + Delta x| := abs_mul _ _ _ ≤ _ := mul_le_mul_of_nonneg_left (hZBound x) (abs_nonneg lam)) have harg : |-lam * Delta x| ≤ |lam| * CDelta := by rw [abs_mul, abs_neg] exact mul_le_mul_of_nonneg_left (hDeltaBound x) (abs_nonneg lam) have hphi : |blmPhi (-lam * Delta x)| ≤ P := by dsimp [blmPhi, P] calc |exp (-lam * Delta x) - (-lam * Delta x) - 1| ≤ |exp (-lam * Delta x) - (-lam * Delta x)| + |(1 : ℝ)| := abs_sub _ _ _ ≤ (|exp (-lam * Delta x)| + |-lam * Delta x|) + 1 := by simpa using add_le_add_right (abs_sub (exp (-lam * Delta x)) (-lam * Delta x)) 1 _ = exp (-lam * Delta x) + |-lam * Delta x| + 1 := by rw [abs_of_pos (Real.exp_pos _)] _ ≤ exp (|lam| * CDelta) + |lam| * CDelta + 1 := by simpa [add_comm, add_left_comm, add_assoc] using add_le_add_right (add_le_add (Real.exp_le_exp.mpr (le_trans (le_abs_self _) harg)) harg) 1 change |exp (lam * (zi + Delta x)) * blmPhi (-lam * Delta x)| ≤ _ rw [abs_mul, abs_of_pos (Real.exp_pos _)] exact mul_le_mul he hphi (abs_nonneg _) (Real.exp_pos _).le have hLower : ∀ᵐ x ∂mu, Y x ≤ Delta x := ae_of_all _ (finiteEmpiricalSliceWitness_le_increment g n offset rest) have hDeltaUpper : ∀ᵐ x ∂mu, Delta x ≤ 1 := ae_of_all _ (finiteEmpiricalSliceIncrement_le_one g hupper n offset rest) have hYUpper : ∀ᵐ x ∂mu, Y x ≤ 1 := ae_of_all _ (finiteEmpiricalSliceWitness_le_one g hupper n offset rest) have hYMean : 0 ≤ ∫ x, Y x ∂mu := by rw [integral_finiteEmpiricalSliceWitness_eq_zero mu g hmean n offset rest] have hDeltaMean : 0 ≤ ∫ x, Delta x ∂mu := integral_finiteEmpiricalSliceIncrement_nonneg g hg hbound hupper hmean n offset rest have hYSecond : (∫ x, Y x ^ 2 ∂mu) ≤ sigma2 := integral_finiteEmpiricalSliceWitness_sq_le mu g hsecond n offset rest exact blm_conditional_phi_cost_le hlam hsigma hDelta hDeltaSq hY hYSq hExp hExpDelta hPhi hLower hDeltaUpper hYUpper hYMean hDeltaMean hYSecond
Causalean.Stat.Concentration.EntropyMethod.finiteEmpiricalSlice_phi_cost_le · Causalean/Stat/Concentration/EntropyMethod/FiniteEmpiricalEntropy.lean:181 · uses blmPhi , finiteEmpiricalSliceIncrement , finiteEmpiricalSupremum
3 supporting declarations (lemmas, instances)
Herbst 1 core · 2 supporting This file turns an entropy bound for every exponential tilt into a centered logarithmic moment-generating-function bound. ★ herbst_upper_tail

The Herbst argument

This file turns an entropy bound for every exponential tilt into a centered logarithmic moment-generating-function bound. The proof is the classical Herbst differential argument from Boucheron--Lugosi--Massart, Section 6.1.

theorem herbst_upper_tail reviewed
Causalean.Stat.Concentration.EntropyMethod

Under exponential integrability at every real tilt, the entropy bound at every positive tilt, and a positive variance proxy, every positive deviation of the centered variable obeys the sub-Gaussian upper-tail bound.

Formal statement
hypotheses
Ω :
Type*
MeasurableSpace Ω
Measure Ω
IsProbabilityMeasure μ
Z :
Ω → ℝ
v :
ℝ
hExp :
∀ t : ℝ, Integrable (fun ω => exp (t * Z ω)) μ
hEnt :
∀ t : ℝ
if
0 < t
then
entropy μ (fun ω => exp (t * Z ω)) ≤ t ^ 2 * v / 2 * ∫ ω, exp (t * Z ω) ∂μ
hv :
0 < v
t :
ℝ
ht :
0 < t
conclusion
μ.real {ω | t ≤ Z ω - ∫ x, Z x ∂μ} ≤ exp (-t ^ 2 / (2 * v))
Proof (Lean source)
theorem herbst_upper_tail {Ω : Type*} [MeasurableSpace Ω] {μ : Measure Ω} [IsProbabilityMeasure μ] {Z : Ω → ℝ} {v : ℝ} (hExp : ∀ t : ℝ, Integrable (fun ω => exp (t * Z ω)) μ) (hEnt : ∀ t : ℝ, 0 < t → entropy μ (fun ω => exp (t * Z ω)) ≤ t ^ 2 * v / 2 * ∫ ω, exp (t * Z ω) ∂μ) (hv : 0 < v) {t : ℝ} (ht : 0 < t) : μ.real {ω | t ≤ Z ω - ∫ x, Z x ∂μ} ≤ exp (-t ^ 2 / (2 * v)) := by let m := ∫ x, Z x ∂μ let lam := t / v have hlam : 0 < lam := div_pos ht hv have hint : Integrable (fun ω => exp (lam * (Z ω - m))) μ := by have h := (hExp lam).mul_const (exp (-lam * m)) convert h using 1 funext ω rw [← Real.exp_add] congr 1 ring have hchernoff := measure_ge_le_exp_mul_mgf t hlam.le hint have hmgf : mgf (fun ω => Z ω - m) μ lam ≤ exp (lam ^ 2 * v / 2) := by dsimp [m] exact herbst_mgf_centered_le hExp hEnt hlam calc μ.real {ω | t ≤ Z ω - ∫ x, Z x ∂μ} = μ.real {ω | t ≤ Z ω - m} := by rfl _ ≤ exp (-lam * t) * mgf (fun ω => Z ω - m) μ lam := hchernoff _ ≤ exp (-lam * t) * exp (lam ^ 2 * v / 2) := mul_le_mul_of_nonneg_left hmgf (Real.exp_pos _).le _ = exp (-t ^ 2 / (2 * v)) := by rw [← Real.exp_add] congr 1 dsimp [lam] field_simp [hv.ne'] ring
Causalean.Stat.Concentration.EntropyMethod.herbst_upper_tail · Causalean/Stat/Concentration/EntropyMethod/Herbst.lean:160 · uses entropy
2 supporting declarations (lemmas, instances)
  • herbst_cgf_le theorem — Under exponential integrability at every real tilt and the entropy bound at every positive tilt, the centered cumulant-generating function at a positive tilt is at most lam ^ 2 * v / 2 as claimed.
    hypotheses
    Ω :
    Type*
    MeasurableSpace Ω
    Measure Ω
    IsProbabilityMeasure μ
    Z :
    Ω → ℝ
    v :
    ℝ
    hExp :
    ∀ t : ℝ, Integrable (fun ω => exp (t * Z ω)) μ
    hEnt :
    ∀ t : ℝ
    if
    0 < t
    then
    entropy μ (fun ω => exp (t * Z ω)) ≤ t ^ 2 * v / 2 * ∫ ω, exp (t * Z ω) ∂μ
    lam :
    ℝ
    hlam :
    0 < lam
    conclusion
    cgf Z μ lam - lam * (∫ ω, Z ω ∂μ) ≤ lam ^ 2 * v / 2
    Proof (Lean source)
    theorem herbst_cgf_le {Ω : Type*} [MeasurableSpace Ω] {μ : Measure Ω} [IsProbabilityMeasure μ] {Z : Ω → ℝ} {v : ℝ} (hExp : ∀ t : ℝ, Integrable (fun ω => exp (t * Z ω)) μ) (hEnt : ∀ t : ℝ, 0 < t → entropy μ (fun ω => exp (t * Z ω)) ≤ t ^ 2 * v / 2 * ∫ ω, exp (t * Z ω) ∂μ) {lam : ℝ} (hlam : 0 < lam) : cgf Z μ lam - lam * (∫ ω, Z ω ∂μ) ≤ lam ^ 2 * v / 2 := by have hset : interior (integrableExpSet Z μ) = univ := by rw [interior_eq_univ] ext t simpa [integrableExpSet] using hExp t have hdiff : Differentiable ℝ (cgf Z μ) := by intro t exact (analyticAt_cgf (by simp [hset])).differentiableAt have hderiv0 : deriv (cgf Z μ) 0 = ∫ ω, Z ω ∂μ := by simpa using deriv_cgf_zero (X := Z) (μ := μ) (by simp [hset]) have hdifferential : ∀ t : ℝ, 0 < t → t * deriv (cgf Z μ) t - cgf Z μ t ≤ t ^ 2 * v / 2 := by intro t ht have hmem : t ∈ interior (integrableExpSet Z μ) := by simp [hset] have hMpos : 0 < mgf Z μ t := mgf_pos (hExp t) have hidentity : entropy μ (fun ω => exp (t * Z ω)) = mgf Z μ t * (t * deriv (cgf Z μ) t - cgf Z μ t) := by rw [entropy] simp_rw [Real.log_exp] rw [show (∫ ω, exp (t * Z ω) * (t * Z ω) ∂μ) = t * ∫ ω, Z ω * exp (t * Z ω) ∂μ by rw [← integral_const_mul] congr with ω ring] rw [show (∫ ω, exp (t * Z ω) ∂μ) = mgf Z μ t by rfl] rw [deriv_cgf hmem] dsimp [cgf] field_simp [hMpos.ne'] have hbound := hEnt t ht rw [hidentity, show (∫ ω, exp (t * Z ω) ∂μ) = mgf Z μ t by rfl] at hbound exact (mul_le_mul_iff_of_pos_left hMpos).mp (by simpa [mul_comm, mul_left_comm, mul_assoc] using hbound) have hcalc := herbst_calculus hdiff cgf_zero hdifferential lam hlam simpa [hderiv0] using hcalc
    Causalean.Stat.Concentration.EntropyMethod.herbst_cgf_le · Causalean/Stat/Concentration/EntropyMethod/Herbst.lean:94
  • herbst_mgf_centered_le theorem — Under exponential integrability at every real tilt and the entropy bound at every positive tilt, the moment-generating function of the centered variable at a positive tilt satisfies the sub-Gaussian bound.
    hypotheses
    Ω :
    Type*
    MeasurableSpace Ω
    Measure Ω
    IsProbabilityMeasure μ
    Z :
    Ω → ℝ
    v :
    ℝ
    hExp :
    ∀ t : ℝ, Integrable (fun ω => exp (t * Z ω)) μ
    hEnt :
    ∀ t : ℝ
    if
    0 < t
    then
    entropy μ (fun ω => exp (t * Z ω)) ≤ t ^ 2 * v / 2 * ∫ ω, exp (t * Z ω) ∂μ
    lam :
    ℝ
    hlam :
    0 < lam
    conclusion
    mgf (fun ω => Z ω - ∫ x, Z x ∂μ) μ lam ≤ exp (lam ^ 2 * v / 2)
    Proof (Lean source)
    theorem herbst_mgf_centered_le {Ω : Type*} [MeasurableSpace Ω] {μ : Measure Ω} [IsProbabilityMeasure μ] {Z : Ω → ℝ} {v : ℝ} (hExp : ∀ t : ℝ, Integrable (fun ω => exp (t * Z ω)) μ) (hEnt : ∀ t : ℝ, 0 < t → entropy μ (fun ω => exp (t * Z ω)) ≤ t ^ 2 * v / 2 * ∫ ω, exp (t * Z ω) ∂μ) {lam : ℝ} (hlam : 0 < lam) : mgf (fun ω => Z ω - ∫ x, Z x ∂μ) μ lam ≤ exp (lam ^ 2 * v / 2) := by let m := ∫ x, Z x ∂μ have hcgf := herbst_cgf_le hExp hEnt hlam change mgf (fun ω => Z ω + -m) μ lam ≤ exp (lam ^ 2 * v / 2) rw [mgf_add_const, ← exp_cgf (hExp lam), ← Real.exp_add, Real.exp_le_exp] dsimp [m] at hcgf ⊢ linarith
    Causalean.Stat.Concentration.EntropyMethod.herbst_mgf_centered_le · Causalean/Stat/Concentration/EntropyMethod/Herbst.lean:141
Self­Bounding 7 core · 2 supporting This file connects the recursive replacement-square expression in the modified logarithmic-Sobolev inequality to a pointwise replacement variance. ★ entropy_exp_le★ cgf_centered_le★ upper_tail

Replacement self-bounding functions

This file connects the recursive replacement-square expression in the modified logarithmic-Sobolev inequality to a pointwise replacement variance. It then records the entropy consequence of the standard weak self-bounding condition.

def replacementSquareSum reviewed
Causalean.Stat.Concentration.EntropyMethod

Given coordinate laws μ, a coordinate count n, and a statistic Z, the pointwise sum of conditional positive coordinate replacement squares is zero with no coordinates, while at a positive number of coordinates it integrates the head replacement square against a fresh head coordinate and adds the tail-coordinate sum.

Definition (Lean source)
parameters
X :
Type u
MeasurableSpace X
μ :
ℕ → Measure X
n :
ℕ
def
replacementSquareSum μ n :
((Fin n → X) → ℝ) → (Fin n → X) → ℝ
given by
clause 1
| 0, _, _ => 0
clause 2
| n + 1, Z, s
=> let e := piFinSuccAbove (fun _ : Fin (n + 1) => X) 0 let p := e s (∫ y, (max (Z s - Z (e.symm (y, p.2))) 0) ^ 2 ∂μ 0)
+ replacementSquareSum (fun i => μ (i + 1)) n (fun tail => Z (e.symm (p.1, tail))) p.2
Causalean.Stat.Concentration.EntropyMethod.replacementSquareSum · Causalean/Stat/Concentration/EntropyMethod/SelfBounding.lean:29
def ReplacementSquareFubiniRegularity reviewed
Causalean.Stat.Concentration.EntropyMethod

Given coordinate laws μ, a coordinate count n, a tilt lam, and a statistic Z, the Fubini regularity conditions for replacement squares recursively require integrability of the tilted head and tail replacement contributions under the head--tail product law: the zero-coordinate condition is automatic, and the positive-coordinate condition contains recursive tail regularity and integrability of the tilted head and tail contributions.

Definition (Lean source)
parameters
X :
Type u
MeasurableSpace X
μ :
ℕ → Measure X
n :
ℕ
def
ReplacementSquareFubiniRegularity μ n :
ℝ → ((Fin n → X) → ℝ) → Prop
given by
clause 1
| 0, _, _ => True
clause 2
| n + 1, lam, Z
=> let e := piFinSuccAbove (fun _ : Fin (n + 1) => X) 0 let ν := Measure.pi (fun j : Fin n => μ (j.val + 1)) (∀ x, ReplacementSquareFubiniRegularity (fun i => μ (i + 1)) n lam (fun tail => Z (e.symm (x, tail)))) ∧
Integrable (fun p : X × (Fin n → X) => exp (lam * Z (e.symm p)) * (∫ y, (max (Z (e.symm p) - Z (e.symm (y, p.2))) 0) ^ 2 ∂μ 0)) ((μ 0).prod ν) ∧
Integrable (fun p : X × (Fin n → X) => exp (lam * Z (e.symm p)) * replacementSquareSum (fun i => μ (i + 1)) n (fun tail => Z (e.symm (p.1, tail))) p.2) ((μ 0).prod ν)
Causalean.Stat.Concentration.EntropyMethod.ReplacementSquareFubiniRegularity · Causalean/Stat/Concentration/EntropyMethod/SelfBounding.lean:45
structure ReplacementSelfBounding reviewed
Causalean.Stat.Concentration.EntropyMethod

Given coordinate laws μ, a coordinate count n, a statistic Z, and coefficients a and b, weak replacement self-bounding means that the sum of positive coordinate replacement squares is pointwise at most a Z + b.

Definition (Lean source)
parameters
X :
Type u
MeasurableSpace X
μ :
ℕ → Measure X
n :
ℕ
Z :
(Fin n → X) → ℝ
a b :
ℝ
assumes
bound :
∀ s, replacementSquareSum μ n Z s ≤ a * Z s + b
Causalean.Stat.Concentration.EntropyMethod.ReplacementSelfBounding · Causalean/Stat/Concentration/EntropyMethod/SelfBounding.lean:70
structure ReplacementSelfBoundingCGFRegularity reviewed
Causalean.Stat.Concentration.EntropyMethod

For coordinate laws μ, a coordinate count n, a statistic Z, and self-bounding coefficients a,b, cumulant-generating-function regularity consists of exponential integrability at every real tilt, finite-product entropy regularity, modified logarithmic-Sobolev regularity, replacement Fubini regularity, and integrability of both sides of the tilted replacement comparison at every positive tilt below the linear pole.

Definition (Lean source)
parameters
X :
Type u
MeasurableSpace X
μ :
ℕ → Measure X
n :
ℕ
Z :
(Fin n → X) → ℝ
a b :
ℝ
assumes
exp_integrable :
∀ t : ℝ, Integrable (fun s => exp (t * Z s)) (Measure.pi (fun i : Fin n => μ i.val))
tensorization :
∀ t
if
0 < t
and
a * t < 1
then
FiniteTensorizationRegularity μ n (fun s => exp (t * Z s))
modifiedLogSobolev :
∀ t
if
0 < t
and
a * t < 1
then
ModifiedLogSobolevRegularity μ n t Z
replacementFubini :
∀ t
if
0 < t
and
a * t < 1
then
ReplacementSquareFubiniRegularity μ n t Z
left_integrable :
∀ t
if
0 < t
and
a * t < 1
then
Integrable (fun s => exp (t * Z s) * replacementSquareSum μ n Z s) (Measure.pi (fun i : Fin n => μ i.val))
right_integrable :
∀ t
if
0 < t
and
a * t < 1
then
Integrable (fun s => exp (t * Z s) * (a * Z s + b)) (Measure.pi (fun i : Fin n => μ i.val))
Causalean.Stat.Concentration.EntropyMethod.ReplacementSelfBoundingCGFRegularity · Causalean/Stat/Concentration/EntropyMethod/SelfBounding.lean:88
theorem entropy_exp_le reviewed
Causalean.Stat.Concentration.EntropyMethod.ReplacementSelfBounding

If the coordinate laws μ are probability laws, the tilt lam is nonnegative, the product has n coordinates, the statistic is Z, the self-bounding coefficients are a and b, the tensorization and replacement regularity conditions hold, the replacement Fubini conditions hold, the statistic is weakly self-bounding, and both tilted comparison integrands are integrable, then the entropy of the exponential tilt is at most lam² times the tilted expectation of a Z + b.

Formal statement
hypotheses
X :
Type u
MeasurableSpace X
μ :
ℕ → Measure X
∀ i, IsProbabilityMeasure (μ i)
lam :
ℝ
hlam :
0 ≤ lam
n :
ℕ
Z :
(Fin n → X) → ℝ
a b :
ℝ
hTensor :
FiniteTensorizationRegularity μ n (fun x => exp (lam * Z x))
hModified :
ModifiedLogSobolevRegularity μ n lam Z
hFubini :
ReplacementSquareFubiniRegularity μ n lam Z
hSelf :
ReplacementSelfBounding μ n Z a b
hLeftInt :
Integrable (fun s => exp (lam * Z s) * replacementSquareSum μ n Z s) (Measure.pi (fun i : Fin n => μ i.val))
hRightInt :
Integrable (fun s => exp (lam * Z s) * (a * Z s + b)) (Measure.pi (fun i : Fin n => μ i.val))
conclusion
entropy (Measure.pi (fun i : Fin n => μ i.val)) (fun s => exp (lam * Z s))
≤ lam ^ 2 * ∫ s, exp (lam * Z s) * (a * Z s + b) ∂Measure.pi (fun i : Fin n => μ i.val)
Proof (Lean source)
theorem ReplacementSelfBounding.entropy_exp_le {X : Type u} [MeasurableSpace X] (μ : ℕ → Measure X) [hprob : ∀ i, IsProbabilityMeasure (μ i)] {lam : ℝ} (hlam : 0 ≤ lam) (n : ℕ) (Z : (Fin n → X) → ℝ) {a b : ℝ} (hTensor : FiniteTensorizationRegularity μ n (fun x => exp (lam * Z x))) (hModified : ModifiedLogSobolevRegularity μ n lam Z) (hFubini : ReplacementSquareFubiniRegularity μ n lam Z) (hSelf : ReplacementSelfBounding μ n Z a b) (hLeftInt : Integrable (fun s => exp (lam * Z s) * replacementSquareSum μ n Z s) (Measure.pi (fun i : Fin n => μ i.val))) (hRightInt : Integrable (fun s => exp (lam * Z s) * (a * Z s + b)) (Measure.pi (fun i : Fin n => μ i.val))) : entropy (Measure.pi (fun i : Fin n => μ i.val)) (fun s => exp (lam * Z s)) ≤ lam ^ 2 * ∫ s, exp (lam * Z s) * (a * Z s + b) ∂Measure.pi (fun i : Fin n => μ i.val) := by have hmlsi := modifiedLogSobolev_pi μ hlam n Z hTensor hModified rw [exponentialReplacementSquareSum_eq_integral μ n lam Z hModified hFubini] at hmlsi have hpoint : (fun s => exp (lam * Z s) * replacementSquareSum μ n Z s) ≤ᵐ[ Measure.pi (fun i : Fin n => μ i.val)] fun s => exp (lam * Z s) * (a * Z s + b) := by filter_upwards with s exact mul_le_mul_of_nonneg_left (hSelf.bound s) (Real.exp_pos _).le have hint := integral_mono_ae hLeftInt hRightInt hpoint exact hmlsi.trans (mul_le_mul_of_nonneg_left hint (sq_nonneg lam))
Causalean.Stat.Concentration.EntropyMethod.ReplacementSelfBounding.entropy_exp_le · Causalean/Stat/Concentration/EntropyMethod/SelfBounding.lean:249 · uses FiniteTensorizationRegularity , ModifiedLogSobolevRegularity , ReplacementSelfBounding , ReplacementSquareFubiniRegularity , entropy , replacementSquareSum
theorem cgf_centered_le reviewed
Causalean.Stat.Concentration.EntropyMethod.ReplacementSelfBounding

If the coordinate laws μ are probability laws, the product has n coordinates, the statistic is Z, the self-bounding coefficients a,b are nonnegative, the statistic is weakly replacement self-bounding, and the exponential-tilt regularity conditions hold, then at a nonnegative tilt lam below the linear pole, the centered cumulant-generating function is at most (a E[Z] + b) lam² / (1 - a lam).

Formal statement
hypotheses
X :
Type u
MeasurableSpace X
μ :
ℕ → Measure X
∀ i, IsProbabilityMeasure (μ i)
n :
ℕ
Z :
(Fin n → X) → ℝ
a b :
ℝ
ha :
0 ≤ a
hb :
0 ≤ b
hSelf :
ReplacementSelfBounding μ n Z a b
hReg :
ReplacementSelfBoundingCGFRegularity μ n Z a b
lam :
ℝ
hlam0 :
0 ≤ lam
hlam :
a * lam < 1
conclusion
cgf Z (Measure.pi (fun i : Fin n => μ i.val)) lam
- lam * (∫ s, Z s ∂Measure.pi (fun i : Fin n => μ i.val))
≤ (a * (∫ s, Z s ∂Measure.pi (fun i : Fin n => μ i.val)) + b) * lam ^ 2 / (1 - a * lam)
Proof (Lean source)
theorem ReplacementSelfBounding.cgf_centered_le {X : Type u} [MeasurableSpace X] (μ : ℕ → Measure X) [hprob : ∀ i, IsProbabilityMeasure (μ i)] (n : ℕ) (Z : (Fin n → X) → ℝ) {a b : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) (hSelf : ReplacementSelfBounding μ n Z a b) (hReg : ReplacementSelfBoundingCGFRegularity μ n Z a b) {lam : ℝ} (hlam0 : 0 ≤ lam) (hlam : a * lam < 1) : cgf Z (Measure.pi (fun i : Fin n => μ i.val)) lam - lam * (∫ s, Z s ∂Measure.pi (fun i : Fin n => μ i.val)) ≤ (a * (∫ s, Z s ∂Measure.pi (fun i : Fin n => μ i.val)) + b) * lam ^ 2 / (1 - a * lam) := by let ν : Measure (Fin n → X) := Measure.pi (fun i : Fin n => μ i.val) have hset : interior (integrableExpSet Z ν) = univ := by rw [interior_eq_univ] ext t simpa [ν, integrableExpSet] using hReg.exp_integrable t have hdiff : Differentiable ℝ (cgf Z ν) := by intro t exact (analyticAt_cgf (by simp [hset])).differentiableAt have hderiv0 : deriv (cgf Z ν) 0 = ∫ s, Z s ∂ν := by simpa using deriv_cgf_zero (X := Z) (μ := ν) (by simp [hset]) have hdifferential : ∀ t, 0 < t → a * t < 1 → t * (1 - a * t) * deriv (cgf Z ν) t - cgf Z ν t ≤ b * t ^ 2 := by intro t ht hta have hmem : t ∈ interior (integrableExpSet Z ν) := by simp [hset] have hMpos : 0 < mgf Z ν t := mgf_pos (by simpa [ν] using hReg.exp_integrable t) have hidentity : entropy ν (fun s => exp (t * Z s)) = mgf Z ν t * (t * deriv (cgf Z ν) t - cgf Z ν t) := by rw [entropy] simp_rw [Real.log_exp] rw [show (∫ s, exp (t * Z s) * (t * Z s) ∂ν) = t * ∫ s, Z s * exp (t * Z s) ∂ν by rw [← integral_const_mul] congr with s ring] rw [show (∫ s, exp (t * Z s) ∂ν) = mgf Z ν t by rfl] rw [deriv_cgf hmem] dsimp [cgf] field_simp [hMpos.ne'] have hweighted : (∫ s, exp (t * Z s) * (a * Z s + b) ∂ν) = mgf Z ν t * (a * deriv (cgf Z ν) t + b) := by exact integral_exp_mul_affine_eq_mgf_mul (by intro u; simpa [ν] using hReg.exp_integrable u) have hEnt := hSelf.entropy_exp_le μ ht.le n Z (hReg.tensorization t ht hta) (hReg.modifiedLogSobolev t ht hta) (hReg.replacementFubini t ht hta) (hReg.left_integrable t ht hta) (hReg.right_integrable t ht hta) change entropy ν (fun s => exp (t * Z s)) ≤ t ^ 2 * ∫ s, exp (t * Z s) * (a * Z s + b) ∂ν at hEnt rw [hidentity, hweighted] at hEnt have hbase : t * deriv (cgf Z ν) t - cgf Z ν t ≤ t ^ 2 * (a * deriv (cgf Z ν) t + b) := by apply (mul_le_mul_iff_of_pos_left hMpos).mp simpa [mul_assoc, mul_left_comm, mul_comm] using hEnt nlinarith have hcalc := centered_le_of_differential_inequality (hdiff 0) (fun t _ _ => hdiff t) cgf_zero ha hb hdifferential hlam0 hlam simpa [ν, hderiv0] using hcalc
Causalean.Stat.Concentration.EntropyMethod.ReplacementSelfBounding.cgf_centered_le · Causalean/Stat/Concentration/EntropyMethod/SelfBounding.lean:319 · uses ReplacementSelfBounding , ReplacementSelfBoundingCGFRegularity
theorem upper_tail reviewed
Causalean.Stat.Concentration.EntropyMethod.ReplacementSelfBounding

If the coordinate laws μ are probability laws, the product has n coordinates, the statistic is Z, the self-bounding coefficients a,b are nonnegative, the statistic is weakly replacement self-bounding, the exponential-tilt regularity conditions hold, and the variance factor a E[Z] + b is positive, then every positive deviation t satisfies the Bernstein upper tail bound with exponent -t² / (4(a E[Z] + b) + 2at).

Formal statement
hypotheses
X :
Type u
MeasurableSpace X
μ :
ℕ → Measure X
∀ i, IsProbabilityMeasure (μ i)
n :
ℕ
Z :
(Fin n → X) → ℝ
a b :
ℝ
ha :
0 ≤ a
hb :
0 ≤ b
hSelf :
ReplacementSelfBounding μ n Z a b
hReg :
ReplacementSelfBoundingCGFRegularity μ n Z a b
hscale :
0 < a * (∫ s, Z s ∂Measure.pi (fun i : Fin n => μ i.val)) + b
t :
ℝ
ht :
0 < t
conclusion
(Measure.pi (fun i : Fin n => μ i.val)).real {s | t ≤ Z s - ∫ x, Z x ∂Measure.pi (fun i : Fin n => μ i.val)}
≤ exp (-t ^ 2 / (4 * (a * (∫ s, Z s ∂Measure.pi (fun i : Fin n => μ i.val)) + b) + 2 * a * t))
Proof (Lean source)
theorem ReplacementSelfBounding.upper_tail {X : Type u} [MeasurableSpace X] (μ : ℕ → Measure X) [hprob : ∀ i, IsProbabilityMeasure (μ i)] (n : ℕ) (Z : (Fin n → X) → ℝ) {a b : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) (hSelf : ReplacementSelfBounding μ n Z a b) (hReg : ReplacementSelfBoundingCGFRegularity μ n Z a b) (hscale : 0 < a * (∫ s, Z s ∂Measure.pi (fun i : Fin n => μ i.val)) + b) {t : ℝ} (ht : 0 < t) : (Measure.pi (fun i : Fin n => μ i.val)).real {s | t ≤ Z s - ∫ x, Z x ∂Measure.pi (fun i : Fin n => μ i.val)} ≤ exp (-t ^ 2 / (4 * (a * (∫ s, Z s ∂Measure.pi (fun i : Fin n => μ i.val)) + b) + 2 * a * t)) := by let ν : Measure (Fin n → X) := Measure.pi (fun i : Fin n => μ i.val) let m := ∫ s, Z s ∂ν let c := a * m + b let lam := t / (2 * c + a * t) have hc : 0 < c := by simpa [c, m, ν] using hscale have hden : 0 < 2 * c + a * t := by positivity have hlam0 : 0 ≤ lam := (div_pos ht hden).le have hlam : a * lam < 1 := by rw [show lam = t / (2 * c + a * t) by rfl, ← mul_div_assoc] rw [div_lt_iff₀ hden] nlinarith have hint : Integrable (fun s => exp (lam * (Z s - m))) ν := by have h := (hReg.exp_integrable lam).mul_const (exp (-lam * m)) change Integrable (fun s => exp (lam * (Z s - m))) (Measure.pi (fun i : Fin n => μ i.val)) convert h using 1 funext s rw [← Real.exp_add] congr 1 ring have hchernoff := measure_ge_le_exp_mul_mgf t hlam0 hint have hmgf : mgf (fun s => Z s - m) ν lam ≤ exp (c * lam ^ 2 / (1 - a * lam)) := by simpa [c, m, ν] using hSelf.mgf_centered_le μ n Z ha hb hReg hlam0 hlam calc ν.real {s | t ≤ Z s - m} ≤ exp (-lam * t) * mgf (fun s => Z s - m) ν lam := hchernoff _ ≤ exp (-lam * t) * exp (c * lam ^ 2 / (1 - a * lam)) := mul_le_mul_of_nonneg_left hmgf (Real.exp_pos _).le _ = exp (-t ^ 2 / (4 * c + 2 * a * t)) := by rw [← Real.exp_add] congr 1 dsimp [lam] have hpole : 1 - a * (t / (2 * c + a * t)) ≠ 0 := ne_of_gt (sub_pos.mpr hlam) field_simp [hden.ne', hpole] ring
Causalean.Stat.Concentration.EntropyMethod.ReplacementSelfBounding.upper_tail · Causalean/Stat/Concentration/EntropyMethod/SelfBounding.lean:418 · uses ReplacementSelfBounding , ReplacementSelfBoundingCGFRegularity
2 supporting declarations (lemmas, instances)
  • exponentialReplacementSquareSum_eq_integral theorem — If the coordinate laws μ are probability laws, the product has n coordinates, the tilt is lam, the statistic is Z, the modified logarithmic-Sobolev integrability conditions hold, and the additional Fubini conditions hold, then the recursive tilted replacement-square sum equals the product expectation of the exponential tilt times the pointwise replacement-square sum.
    hypotheses
    X :
    Type u
    MeasurableSpace X
    μ :
    ℕ → Measure X
    ∀ i, IsProbabilityMeasure (μ i)
    n :
    ℕ
    lam :
    ℝ
    Z :
    (Fin n → X) → ℝ
    hModified :
    ModifiedLogSobolevRegularity μ n lam Z
    hFubini :
    ReplacementSquareFubiniRegularity μ n lam Z
    conclusion
    exponentialReplacementSquareSum μ n lam Z
    = ∫ s, exp (lam * Z s) * replacementSquareSum μ n Z s ∂Measure.pi (fun i : Fin n => μ i.val)
    Proof (Lean source)
    theorem exponentialReplacementSquareSum_eq_integral {X : Type u} [MeasurableSpace X] (μ : ℕ → Measure X) [hprob : ∀ i, IsProbabilityMeasure (μ i)] (n : ℕ) (lam : ℝ) (Z : (Fin n → X) → ℝ) (hModified : ModifiedLogSobolevRegularity μ n lam Z) (hFubini : ReplacementSquareFubiniRegularity μ n lam Z) : exponentialReplacementSquareSum μ n lam Z = ∫ s, exp (lam * Z s) * replacementSquareSum μ n Z s ∂Measure.pi (fun i : Fin n => μ i.val) := by induction n generalizing μ with | zero => simp [exponentialReplacementSquareSum, replacementSquareSum] | succ n ih => let e := piFinSuccAbove (fun _ : Fin (n + 1) => X) 0 let ν : Measure (Fin n → X) := Measure.pi (fun j : Fin n => μ (j.val + 1)) change (∀ tail, ReplacementEntropyIntegrable (μ 0) lam (fun x => Z (e.symm (x, tail)))) ∧ (∀ x, ModifiedLogSobolevRegularity (fun i => μ (i + 1)) n lam (fun tail => Z (e.symm (x, tail)))) ∧ Integrable (fun tail => entropy (μ 0) (fun x => exp (lam * Z (e.symm (x, tail))))) ν ∧ Integrable (fun tail => ∫ p : X × X, exp (lam * Z (e.symm (p.1, tail))) * (max (Z (e.symm (p.1, tail)) - Z (e.symm (p.2, tail))) 0) ^ 2 ∂(μ 0).prod (μ 0)) ν ∧ Integrable (fun x => coordinateEntropySum (fun i => μ (i + 1)) n (fun tail => exp (lam * Z (e.symm (x, tail))))) (μ 0) ∧ Integrable (fun x => exponentialReplacementSquareSum (fun i => μ (i + 1)) n lam (fun tail => Z (e.symm (x, tail)))) (μ 0) at hModified rcases hModified with ⟨hhead, htailModified, _, _, _, _⟩ change (∀ x, ReplacementSquareFubiniRegularity (fun i => μ (i + 1)) n lam (fun tail => Z (e.symm (x, tail)))) ∧ Integrable (fun p : X × (Fin n → X) => exp (lam * Z (e.symm p)) * (∫ y, (max (Z (e.symm p) - Z (e.symm (y, p.2))) 0) ^ 2 ∂μ 0)) ((μ 0).prod ν) ∧ Integrable (fun p : X × (Fin n → X) => exp (lam * Z (e.symm p)) * replacementSquareSum (fun i => μ (i + 1)) n (fun tail => Z (e.symm (p.1, tail))) p.2) ((μ 0).prod ν) at hFubini rcases hFubini with ⟨htailFubini, hHeadInt, hTailInt⟩ let headPart : X × (Fin n → X) → ℝ := fun p => exp (lam * Z (e.symm p)) * (∫ y, (max (Z (e.symm p) - Z (e.symm (y, p.2))) 0) ^ 2 ∂μ 0) let tailPart : X × (Fin n → X) → ℝ := fun p => exp (lam * Z (e.symm p)) * replacementSquareSum (fun i => μ (i + 1)) n (fun tail => Z (e.symm (p.1, tail))) p.2 have hHead : (∫ tail, ∫ p : X × X, exp (lam * Z (e.symm (p.1, tail))) * (max (Z (e.symm (p.1, tail)) - Z (e.symm (p.2, tail))) 0) ^ 2 ∂(μ 0).prod (μ 0) ∂ν) = ∫ p, headPart p ∂((μ 0).prod ν) := by calc _ = ∫ tail, ∫ x, exp (lam * Z (e.symm (x, tail))) * (∫ y, (max (Z (e.symm (x, tail)) - Z (e.symm (y, tail))) 0) ^ 2 ∂μ 0) ∂μ 0 ∂ν := by apply integral_congr_ae filter_upwards with tail rw [integral_prod _ (hhead tail).hplus] apply integral_congr_ae filter_upwards with x rw [← integral_const_mul] _ = ∫ p, headPart p ∂((μ 0).prod ν) := by simpa [headPart] using (integral_prod_symm headPart hHeadInt).symm have hTail : (∫ x, exponentialReplacementSquareSum (fun i => μ (i + 1)) n lam (fun tail => Z (e.symm (x, tail))) ∂μ 0) = ∫ p, tailPart p ∂((μ 0).prod ν) := by calc _ = ∫ x, ∫ tail, exp (lam * Z (e.symm (x, tail))) * replacementSquareSum (fun i => μ (i + 1)) n (fun tail' => Z (e.symm (x, tail'))) tail ∂ν ∂μ 0 := by apply integral_congr_ae filter_upwards with x exact ih (fun i => μ (i + 1)) (fun tail => Z (e.symm (x, tail))) (htailModified x) (htailFubini x) _ = ∫ p, tailPart p ∂((μ 0).prod ν) := by simpa [tailPart] using (integral_prod tailPart hTailInt).symm have hsplit : MeasurePreserving e (Measure.pi (fun i : Fin (n + 1) => μ i.val)) ((μ 0).prod ν) := by simpa [e, ν] using (MeasureTheory.measurePreserving_piFinSuccAbove (μ := fun i : Fin (n + 1) => μ i.val) 0) have hProduct : (∫ p, headPart p + tailPart p ∂((μ 0).prod ν)) = ∫ s, exp (lam * Z s) * replacementSquareSum μ (n + 1) Z s ∂Measure.pi (fun i : Fin (n + 1) => μ i.val) := by let G : X × (Fin n → X) → ℝ := fun p => exp (lam * Z (e.symm p)) * replacementSquareSum μ (n + 1) Z (e.symm p) have hcomp : G ∘ e = fun s => exp (lam * Z s) * replacementSquareSum μ (n + 1) Z s := by funext s dsimp [G] rw [e.symm_apply_apply] have htransport := hsplit.integral_comp' G have hpoint : G = fun p => headPart p + tailPart p := by funext p dsimp [G, headPart, tailPart, replacementSquareSum] rw [e.apply_symm_apply] ring calc (∫ p, headPart p + tailPart p ∂((μ 0).prod ν)) = ∫ p, G p ∂((μ 0).prod ν) := by apply integral_congr_ae exact ae_of_all _ (congrFun hpoint.symm) _ = ∫ s, G (e s) ∂Measure.pi (fun i : Fin (n + 1) => μ i.val) := htransport.symm _ = ∫ s, exp (lam * Z s) * replacementSquareSum μ (n + 1) Z s ∂Measure.pi (fun i : Fin (n + 1) => μ i.val) := by apply integral_congr_ae exact ae_of_all _ (congrFun hcomp) change (∫ tail, ∫ p : X × X, exp (lam * Z (e.symm (p.1, tail))) * (max (Z (e.symm (p.1, tail)) - Z (e.symm (p.2, tail))) 0) ^ 2 ∂(μ 0).prod (μ 0) ∂ν) + (∫ x, exponentialReplacementSquareSum (fun i => μ (i + 1)) n lam (fun tail => Z (e.symm (x, tail))) ∂μ 0) = _ rw [hHead, hTail, ← integral_add hHeadInt hTailInt, hProduct]
    Causalean.Stat.Concentration.EntropyMethod.exponentialReplacementSquareSum_eq_integral · Causalean/Stat/Concentration/EntropyMethod/SelfBounding.lean:113
  • mgf_centered_le theorem — If the coordinate laws μ are probability laws, the product has n coordinates, the statistic is Z, the self-bounding coefficients a,b are nonnegative, the statistic is weakly replacement self-bounding, and the exponential-tilt regularity conditions hold, then at a nonnegative tilt lam below the linear pole, the centered moment-generating function is at most the exponential of (a E[Z] + b) lam² / (1 - a lam).
    hypotheses
    X :
    Type u
    MeasurableSpace X
    μ :
    ℕ → Measure X
    ∀ i, IsProbabilityMeasure (μ i)
    n :
    ℕ
    Z :
    (Fin n → X) → ℝ
    a b :
    ℝ
    ha :
    0 ≤ a
    hb :
    0 ≤ b
    hSelf :
    ReplacementSelfBounding μ n Z a b
    hReg :
    ReplacementSelfBoundingCGFRegularity μ n Z a b
    lam :
    ℝ
    hlam0 :
    0 ≤ lam
    hlam :
    a * lam < 1
    conclusion
    mgf (fun s => Z s - ∫ x, Z x ∂Measure.pi (fun i : Fin n => μ i.val)) (Measure.pi (fun i : Fin n => μ i.val)) lam
    ≤ exp ((a * (∫ s, Z s ∂Measure.pi (fun i : Fin n => μ i.val)) + b) * lam ^ 2 / (1 - a * lam))
    Proof (Lean source)
    theorem ReplacementSelfBounding.mgf_centered_le {X : Type u} [MeasurableSpace X] (μ : ℕ → Measure X) [hprob : ∀ i, IsProbabilityMeasure (μ i)] (n : ℕ) (Z : (Fin n → X) → ℝ) {a b : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) (hSelf : ReplacementSelfBounding μ n Z a b) (hReg : ReplacementSelfBoundingCGFRegularity μ n Z a b) {lam : ℝ} (hlam0 : 0 ≤ lam) (hlam : a * lam < 1) : mgf (fun s => Z s - ∫ x, Z x ∂Measure.pi (fun i : Fin n => μ i.val)) (Measure.pi (fun i : Fin n => μ i.val)) lam ≤ exp ((a * (∫ s, Z s ∂Measure.pi (fun i : Fin n => μ i.val)) + b) * lam ^ 2 / (1 - a * lam)) := by let ν : Measure (Fin n → X) := Measure.pi (fun i : Fin n => μ i.val) let m := ∫ s, Z s ∂ν have hcgf := hSelf.cgf_centered_le μ n Z ha hb hReg hlam0 hlam change mgf (fun s => Z s + -m) ν lam ≤ exp ((a * m + b) * lam ^ 2 / (1 - a * lam)) rw [mgf_add_const, ← exp_cgf (by simpa [ν] using hReg.exp_integrable lam)] rw [← Real.exp_add, Real.exp_le_exp] dsimp [m, ν] at hcgf ⊢ linarith
    Causalean.Stat.Concentration.EntropyMethod.ReplacementSelfBounding.mgf_centered_le · Causalean/Stat/Concentration/EntropyMethod/SelfBounding.lean:390