Hanson-Wright Inequality

This file formalizes a finite-dimensional Hanson-Wright tail bound for real quadratic forms. The public theorem proves the required Hanson-Wright MGF certificate from independent sub-Gaussian coordinates, using local diagonal/off-diagonal MGF infrastructure and then optimizing the resulting two-scale Chernoff bound.

Main definitions

• HansonWright.quadraticForm: the deterministic quadratic form xᵀ A x.
• HansonWright.centeredQuadraticForm: the centered random quadratic form.
• HansonWright.frobeniusNorm: the Frobenius norm of a finite real matrix.
• HansonWright.operatorNorm: the ℓ² operator norm of a finite real matrix.
• HansonWright.entrywiseL1Norm: the entrywise ℓ¹ norm of a finite real matrix.
• HansonWright.HasHansonWrightMGF: the local quadratic CGF hypothesis used internally by the tail optimization step.

Main results

• HansonWright.hasSubgaussianMGF_of_abs_le_of_integral_eq_zero: local symmetric bounded-variable MGF estimate.
• HansonWright.hasHansonWrightMGF_of_subgaussian: a proved Hanson-Wright MGF certificate for independent sub-Gaussian coordinates.
• HansonWright.hasHansonWrightMGF_of_bounded: a proved Hanson-Wright MGF certificate for bounded coordinates.
• HansonWright.hanson_wright_inequality: Hanson-Wright tail bound after deriving the MGF certificate from independent sub-Gaussian coordinates.
• HansonWright.hanson_wright_inequality_hdp: HDP-style Hanson-Wright tail bound using the maximum coordinate least global-MGF sub-Gaussian scale.

theorem LeanPool.HansonWright.mgf_innerSL_stdGaussian {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (v : E) (t : ℝ) : ProbabilityTheory.mgf (fun (x : E) => inner ℝ v x) (ProbabilityTheory.stdGaussian E) t = Real.exp (‖v‖ ^ 2 * t ^ 2 / 2)

theorem LeanPool.HansonWright.integrable_exp_innerSL_stdGaussian {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (v : E) (t : ℝ) : MeasureTheory.Integrable (fun (x : E) => Real.exp (t * inner ℝ v x)) (ProbabilityTheory.stdGaussian E)

theorem LeanPool.HansonWright.integral_exp_innerSL_stdGaussian {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (v : E) (t : ℝ) : ∫ (x : E), Real.exp (t * inner ℝ v x) ∂ProbabilityTheory.stdGaussian E = Real.exp (‖v‖ ^ 2 * t ^ 2 / 2)

theorem LeanPool.HansonWright.hasSubgaussianMGF_id_gaussianReal_zero_one : ProbabilityTheory.HasSubgaussianMGF id 1 (ProbabilityTheory.gaussianReal 0 1)

theorem LeanPool.HansonWright.symmetric_inner_apply_eq_sum_eigenvalues_repr {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] (T : E →ₗ[ℝ] E) (hT : T.IsSymmetric) (x : E) : inner ℝ (T x) x = ∑ i : Fin (Module.finrank ℝ E), hT.eigenvalues ⋯ i * ((hT.eigenvectorBasis ⋯).repr x).ofLp i ^ 2

theorem LeanPool.HansonWright.orthonormalBasis_repr_sum_smul {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (b : OrthonormalBasis (Fin (Module.finrank ℝ E)) ℝ E) (z : Fin (Module.finrank ℝ E) → ℝ) (i : Fin (Module.finrank ℝ E)) : (b.repr (∑ i : Fin (Module.finrank ℝ E), z i • b i)).ofLp i = z i

def LeanPool.HansonWright.quadraticForm {n : ℕ} (A : Matrix (Fin n) (Fin n) ℝ) (x : Fin n → ℝ) : ℝ

The deterministic quadratic form xᵀ A x.

Equations

• LeanPool.HansonWright.quadraticForm A x = ∑ i : Fin n, ∑ j : Fin n, A i j * x i * x j

def LeanPool.HansonWright.randomQuadraticForm {Ω : Type u_1} {n : ℕ} (A : Matrix (Fin n) (Fin n) ℝ) (X : Fin n → Ω → ℝ) : Ω → ℝ

The random quadratic form associated to a random vector X.

Equations

• LeanPool.HansonWright.randomQuadraticForm A X ω = LeanPool.HansonWright.quadraticForm A fun (i : Fin n) => X i ω

def LeanPool.HansonWright.randomVector {Ω : Type u_1} {n : ℕ} (X : Fin n → Ω → ℝ) : Ω → EuclideanSpace ℝ (Fin n)

The coordinate random vector as an element of Euclidean space.

Equations

• LeanPool.HansonWright.randomVector X ω = WithLp.toLp 2 fun (i : Fin n) => X i ω

@[simp]

theorem LeanPool.HansonWright.randomVector_apply {Ω : Type u_1} {n : ℕ} (X : Fin n → Ω → ℝ) (ω : Ω) (i : Fin n) : (randomVector X ω).ofLp i = X i ω

theorem LeanPool.HansonWright.randomVector_aemeasurable {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {n : ℕ} {X : Fin n → Ω → ℝ} (hX_meas : ∀ (i : Fin n), AEMeasurable (X i) μ) : AEMeasurable (randomVector X) μ

theorem LeanPool.HansonWright.measure_map_prod_map_of_aemeasurable {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] [MeasurableSpace δ] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite μ] [MeasureTheory.SFinite ν] {f : α → γ} {g : β → δ} (hf : AEMeasurable f μ) (hg : AEMeasurable g ν) : (MeasureTheory.Measure.map f μ).prod (MeasureTheory.Measure.map g ν) = MeasureTheory.Measure.map (fun (p : α × β) => (f p.1, g p.2)) (μ.prod ν)

noncomputable def LeanPool.HansonWright.centeredQuadraticForm {Ω : Type u_1} [MeasurableSpace Ω] {n : ℕ} (μ : MeasureTheory.Measure Ω) (A : Matrix (Fin n) (Fin n) ℝ) (X : Fin n → Ω → ℝ) : Ω → ℝ

The centered random quadratic form Xᵀ A X - E Xᵀ A X.

Equations

• LeanPool.HansonWright.centeredQuadraticForm μ A X ω = LeanPool.HansonWright.randomQuadraticForm A X ω - ∫ (ω : Ω), LeanPool.HansonWright.randomQuadraticForm A X ω ∂μ

def LeanPool.HansonWright.frobeniusNormSq {n : ℕ} (A : Matrix (Fin n) (Fin n) ℝ) : ℝ

The squared Frobenius norm of a finite real matrix.

Equations

• LeanPool.HansonWright.frobeniusNormSq A = ∑ i : Fin n, ∑ j : Fin n, A i j ^ 2

noncomputable def LeanPool.HansonWright.frobeniusNorm {n : ℕ} (A : Matrix (Fin n) (Fin n) ℝ) : ℝ

The Frobenius norm of a finite real matrix.

Equations

• LeanPool.HansonWright.frobeniusNorm A = √(LeanPool.HansonWright.frobeniusNormSq A)

noncomputable def LeanPool.HansonWright.operatorNorm {n : ℕ} (A : Matrix (Fin n) (Fin n) ℝ) : ℝ

The ℓ² operator norm of a finite real matrix.

Equations

• LeanPool.HansonWright.operatorNorm A = ‖Matrix.toEuclideanCLM A‖

def LeanPool.HansonWright.entrywiseL1Norm {n : ℕ} (A : Matrix (Fin n) (Fin n) ℝ) : ℝ

The entrywise ℓ¹ norm of a finite real matrix.

Equations

• LeanPool.HansonWright.entrywiseL1Norm A = ∑ i : Fin n, ∑ j : Fin n, |A i j|

def LeanPool.HansonWright.offDiagonalMatrix {n : ℕ} (A : Matrix (Fin n) (Fin n) ℝ) : Matrix (Fin n) (Fin n) ℝ

The matrix obtained by deleting the diagonal entries.

Equations

• LeanPool.HansonWright.offDiagonalMatrix A i j = if i = j then 0 else A i j

def LeanPool.HansonWright.cutMatrix {n : ℕ} (A : Matrix (Fin n) (Fin n) ℝ) (s : Finset (Fin n)) : Matrix (Fin n) (Fin n) ℝ

The matrix keeping only rows in s and columns outside s.

Equations

• LeanPool.HansonWright.cutMatrix A s i j = if i ∈ s ∧ j ∉ s then A i j else 0

def LeanPool.HansonWright.coordinateMask {n : ℕ} (s : Finset (Fin n)) (x : EuclideanSpace ℝ (Fin n)) : EuclideanSpace ℝ (Fin n)

Coordinate projection onto a finite set of coordinates.

Equations

• LeanPool.HansonWright.coordinateMask s x = WithLp.toLp 2 fun (i : Fin n) => if i ∈ s then x.ofLp i else 0

@[simp]

theorem LeanPool.HansonWright.coordinateMask_apply {n : ℕ} (s : Finset (Fin n)) (x : EuclideanSpace ℝ (Fin n)) (i : Fin n) : (coordinateMask s x).ofLp i = if i ∈ s then x.ofLp i else 0

def LeanPool.HansonWright.subtypeMask {n : ℕ} (s : Finset (Fin n)) (x : ↥s → ℝ) : EuclideanSpace ℝ (Fin n)

Embed a tuple indexed by a finite set into Euclidean space, filling other coordinates by zero.

Equations

• LeanPool.HansonWright.subtypeMask s x = WithLp.toLp 2 fun (i : Fin n) => if h : i ∈ s then x ⟨i, h⟩ else 0

@[simp]

theorem LeanPool.HansonWright.subtypeMask_apply {n : ℕ} (s : Finset (Fin n)) (x : ↥s → ℝ) (i : Fin n) : (subtypeMask s x).ofLp i = if h : i ∈ s then x ⟨i, h⟩ else 0

theorem LeanPool.HansonWright.measurable_subtypeMask {n : ℕ} (s : Finset (Fin n)) : Measurable (subtypeMask s)

theorem LeanPool.HansonWright.subtypeMask_subtype_randomVector {Ω : Type u_1} {n : ℕ} (s : Finset (Fin n)) (X : Fin n → Ω → ℝ) : (fun (ω : Ω) => subtypeMask s fun (i : ↥s) => X (↑i) ω) = fun (ω : Ω) => coordinateMask s (randomVector X ω)

theorem LeanPool.HansonWright.coordinateMask_aemeasurable {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {n : ℕ} (s : Finset (Fin n)) {X : Fin n → Ω → ℝ} (hX_meas : ∀ (i : Fin n), AEMeasurable (X i) μ) : AEMeasurable (fun (ω : Ω) => coordinateMask s (randomVector X ω)) μ

theorem LeanPool.HansonWright.coordinateMask_indepFun_compl {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {n : ℕ} {X : Fin n → Ω → ℝ} (h_indep : ProbabilityTheory.iIndepFun X μ) (hX_meas : ∀ (i : Fin n), AEMeasurable (X i) μ) (s : Finset (Fin n)) : ProbabilityTheory.IndepFun (fun (ω : Ω) => coordinateMask (Finset.univ \ s) (randomVector X ω)) (fun (ω : Ω) => coordinateMask s (randomVector X ω)) μ

theorem LeanPool.HansonWright.frobeniusNormSq_nonneg {n : ℕ} (A : Matrix (Fin n) (Fin n) ℝ) : 0 ≤ frobeniusNormSq A

theorem LeanPool.HansonWright.frobeniusNorm_nonneg {n : ℕ} (A : Matrix (Fin n) (Fin n) ℝ) : 0 ≤ frobeniusNorm A

theorem LeanPool.HansonWright.operatorNorm_nonneg {n : ℕ} (A : Matrix (Fin n) (Fin n) ℝ) : 0 ≤ operatorNorm A

theorem LeanPool.HansonWright.entrywiseL1Norm_nonneg {n : ℕ} (A : Matrix (Fin n) (Fin n) ℝ) : 0 ≤ entrywiseL1Norm A

theorem LeanPool.HansonWright.coordinateMask_norm_le {n : ℕ} (s : Finset (Fin n)) (x : EuclideanSpace ℝ (Fin n)) : ‖coordinateMask s x‖ ≤ ‖x‖

theorem LeanPool.HansonWright.toEuclideanCLM_cutMatrix_apply {n : ℕ} (A : Matrix (Fin n) (Fin n) ℝ) (s : Finset (Fin n)) (x : EuclideanSpace ℝ (Fin n)) : (Matrix.toEuclideanCLM (cutMatrix A s)) x = coordinateMask s ((Matrix.toEuclideanCLM A) (coordinateMask (Finset.univ \ s) x))

theorem LeanPool.HansonWright.inner_toEuclideanCLM_cutMatrix_eq_inner_masks {n : ℕ} (A : Matrix (Fin n) (Fin n) ℝ) (s : Finset (Fin n)) (x y : EuclideanSpace ℝ (Fin n)) : inner ℝ ((Matrix.toEuclideanCLM (cutMatrix A s)) x) y = inner ℝ ((Matrix.toEuclideanCLM A) (coordinateMask (Finset.univ \ s) x)) (coordinateMask s y)

theorem LeanPool.HansonWright.operatorNorm_cutMatrix_le {n : ℕ} (A : Matrix (Fin n) (Fin n) ℝ) (s : Finset (Fin n)) : operatorNorm (cutMatrix A s) ≤ operatorNorm A

theorem LeanPool.HansonWright.frobeniusNormSq_cutMatrix_le {n : ℕ} (A : Matrix (Fin n) (Fin n) ℝ) (s : Finset (Fin n)) : frobeniusNormSq (cutMatrix A s) ≤ frobeniusNormSq A

theorem LeanPool.HansonWright.frobeniusNorm_sq {n : ℕ} (A : Matrix (Fin n) (Fin n) ℝ) : frobeniusNorm A ^ 2 = frobeniusNormSq A

theorem LeanPool.HansonWright.frobeniusNorm_cutMatrix_sq_le {n : ℕ} (A : Matrix (Fin n) (Fin n) ℝ) (s : Finset (Fin n)) : frobeniusNorm (cutMatrix A s) ^ 2 ≤ frobeniusNorm A ^ 2

theorem LeanPool.HansonWright.card_powerset_filter_mem_notMem_eq {n : ℕ} {i j : Fin n} (hij : i ≠ j) : {s ∈ Finset.univ.powerset | i ∈ s ∧ j ∉ s}.card = ((Finset.univ.erase i).erase j).powerset.card

theorem LeanPool.HansonWright.four_mul_card_powerset_filter_mem_notMem {n : ℕ} {i j : Fin n} (hij : i ≠ j) : 4 * {s ∈ Finset.univ.powerset | i ∈ s ∧ j ∉ s}.card = Finset.univ.powerset.card

theorem LeanPool.HansonWright.sum_powerset_cut_indicator {n : ℕ} (i j : Fin n) (a : ℝ) : (∑ s ∈ Finset.univ.powerset, if i ∈ s ∧ j ∉ s then a else 0) = ↑{s ∈ Finset.univ.powerset | i ∈ s ∧ j ∉ s}.card * a

theorem LeanPool.HansonWright.four_mul_sum_cut_quadraticForm_eq_card_mul_offDiagonal {n : ℕ} (A : Matrix (Fin n) (Fin n) ℝ) (x : Fin n → ℝ) : 4 * ∑ s ∈ Finset.univ.powerset, quadraticForm (cutMatrix A s) x = ↑Finset.univ.powerset.card * quadraticForm (offDiagonalMatrix A) x

theorem LeanPool.HansonWright.quadraticForm_offDiagonal_eq_average_cut {n : ℕ} (A : Matrix (Fin n) (Fin n) ℝ) (x : Fin n → ℝ) : quadraticForm (offDiagonalMatrix A) x = 4 / ↑Finset.univ.powerset.card * ∑ s ∈ Finset.univ.powerset, quadraticForm (cutMatrix A s) x

theorem LeanPool.HansonWright.exp_mul_quadraticForm_offDiagonal_le_average_cut {n : ℕ} (A : Matrix (Fin n) (Fin n) ℝ) (x : Fin n → ℝ) (l : ℝ) : Real.exp (l * quadraticForm (offDiagonalMatrix A) x) ≤ (↑Finset.univ.powerset.card)⁻¹ * ∑ s ∈ Finset.univ.powerset, Real.exp (4 * l * quadraticForm (cutMatrix A s) x)

theorem LeanPool.HansonWright.quadraticForm_eq_inner_toEuclideanCLM {n : ℕ} (A : Matrix (Fin n) (Fin n) ℝ) (x : Fin n → ℝ) : quadraticForm A x = inner ℝ ((Matrix.toEuclideanCLM A) (WithLp.toLp 2 x)) (WithLp.toLp 2 x)

theorem LeanPool.HansonWright.sum_diag_sq_le_frobeniusNormSq {n : ℕ} (A : Matrix (Fin n) (Fin n) ℝ) : ∑ i : Fin n, A i i ^ 2 ≤ frobeniusNormSq A

theorem LeanPool.HansonWright.sum_diag_sq_le_frobeniusNorm_sq {n : ℕ} (A : Matrix (Fin n) (Fin n) ℝ) : ∑ i : Fin n, A i i ^ 2 ≤ frobeniusNorm A ^ 2

theorem LeanPool.HansonWright.abs_diag_le_operatorNorm {n : ℕ} (A : Matrix (Fin n) (Fin n) ℝ) (i : Fin n) : |A i i| ≤ operatorNorm A

theorem LeanPool.HansonWright.abs_quadraticForm_le {n : ℕ} (A : Matrix (Fin n) (Fin n) ℝ) {x : Fin n → ℝ} {K : ℝ} (hK : 0 ≤ K) (hx : ∀ (i : Fin n), |x i| ≤ K) : |quadraticForm A x| ≤ K ^ 2 * entrywiseL1Norm A

theorem LeanPool.HansonWright.randomQuadraticForm_aemeasurable {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {n : ℕ} (A : Matrix (Fin n) (Fin n) ℝ) {X : Fin n → Ω → ℝ} (hX_meas : ∀ (i : Fin n), AEMeasurable (X i) μ) : AEMeasurable (randomQuadraticForm A X) μ

theorem LeanPool.HansonWright.randomQuadraticForm_mem_Icc_of_ae_coord_bound {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {n : ℕ} (A : Matrix (Fin n) (Fin n) ℝ) {X : Fin n → Ω → ℝ} {K : ℝ} (hK : 0 ≤ K) (hX_bound : ∀ (i : Fin n), ∀ᵐ (ω : Ω) ∂μ, |X i ω| ≤ K) : ∀ᵐ (ω : Ω) ∂μ, randomQuadraticForm A X ω ∈ Set.Icc (-(K ^ 2 * entrywiseL1Norm A)) (K ^ 2 * entrywiseL1Norm A)

theorem LeanPool.HansonWright.bounded_hansonWright_cgf_constant_le {n : ℕ} (A : Matrix (Fin n) (Fin n) ℝ) {K C : ℝ} (hC_bound : 2 * entrywiseL1Norm A ^ 2 ≤ C * frobeniusNorm A ^ 2) (l : ℝ) : 2 * (K ^ 2 * entrywiseL1Norm A) ^ 2 * l ^ 2 ≤ C * l ^ 2 * K ^ 4 * frobeniusNorm A ^ 2

structure LeanPool.HansonWright.HasHansonWrightMGF {Ω : Type u_1} [MeasurableSpace Ω] {n : ℕ} (μ : MeasureTheory.Measure Ω) (A : Matrix (Fin n) (Fin n) ℝ) (X : Fin n → Ω → ℝ) (K C : ℝ) : Prop

The local quadratic CGF estimate used in the Hanson-Wright proof.

For Y = Xᵀ A X - E Xᵀ A X, this records cgf Y λ ≤ C λ² K⁴ ‖A‖_F² for |λ| ≤ (2 C K² ‖A‖)⁻¹, together with local exponential integrability.

• cgf_le (l : ℝ) : |l| ≤ (2 * C * K ^ 2 * operatorNorm A)⁻¹ → ProbabilityTheory.cgf (centeredQuadraticForm μ A X) μ l ≤ C * l ^ 2 * K ^ 4 * frobeniusNorm A ^ 2
• integrable_exp (l : ℝ) : |l| ≤ (2 * C * K ^ 2 * operatorNorm A)⁻¹ → MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (l * centeredQuadraticForm μ A X ω)) μ

theorem LeanPool.HansonWright.exp_le_chord {R t x : ℝ} (hR : 0 < R) (hx : x ∈ Set.Icc (-R) R) : Real.exp (t * x) ≤ (R - x) / (2 * R) * Real.exp (t * -R) + (x + R) / (2 * R) * Real.exp (t * R)

Convexity of exp gives the chord bound on a compact interval.

theorem LeanPool.HansonWright.hasSubgaussianMGF_of_abs_le_of_integral_eq_zero {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {Y : Ω → ℝ} {R : ℝ} (hY_meas : AEMeasurable Y μ) (hR : 0 ≤ R) (hY_bound : ∀ᵐ (ω : Ω) ∂μ, |Y ω| ≤ R) (hY_center : ∫ (ω : Ω), Y ω ∂μ = 0) : ProbabilityTheory.HasSubgaussianMGF Y ⟨R ^ 2, ⋯⟩ μ

A self-contained bounded, centered MGF estimate.

This is the symmetric bounded-variable form of Hoeffding's lemma, proved locally from the chord bound for exp and cosh x ≤ exp (x² / 2).

theorem LeanPool.HansonWright.integral_cosh_mul_le_of_hasSubgaussianMGF {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {c : NNReal} (h : ProbabilityTheory.HasSubgaussianMGF X c μ) (t : ℝ) : ∫ (ω : Ω), Real.cosh (t * X ω) ∂μ ≤ Real.exp (↑c * t ^ 2 / 2)

A two-sided exponential consequence of a sub-Gaussian MGF bound.

theorem LeanPool.HansonWright.cosh_taylor_term_le (y : ℝ) (m : ℕ) : y ^ (2 * m) / ↑(2 * m).factorial ≤ Real.cosh y

Each nonnegative Taylor term of cosh is bounded by cosh itself.

theorem LeanPool.HansonWright.integral_even_taylor_term_le_of_hasSubgaussianMGF {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {c : NNReal} (h : ProbabilityTheory.HasSubgaussianMGF X c μ) (t : ℝ) (m : ℕ) : ∫ (ω : Ω), (t * X ω) ^ (2 * m) / ↑(2 * m).factorial ∂μ ≤ Real.exp (↑c * t ^ 2 / 2)

Sub-Gaussian MGF control bounds every integrated even Taylor term.

theorem LeanPool.HansonWright.integral_even_power_le_of_hasSubgaussianMGF {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {c : NNReal} (h : ProbabilityTheory.HasSubgaussianMGF X c μ) {s : ℝ} (hs : 0 < s) (m : ℕ) : ∫ (ω : Ω), X ω ^ (2 * m) ∂μ ≤ ↑(2 * m).factorial / s ^ (2 * m) * Real.exp (↑c * s ^ 2 / 2)

Even moment bound obtained from sub-Gaussian MGF control at an arbitrary scale.

theorem LeanPool.HansonWright.exp_mul_sq_eq_tsum (θ x : ℝ) : Real.exp (θ * x ^ 2) = ∑' (m : ℕ), θ ^ m * x ^ (2 * m) / ↑m.factorial

Pointwise power-series expansion of exp (θ x²).

theorem LeanPool.HansonWright.factorial_two_mul_div_factorial_le_succ_pow (m : ℕ) : ↑(2 * m).factorial / ↑m.factorial ≤ ↑(2 * m + 1) ^ m

A factorial estimate used to sum the square-exponential moment series.

theorem LeanPool.HansonWright.integral_exp_sq_series_term_le_of_hasSubgaussianMGF_of_le {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {c : NNReal} (h : ProbabilityTheory.HasSubgaussianMGF X c μ) {θ C0 : ℝ} (hθ : 0 ≤ θ) (hC0 : 0 < C0) (hc_le : ↑c ≤ C0) (m : ℕ) : ∫ (ω : Ω), θ ^ m * X ω ^ (2 * m) / ↑m.factorial ∂μ ≤ Real.exp 1 * (θ * C0 * Real.exp 1) ^ m

A geometric Taylor-term bound using any positive real proxy above the sub-Gaussian parameter.

theorem LeanPool.HansonWright.integral_exp_sq_series_term_le_of_hasSubgaussianMGF {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {c : NNReal} (h : ProbabilityTheory.HasSubgaussianMGF X c μ) {θ : ℝ} (hθ : 0 ≤ θ) (m : ℕ) : ∫ (ω : Ω), θ ^ m * X ω ^ (2 * m) / ↑m.factorial ∂μ ≤ Real.exp 1 * (θ * (↑c + 1) * Real.exp 1) ^ m

A geometric bound for each integrated square-exponential Taylor term.

theorem LeanPool.HansonWright.summable_integral_exp_sq_series_of_hasSubgaussianMGF_of_le {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {c : NNReal} (h : ProbabilityTheory.HasSubgaussianMGF X c μ) {θ C0 : ℝ} (hθ : 0 ≤ θ) (hC0 : 0 < C0) (hc_le : ↑c ≤ C0) (hθ_small : θ * C0 * Real.exp 1 < 1) : Summable fun (m : ℕ) => ∫ (ω : Ω), θ ^ m * X ω ^ (2 * m) / ↑m.factorial ∂μ

Summability of square-exponential Taylor integrals using a positive proxy C0 ≥ c.

theorem LeanPool.HansonWright.summable_integral_exp_sq_series_of_hasSubgaussianMGF {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {c : NNReal} (h : ProbabilityTheory.HasSubgaussianMGF X c μ) {θ : ℝ} (hθ : 0 ≤ θ) (hθ_small : θ * (↑c + 1) * Real.exp 1 < 1) : Summable fun (m : ℕ) => ∫ (ω : Ω), θ ^ m * X ω ^ (2 * m) / ↑m.factorial ∂μ

The square-exponential Taylor integrals are summable below the explicit radius.

theorem LeanPool.HansonWright.integral_exp_mul_sq_eq_tsum_integrals {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {c : NNReal} (h : ProbabilityTheory.HasSubgaussianMGF X c μ) {θ : ℝ} (hθ : 0 ≤ θ) (hsum : Summable fun (m : ℕ) => ∫ (ω : Ω), θ ^ m * X ω ^ (2 * m) / ↑m.factorial ∂μ) : ∫ (ω : Ω), Real.exp (θ * X ω ^ 2) ∂μ = ∑' (m : ℕ), ∫ (ω : Ω), θ ^ m * X ω ^ (2 * m) / ↑m.factorial ∂μ

Integral form of the square-exponential Taylor expansion.

theorem LeanPool.HansonWright.integral_exp_mul_sq_le_inv_of_hasSubgaussianMGF_of_le {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {c : NNReal} (h : ProbabilityTheory.HasSubgaussianMGF X c μ) {θ C0 : ℝ} (hθ : 0 ≤ θ) (hC0 : 0 < C0) (hc_le : ↑c ≤ C0) (hθ_small : θ * C0 * Real.exp 1 < 1) : ∫ (ω : Ω), Real.exp (θ * X ω ^ 2) ∂μ ≤ Real.exp 1 * (1 - θ * C0 * Real.exp 1)⁻¹

A quantitative square-exponential integral bound below the proxy radius.

theorem LeanPool.HansonWright.integral_exp_mul_sq_le_one_add_tail_of_hasSubgaussianMGF_of_le {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : Ω → ℝ} {c : NNReal} (h : ProbabilityTheory.HasSubgaussianMGF X c μ) {θ C0 : ℝ} (hθ : 0 ≤ θ) (hC0 : 0 < C0) (hc_le : ↑c ≤ C0) (hθ_small : θ * C0 * Real.exp 1 < 1) : ∫ (ω : Ω), Real.exp (θ * X ω ^ 2) ∂μ ≤ 1 + Real.exp 1 * (θ * C0 * Real.exp 1 * (1 - θ * C0 * Real.exp 1)⁻¹)

A sharper square-exponential bound with the exact zeroth Taylor term isolated.

theorem LeanPool.HansonWright.integral_exp_mul_sq_le_one_add_linear_add_tail_of_hasSubgaussianMGF_of_le {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : Ω → ℝ} {c : NNReal} (h : ProbabilityTheory.HasSubgaussianMGF X c μ) {θ C0 : ℝ} (hθ : 0 ≤ θ) (hC0 : 0 < C0) (hc_le : ↑c ≤ C0) (hθ_small : θ * C0 * Real.exp 1 < 1) : ∫ (ω : Ω), Real.exp (θ * X ω ^ 2) ∂μ ≤ 1 + θ * ∫ (ω : Ω), X ω ^ 2 ∂μ + Real.exp 1 * ((θ * C0 * Real.exp 1) ^ 2 * (1 - θ * C0 * Real.exp 1)⁻¹)

A square-exponential bound with the zeroth and first Taylor terms isolated.

theorem LeanPool.HansonWright.integral_exp_mul_sq_le_exp_linear_of_hasSubgaussianMGF_of_le {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : Ω → ℝ} {c : NNReal} (h : ProbabilityTheory.HasSubgaussianMGF X c μ) {θ C0 : ℝ} (hθ : 0 ≤ θ) (hC0 : 0 < C0) (hc_le : ↑c ≤ C0) (hθ_half : θ * C0 * Real.exp 1 ≤ 1 / 2) : ∫ (ω : Ω), Real.exp (θ * X ω ^ 2) ∂μ ≤ Real.exp (2 * Real.exp 1 * (θ * C0 * Real.exp 1))

A linear-in-θ square-exponential bound at half the explicit radius.

theorem LeanPool.HansonWright.integral_exp_quadratic_stdGaussian_le {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (T : E →L[ℝ] E) (hTpos : (↑T).IsPositive) {θ : ℝ} (hθ : 0 ≤ θ) (hsmall : ∀ (i : Fin (Module.finrank ℝ E)), θ * ⋯.eigenvalues ⋯ i * Real.exp 1 ≤ 1 / 2) : ∫ (x : E), Real.exp (θ * inner ℝ (T x) x) ∂ProbabilityTheory.stdGaussian E ≤ Real.exp (2 * Real.exp 1 ^ 2 * θ * ∑ i : Fin (Module.finrank ℝ E), ⋯.eigenvalues ⋯ i)

Gaussian square-form bound for a positive symmetric operator, proved by spectral diagonalization and one-dimensional square-exponential estimates.

theorem LeanPool.HansonWright.matrix_trace_conjTranspose_mul_self_eq_frobeniusNormSq {n : ℕ} (A : Matrix (Fin n) (Fin n) ℝ) : (A.conjTranspose * A).trace = frobeniusNormSq A

theorem LeanPool.HansonWright.toEuclideanCLM_adjoint {n : ℕ} (A : Matrix (Fin n) (Fin n) ℝ) : ContinuousLinearMap.adjoint (Matrix.toEuclideanCLM A) = Matrix.toEuclideanCLM A.conjTranspose

theorem LeanPool.HansonWright.operatorNorm_conjTranspose {n : ℕ} (A : Matrix (Fin n) (Fin n) ℝ) : operatorNorm A.conjTranspose = operatorNorm A

theorem LeanPool.HansonWright.frobeniusNormSq_conjTranspose {n : ℕ} (A : Matrix (Fin n) (Fin n) ℝ) : frobeniusNormSq A.conjTranspose = frobeniusNormSq A

theorem LeanPool.HansonWright.frobeniusNorm_conjTranspose_sq {n : ℕ} (A : Matrix (Fin n) (Fin n) ℝ) : frobeniusNorm A.conjTranspose ^ 2 = frobeniusNorm A ^ 2

theorem LeanPool.HansonWright.trace_adjoint_comp_toEuclideanCLM_eq_frobeniusNormSq {n : ℕ} (A : Matrix (Fin n) (Fin n) ℝ) : (LinearMap.trace ℝ (EuclideanSpace ℝ (Fin n))) ↑(ContinuousLinearMap.adjoint (Matrix.toEuclideanCLM A) ∘SL Matrix.toEuclideanCLM A) = frobeniusNormSq A

theorem LeanPool.HansonWright.eigenvalue_adjoint_comp_le_opNorm_sq {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] (T : E →L[ℝ] E) (i : Fin (Module.finrank ℝ E)) : let S := ContinuousLinearMap.adjoint T ∘SL T; have hSpos := ⋯; ⋯.eigenvalues ⋯ i ≤ ‖T‖ ^ 2

theorem LeanPool.HansonWright.integral_sq_le_of_hasSubgaussianMGF_of_le {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {c : NNReal} (h : ProbabilityTheory.HasSubgaussianMGF X c μ) {C0 : ℝ} (hC0 : 0 < C0) (hc_le : ↑c ≤ C0) : ∫ (ω : Ω), X ω ^ 2 ∂μ ≤ Real.exp 1 * (C0 * Real.exp 1)

A second-moment bound from the square-exponential Taylor-term estimate.

theorem LeanPool.HansonWright.integral_fourth_le_of_hasSubgaussianMGF_of_le {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {c : NNReal} (h : ProbabilityTheory.HasSubgaussianMGF X c μ) {C0 : ℝ} (hC0 : 0 < C0) (hc_le : ↑c ≤ C0) : ∫ (ω : Ω), X ω ^ 4 ∂μ ≤ 2 * Real.exp 1 * (C0 * Real.exp 1) ^ 2

A fourth-moment bound from the square-exponential Taylor-term estimate.

theorem LeanPool.HansonWright.exp_neg_le_one_sub_add_sq {u : ℝ} (hu : 0 ≤ u) : Real.exp (-u) ≤ 1 - u + u ^ 2

A global quadratic upper bound for the negative exponential on the nonnegative half-line.

theorem LeanPool.HansonWright.exp_neg_mul_one_add_le_one (u : ℝ) : Real.exp (-u) * (1 + u) ≤ 1

The linear Taylor term cancels after multiplying by exp (-u).

theorem LeanPool.HansonWright.integral_exp_centered_sq_le_exp_quadratic_nonneg {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : Ω → ℝ} {c : NNReal} (h : ProbabilityTheory.HasSubgaussianMGF X c μ) {θ C0 : ℝ} (hθ : 0 ≤ θ) (hC0 : 0 < C0) (hc_le : ↑c ≤ C0) (hθ_half : θ * C0 * Real.exp 1 ≤ 1 / 2) : ∫ (ω : Ω), Real.exp (θ * (X ω ^ 2 - ∫ (ω : Ω), X ω ^ 2 ∂μ)) ∂μ ≤ Real.exp (2 * Real.exp 1 * (θ * C0 * Real.exp 1) ^ 2)

Positive-parameter MGF bound for a centered square of a sub-Gaussian variable.

theorem LeanPool.HansonWright.integral_exp_centered_sq_le_exp_quadratic_nonpos {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : Ω → ℝ} {c : NNReal} (h : ProbabilityTheory.HasSubgaussianMGF X c μ) {θ C0 : ℝ} (hθ : θ ≤ 0) (hC0 : 0 < C0) (hc_le : ↑c ≤ C0) : ∫ (ω : Ω), Real.exp (θ * (X ω ^ 2 - ∫ (ω : Ω), X ω ^ 2 ∂μ)) ∂μ ≤ Real.exp (2 * Real.exp 1 * (-θ * C0 * Real.exp 1) ^ 2)

Negative-parameter MGF bound for a centered square of a sub-Gaussian variable.

theorem LeanPool.HansonWright.integrable_exp_mul_sq_of_summable_integrals {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {c : NNReal} (h : ProbabilityTheory.HasSubgaussianMGF X c μ) {θ : ℝ} (hθ : 0 ≤ θ) (hsum : Summable fun (m : ℕ) => ∫ (ω : Ω), θ ^ m * X ω ^ (2 * m) / ↑m.factorial ∂μ) : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (θ * X ω ^ 2)) μ

Square-exponential integrability from summability of the nonnegative moment series.

theorem LeanPool.HansonWright.integrable_exp_mul_sq_of_hasSubgaussianMGF {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {c : NNReal} (h : ProbabilityTheory.HasSubgaussianMGF X c μ) {θ : ℝ} (hθ : 0 ≤ θ) (hθ_small : θ * (↑c + 1) * Real.exp 1 < 1) : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (θ * X ω ^ 2)) μ

Square-exponential integrability for a sub-Gaussian variable at small positive parameter.

theorem LeanPool.HansonWright.integrable_exp_mul_sq_of_hasSubgaussianMGF_of_le {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {c : NNReal} (h : ProbabilityTheory.HasSubgaussianMGF X c μ) {θ C0 : ℝ} (hθ : 0 ≤ θ) (hC0 : 0 < C0) (hc_le : ↑c ≤ C0) (hθ_small : θ * C0 * Real.exp 1 < 1) : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (θ * X ω ^ 2)) μ

Small-parameter square-exponential integrability using a positive proxy C0 ≥ c.

theorem LeanPool.HansonWright.integrable_exp_quadratic_stdGaussian {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (T : E →L[ℝ] E) (hTpos : (↑T).IsPositive) {θ : ℝ} (hθ : 0 ≤ θ) (hsmall : ∀ (i : Fin (Module.finrank ℝ E)), θ * ⋯.eigenvalues ⋯ i * Real.exp 1 < 1) : MeasureTheory.Integrable (fun (x : E) => Real.exp (θ * inner ℝ (T x) x)) (ProbabilityTheory.stdGaussian E)

Gaussian square-form integrability for a positive symmetric operator, under the strict version of the same coordinate smallness condition.

theorem LeanPool.HansonWright.integrable_exp_inner_toEuclideanCLM_prod_stdGaussian {n : ℕ} (A : Matrix (Fin n) (Fin n) ℝ) {l : ℝ} (hsmall : l ^ 2 / 2 * operatorNorm A ^ 2 * Real.exp 1 < 1) : MeasureTheory.Integrable (fun (p : EuclideanSpace ℝ (Fin n) × EuclideanSpace ℝ (Fin n)) => Real.exp (l * inner ℝ ((Matrix.toEuclideanCLM A) p.1) p.2)) ((ProbabilityTheory.stdGaussian (EuclideanSpace ℝ (Fin n))).prod (ProbabilityTheory.stdGaussian (EuclideanSpace ℝ (Fin n))))

Integrability of the exponential of a Gaussian bilinear form.

theorem LeanPool.HansonWright.integral_exp_inner_toEuclideanCLM_prod_stdGaussian_le {n : ℕ} (A : Matrix (Fin n) (Fin n) ℝ) {l : ℝ} (hsmall : l ^ 2 / 2 * operatorNorm A ^ 2 * Real.exp 1 ≤ 1 / 2) : ∫ (p : EuclideanSpace ℝ (Fin n) × EuclideanSpace ℝ (Fin n)), Real.exp (l * inner ℝ ((Matrix.toEuclideanCLM A) p.1) p.2) ∂(ProbabilityTheory.stdGaussian (EuclideanSpace ℝ (Fin n))).prod (ProbabilityTheory.stdGaussian (EuclideanSpace ℝ (Fin n))) ≤ Real.exp (Real.exp 1 ^ 2 * l ^ 2 * frobeniusNorm A ^ 2)

A Frobenius-scale bound for the exponential moment of a Gaussian bilinear form.

theorem LeanPool.HansonWright.integrable_exp_centered_sq_of_hasSubgaussianMGF_of_le {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : Ω → ℝ} {c : NNReal} (h : ProbabilityTheory.HasSubgaussianMGF X c μ) {θ C0 : ℝ} (hC0 : 0 < C0) (hc_le : ↑c ≤ C0) (hθ_abs : |θ| * C0 * Real.exp 1 < 1) : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (θ * (X ω ^ 2 - ∫ (ω : Ω), X ω ^ 2 ∂μ))) μ

Local exponential integrability for centered squares of sub-Gaussian variables.

theorem LeanPool.HansonWright.mgf_id_map_eq {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} (hX : AEMeasurable X μ) (t : ℝ) : ProbabilityTheory.mgf id (MeasureTheory.Measure.map X μ) t = ProbabilityTheory.mgf X μ t

The MGF of the identity under a push-forward law is the MGF of the original variable.

theorem LeanPool.HansonWright.integrable_exp_mul_id_map {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {t : ℝ} (hX : AEMeasurable X μ) (h : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (t * X ω)) μ) : MeasureTheory.Integrable (fun (x : ℝ) => Real.exp (t * id x)) (MeasureTheory.Measure.map X μ)

theorem LeanPool.HansonWright.hasSubgaussianMGF_id_map {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {c : NNReal} (h : ProbabilityTheory.HasSubgaussianMGF X c μ) : ProbabilityTheory.HasSubgaussianMGF id c (MeasureTheory.Measure.map X μ)

theorem LeanPool.HansonWright.integrable_exp_mul_snd_fst_prod_of_hasSubgaussianMGF_of_le {νX νY : MeasureTheory.Measure ℝ} [MeasureTheory.IsProbabilityMeasure νX] {cX cY : NNReal} (hX : ProbabilityTheory.HasSubgaussianMGF id cX νX) (hY : ProbabilityTheory.HasSubgaussianMGF id cY νY) {C0 θ : ℝ} (hC0 : 0 < C0) (hcX : ↑cX ≤ C0) (hcY : ↑cY ≤ C0) (hθ_half : C0 * θ ^ 2 / 2 * C0 * Real.exp 1 ≤ 1 / 2) : MeasureTheory.Integrable (fun (p : ℝ × ℝ) => Real.exp (θ * p.2 * p.1)) (νY.prod νX)

theorem LeanPool.HansonWright.integral_exp_mul_snd_fst_prod_le_of_hasSubgaussianMGF_of_le {νX νY : MeasureTheory.Measure ℝ} [MeasureTheory.IsProbabilityMeasure νX] [MeasureTheory.IsProbabilityMeasure νY] {cX cY : NNReal} (hX : ProbabilityTheory.HasSubgaussianMGF id cX νX) (hY : ProbabilityTheory.HasSubgaussianMGF id cY νY) {C0 θ : ℝ} (hC0 : 0 < C0) (hcX : ↑cX ≤ C0) (hcY : ↑cY ≤ C0) (hθ_half : C0 * θ ^ 2 / 2 * C0 * Real.exp 1 ≤ 1 / 2) : ∫ (p : ℝ × ℝ), Real.exp (θ * p.2 * p.1) ∂νY.prod νX ≤ Real.exp (Real.exp 1 ^ 2 * C0 ^ 2 * θ ^ 2)

theorem LeanPool.HansonWright.integrable_exp_mul_prod_of_indepFun_hasSubgaussianMGF_of_le {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X Y : Ω → ℝ} (h_indep : ProbabilityTheory.IndepFun X Y μ) {cX cY : NNReal} (hX : ProbabilityTheory.HasSubgaussianMGF X cX μ) (hY : ProbabilityTheory.HasSubgaussianMGF Y cY μ) {C0 θ : ℝ} (hC0 : 0 < C0) (hcX : ↑cX ≤ C0) (hcY : ↑cY ≤ C0) (hθ_half : C0 * θ ^ 2 / 2 * C0 * Real.exp 1 ≤ 1 / 2) : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (θ * X ω * Y ω)) μ

theorem LeanPool.HansonWright.integral_exp_mul_prod_le_of_indepFun_hasSubgaussianMGF_of_le {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X Y : Ω → ℝ} (h_indep : ProbabilityTheory.IndepFun X Y μ) {cX cY : NNReal} (hX : ProbabilityTheory.HasSubgaussianMGF X cX μ) (hY : ProbabilityTheory.HasSubgaussianMGF Y cY μ) {C0 θ : ℝ} (hC0 : 0 < C0) (hcX : ↑cX ≤ C0) (hcY : ↑cY ≤ C0) (hθ_half : C0 * θ ^ 2 / 2 * C0 * Real.exp 1 ≤ 1 / 2) : ∫ (ω : Ω), Real.exp (θ * X ω * Y ω) ∂μ ≤ Real.exp (Real.exp 1 ^ 2 * C0 ^ 2 * θ ^ 2)

theorem LeanPool.HansonWright.centered_sq_cgf_le_of_hasSubgaussianMGF_of_le {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : Ω → ℝ} {c : NNReal} (h : ProbabilityTheory.HasSubgaussianMGF X c μ) {θ C0 : ℝ} (hC0 : 0 < C0) (hc_le : ↑c ≤ C0) (hθ_abs : |θ| * C0 * Real.exp 1 ≤ 1 / 2) : ProbabilityTheory.cgf (fun (ω : Ω) => X ω ^ 2 - ∫ (ω : Ω), X ω ^ 2 ∂μ) μ θ ≤ 2 * Real.exp 1 * (θ * C0 * Real.exp 1) ^ 2

CGF bound for a centered square of a sub-Gaussian variable.

noncomputable def LeanPool.HansonWright.diagonalCenteredQuadraticForm {Ω : Type u_1} [MeasurableSpace Ω] {n : ℕ} (μ : MeasureTheory.Measure Ω) (A : Matrix (Fin n) (Fin n) ℝ) (X : Fin n → Ω → ℝ) : Ω → ℝ

The centered diagonal part of a quadratic form.

Equations

• LeanPool.HansonWright.diagonalCenteredQuadraticForm μ A X ω = ∑ i : Fin n, A i i * (X i ω ^ 2 - ∫ (ω : Ω), X i ω ^ 2 ∂μ)

theorem LeanPool.HansonWright.cgf_const_mul {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {Y : Ω → ℝ} (a θ : ℝ) : ProbabilityTheory.cgf (fun (ω : Ω) => a * Y ω) μ θ = ProbabilityTheory.cgf Y μ (a * θ)

theorem LeanPool.HansonWright.iIndepFun_centered_sq {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {n : ℕ} {X : Fin n → Ω → ℝ} (h_indep : ProbabilityTheory.iIndepFun X μ) : ProbabilityTheory.iIndepFun (fun (i : Fin n) (ω : Ω) => X i ω ^ 2 - ∫ (ω : Ω), X i ω ^ 2 ∂μ) μ

theorem LeanPool.HansonWright.diagonalCenteredQuadraticForm_cgf_le {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {n : ℕ} {A : Matrix (Fin n) (Fin n) ℝ} {X : Fin n → Ω → ℝ} {K C θ : ℝ} (hK : 0 < K) (hC_quad : 2 * Real.exp 1 ^ 3 ≤ C) (hOp : 0 < operatorNorm A) (h_indep : ProbabilityTheory.iIndepFun X μ) (hX_subG : ∀ (i : Fin n), ProbabilityTheory.HasSubgaussianMGF (X i) ⟨K ^ 2, ⋯⟩ μ) (hθ : |θ| ≤ (2 * C * K ^ 2 * operatorNorm A)⁻¹) : ProbabilityTheory.cgf (diagonalCenteredQuadraticForm μ A X) μ θ ≤ C * θ ^ 2 * K ^ 4 * frobeniusNorm A ^ 2

theorem LeanPool.HansonWright.diagonalCenteredQuadraticForm_integrable_exp {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {n : ℕ} {A : Matrix (Fin n) (Fin n) ℝ} {X : Fin n → Ω → ℝ} {K C θ : ℝ} (hK : 0 < K) (hC_domain : Real.exp 1 ≤ C) (hOp : 0 < operatorNorm A) (h_indep : ProbabilityTheory.iIndepFun X μ) (hX_subG : ∀ (i : Fin n), ProbabilityTheory.HasSubgaussianMGF (X i) ⟨K ^ 2, ⋯⟩ μ) (hθ : |θ| ≤ (2 * C * K ^ 2 * operatorNorm A)⁻¹) : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (θ * diagonalCenteredQuadraticForm μ A X ω)) μ

theorem LeanPool.HansonWright.quadraticForm_eq_sum_diag_of_offdiag_eq_zero {n : ℕ} {A : Matrix (Fin n) (Fin n) ℝ} {x : Fin n → ℝ} (hA_diag : ∀ (i j : Fin n), i ≠ j → A i j = 0) : quadraticForm A x = ∑ i : Fin n, A i i * x i ^ 2

theorem LeanPool.HansonWright.centeredQuadraticForm_eq_diagonalCentered_of_offdiag_eq_zero {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {n : ℕ} {A : Matrix (Fin n) (Fin n) ℝ} {X : Fin n → Ω → ℝ} {K : ℝ} (hA_diag : ∀ (i j : Fin n), i ≠ j → A i j = 0) (hX_subG : ∀ (i : Fin n), ProbabilityTheory.HasSubgaussianMGF (X i) ⟨K ^ 2, ⋯⟩ μ) : centeredQuadraticForm μ A X = diagonalCenteredQuadraticForm μ A X

theorem LeanPool.HansonWright.hasHansonWrightMGF_diagonal_of_subgaussian {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {n : ℕ} {A : Matrix (Fin n) (Fin n) ℝ} {X : Fin n → Ω → ℝ} {K C : ℝ} (hK : 0 < K) (hC_quad : 2 * Real.exp 1 ^ 3 ≤ C) (hOp : 0 < operatorNorm A) (hA_diag : ∀ (i j : Fin n), i ≠ j → A i j = 0) (h_indep : ProbabilityTheory.iIndepFun X μ) (hX_subG : ∀ (i : Fin n), ProbabilityTheory.HasSubgaussianMGF (X i) ⟨K ^ 2, ⋯⟩ μ) : HasHansonWrightMGF μ A X K C

Hanson-Wright MGF certificate for diagonal quadratic forms with sub-Gaussian coordinates.

theorem LeanPool.HansonWright.quadraticForm_eq_diag_add_offDiagonal {n : ℕ} (A : Matrix (Fin n) (Fin n) ℝ) (x : Fin n → ℝ) : quadraticForm A x = ∑ i : Fin n, A i i * x i ^ 2 + quadraticForm (offDiagonalMatrix A) x

theorem LeanPool.HansonWright.integrable_randomQuadraticForm_offDiagonal_of_subgaussian {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {n : ℕ} (A : Matrix (Fin n) (Fin n) ℝ) {X : Fin n → Ω → ℝ} {K : ℝ} (h_indep : ProbabilityTheory.iIndepFun X μ) (hX_subG : ∀ (i : Fin n), ProbabilityTheory.HasSubgaussianMGF (X i) ⟨K ^ 2, ⋯⟩ μ) : MeasureTheory.Integrable (randomQuadraticForm (offDiagonalMatrix A) X) μ

theorem LeanPool.HansonWright.integral_randomQuadraticForm_offDiagonal_eq_zero {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {n : ℕ} (A : Matrix (Fin n) (Fin n) ℝ) {X : Fin n → Ω → ℝ} {K : ℝ} (h_indep : ProbabilityTheory.iIndepFun X μ) (hX_subG : ∀ (i : Fin n), ProbabilityTheory.HasSubgaussianMGF (X i) ⟨K ^ 2, ⋯⟩ μ) : ∫ (ω : Ω), randomQuadraticForm (offDiagonalMatrix A) X ω ∂μ = 0

theorem LeanPool.HansonWright.centeredQuadraticForm_eq_diagonal_add_offDiagonal {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {n : ℕ} (A : Matrix (Fin n) (Fin n) ℝ) {X : Fin n → Ω → ℝ} {K : ℝ} (h_indep : ProbabilityTheory.iIndepFun X μ) (hX_subG : ∀ (i : Fin n), ProbabilityTheory.HasSubgaussianMGF (X i) ⟨K ^ 2, ⋯⟩ μ) : centeredQuadraticForm μ A X = fun (ω : Ω) => diagonalCenteredQuadraticForm μ A X ω + quadraticForm (offDiagonalMatrix A) fun (i : Fin n) => X i ω

theorem LeanPool.HansonWright.hasSubgaussianMGF_finset_sum_const_mul_of_iIndepFun {Ω : Type u_1} [MeasurableSpace Ω] {ι : Type u_2} {μ : MeasureTheory.Measure Ω} {X : ι → Ω → ℝ} (h_indep : ProbabilityTheory.iIndepFun X μ) {c : ι → NNReal} {s : Finset ι} (h_subG : ∀ i ∈ s, ProbabilityTheory.HasSubgaussianMGF (X i) (c i) μ) (a : ι → ℝ) : ProbabilityTheory.HasSubgaussianMGF (fun (ω : Ω) => ∑ i ∈ s, a i * X i ω) (∑ i ∈ s, (a i ^ 2).toNNReal * c i) μ

A finite independent linear combination of sub-Gaussian variables is sub-Gaussian.

theorem LeanPool.HansonWright.inner_randomVector_hasSubgaussianMGF_of_iIndepFun {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {n : ℕ} {X : Fin n → Ω → ℝ} {K : ℝ} (h_indep : ProbabilityTheory.iIndepFun X μ) (hX_subG : ∀ (i : Fin n), ProbabilityTheory.HasSubgaussianMGF (X i) ⟨K ^ 2, ⋯⟩ μ) (v : EuclideanSpace ℝ (Fin n)) : ProbabilityTheory.HasSubgaussianMGF (fun (ω : Ω) => inner ℝ v (randomVector X ω)) ⟨K ^ 2 * ‖v‖ ^ 2, ⋯⟩ μ

Fixed linear forms of an independent sub-Gaussian coordinate vector are sub-Gaussian.

theorem LeanPool.HansonWright.integral_exp_norm_toEuclideanCLM_randomVector_sq_le {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {n : ℕ} (A : Matrix (Fin n) (Fin n) ℝ) {X : Fin n → Ω → ℝ} {K θ : ℝ} (hθ : 0 ≤ θ) (h_indep : ProbabilityTheory.iIndepFun X μ) (hX_subG : ∀ (i : Fin n), ProbabilityTheory.HasSubgaussianMGF (X i) ⟨K ^ 2, ⋯⟩ μ) (hsmall : θ * K ^ 2 * operatorNorm A ^ 2 * Real.exp 1 ≤ 1 / 2) : ∫ (ω : Ω), Real.exp (θ * ‖(Matrix.toEuclideanCLM A) (randomVector X ω)‖ ^ 2) ∂μ ≤ Real.exp (2 * Real.exp 1 ^ 2 * θ * K ^ 2 * frobeniusNorm A ^ 2)

Gaussian-comparison square-exponential bound for a linear image of an independent sub-Gaussian vector.

theorem LeanPool.HansonWright.integrable_exp_norm_toEuclideanCLM_randomVector_sq {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {n : ℕ} (A : Matrix (Fin n) (Fin n) ℝ) {X : Fin n → Ω → ℝ} {K θ : ℝ} (hθ : 0 ≤ θ) (h_indep : ProbabilityTheory.iIndepFun X μ) (hX_subG : ∀ (i : Fin n), ProbabilityTheory.HasSubgaussianMGF (X i) ⟨K ^ 2, ⋯⟩ μ) (hsmall : θ * K ^ 2 * operatorNorm A ^ 2 * Real.exp 1 < 1) : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (θ * ‖(Matrix.toEuclideanCLM A) (randomVector X ω)‖ ^ 2)) μ

theorem LeanPool.HansonWright.integrable_exp_inner_toEuclideanCLM_randomVector_prod {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {n : ℕ} (A : Matrix (Fin n) (Fin n) ℝ) {X : Fin n → Ω → ℝ} {K l : ℝ} (h_indep : ProbabilityTheory.iIndepFun X μ) (hX_subG : ∀ (i : Fin n), ProbabilityTheory.HasSubgaussianMGF (X i) ⟨K ^ 2, ⋯⟩ μ) (hsmall : K ^ 2 * l ^ 2 / 2 * K ^ 2 * operatorNorm A ^ 2 * Real.exp 1 < 1) : MeasureTheory.Integrable (fun (p : Ω × Ω) => Real.exp (l * inner ℝ ((Matrix.toEuclideanCLM A) (randomVector X p.1)) (randomVector X p.2))) (μ.prod μ)

theorem LeanPool.HansonWright.integral_exp_inner_toEuclideanCLM_randomVector_prod_le {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {n : ℕ} (A : Matrix (Fin n) (Fin n) ℝ) {X : Fin n → Ω → ℝ} {K l : ℝ} (h_indep : ProbabilityTheory.iIndepFun X μ) (hX_subG : ∀ (i : Fin n), ProbabilityTheory.HasSubgaussianMGF (X i) ⟨K ^ 2, ⋯⟩ μ) (hsmall : K ^ 2 * l ^ 2 / 2 * K ^ 2 * operatorNorm A ^ 2 * Real.exp 1 ≤ 1 / 2) : ∫ (p : Ω × Ω), Real.exp (l * inner ℝ ((Matrix.toEuclideanCLM A) (randomVector X p.1)) (randomVector X p.2)) ∂μ.prod μ ≤ Real.exp (Real.exp 1 ^ 2 * l ^ 2 * K ^ 4 * frobeniusNorm A ^ 2)

theorem LeanPool.HansonWright.integral_exp_quadraticForm_cutMatrix_eq_prod {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {n : ℕ} (A : Matrix (Fin n) (Fin n) ℝ) (s : Finset (Fin n)) {X : Fin n → Ω → ℝ} {l : ℝ} (h_indep : ProbabilityTheory.iIndepFun X μ) (hX_meas : ∀ (i : Fin n), AEMeasurable (X i) μ) (hprod_int : MeasureTheory.Integrable (fun (p : Ω × Ω) => Real.exp (l * inner ℝ ((Matrix.toEuclideanCLM (cutMatrix A s)) (randomVector X p.1)) (randomVector X p.2))) (μ.prod μ)) : ∫ (ω : Ω), Real.exp (l * quadraticForm (cutMatrix A s) fun (i : Fin n) => X i ω) ∂μ = ∫ (p : Ω × Ω), Real.exp (l * inner ℝ ((Matrix.toEuclideanCLM (cutMatrix A s)) (randomVector X p.1)) (randomVector X p.2)) ∂μ.prod μ

theorem LeanPool.HansonWright.integrable_exp_quadraticForm_cutMatrix {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {n : ℕ} (A : Matrix (Fin n) (Fin n) ℝ) (s : Finset (Fin n)) {X : Fin n → Ω → ℝ} {K l : ℝ} (h_indep : ProbabilityTheory.iIndepFun X μ) (hX_subG : ∀ (i : Fin n), ProbabilityTheory.HasSubgaussianMGF (X i) ⟨K ^ 2, ⋯⟩ μ) (hsmall : K ^ 2 * l ^ 2 / 2 * K ^ 2 * operatorNorm (cutMatrix A s) ^ 2 * Real.exp 1 < 1) : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (l * quadraticForm (cutMatrix A s) fun (i : Fin n) => X i ω)) μ

theorem LeanPool.HansonWright.integral_exp_quadraticForm_cutMatrix_le {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {n : ℕ} (A : Matrix (Fin n) (Fin n) ℝ) (s : Finset (Fin n)) {X : Fin n → Ω → ℝ} {K l : ℝ} (h_indep : ProbabilityTheory.iIndepFun X μ) (hX_subG : ∀ (i : Fin n), ProbabilityTheory.HasSubgaussianMGF (X i) ⟨K ^ 2, ⋯⟩ μ) (hsmall : K ^ 2 * l ^ 2 / 2 * K ^ 2 * operatorNorm (cutMatrix A s) ^ 2 * Real.exp 1 ≤ 1 / 2) : ∫ (ω : Ω), Real.exp (l * quadraticForm (cutMatrix A s) fun (i : Fin n) => X i ω) ∂μ ≤ Real.exp (Real.exp 1 ^ 2 * l ^ 2 * K ^ 4 * frobeniusNorm (cutMatrix A s) ^ 2)

theorem LeanPool.HansonWright.integrable_exp_quadraticForm_offDiagonal {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {n : ℕ} (A : Matrix (Fin n) (Fin n) ℝ) {X : Fin n → Ω → ℝ} {K l : ℝ} (h_indep : ProbabilityTheory.iIndepFun X μ) (hX_subG : ∀ (i : Fin n), ProbabilityTheory.HasSubgaussianMGF (X i) ⟨K ^ 2, ⋯⟩ μ) (hsmall : K ^ 2 * (4 * l) ^ 2 / 2 * K ^ 2 * operatorNorm A ^ 2 * Real.exp 1 < 1) : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (l * quadraticForm (offDiagonalMatrix A) fun (i : Fin n) => X i ω)) μ

theorem LeanPool.HansonWright.integral_exp_quadraticForm_offDiagonal_le {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {n : ℕ} (A : Matrix (Fin n) (Fin n) ℝ) {X : Fin n → Ω → ℝ} {K l : ℝ} (h_indep : ProbabilityTheory.iIndepFun X μ) (hX_subG : ∀ (i : Fin n), ProbabilityTheory.HasSubgaussianMGF (X i) ⟨K ^ 2, ⋯⟩ μ) (hsmall : K ^ 2 * (4 * l) ^ 2 / 2 * K ^ 2 * operatorNorm A ^ 2 * Real.exp 1 ≤ 1 / 2) : ∫ (ω : Ω), Real.exp (l * quadraticForm (offDiagonalMatrix A) fun (i : Fin n) => X i ω) ∂μ ≤ Real.exp (Real.exp 1 ^ 2 * (4 * l) ^ 2 * K ^ 4 * frobeniusNorm A ^ 2)

theorem LeanPool.HansonWright.abs_two_mul_le_inv_quarter_of_abs_le {a C l : ℝ} (ha : 0 < a) (hC : 0 < C) (hl : |l| ≤ (2 * C * a)⁻¹) : |2 * l| ≤ (2 * (C / 4) * a)⁻¹

theorem LeanPool.HansonWright.abs_mul_le_inv_two_of_abs_le {a C l : ℝ} (ha : 0 < a) (hC : 0 < C) (hl : |l| ≤ (2 * C * a)⁻¹) : |l| * a ≤ 1 / (2 * C)

theorem LeanPool.HansonWright.offDiagonal_small_two_mul_of_abs_le {K C op l : ℝ} (hK : 0 < K) (hC : 0 < C) (hop : 0 < op) (hC_sq : 16 * Real.exp 1 ≤ C ^ 2) (hl : |l| ≤ (2 * C * K ^ 2 * op)⁻¹) : K ^ 2 * (4 * (2 * l)) ^ 2 / 2 * K ^ 2 * op ^ 2 * Real.exp 1 ≤ 1 / 2

theorem LeanPool.HansonWright.offDiagonal_exponent_two_mul_le {K C F l : ℝ} (hC_offdiag_quad : 64 * Real.exp 1 ^ 2 ≤ C) : Real.exp 1 ^ 2 * (4 * (2 * l)) ^ 2 * K ^ 4 * F ^ 2 ≤ C * l ^ 2 * K ^ 4 * F ^ 2

theorem LeanPool.HansonWright.hasHansonWrightMGF_of_subgaussian {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {n : ℕ} {A : Matrix (Fin n) (Fin n) ℝ} {X : Fin n → Ω → ℝ} {K C : ℝ} (hK : 0 < K) (hC_offdiag_quad : 64 * Real.exp 1 ^ 2 ≤ C) (hOp : 0 < operatorNorm A) (h_indep : ProbabilityTheory.iIndepFun X μ) (hX_subG : ∀ (i : Fin n), ProbabilityTheory.HasSubgaussianMGF (X i) ⟨K ^ 2, ⋯⟩ μ) : HasHansonWrightMGF μ A X K C

Hanson-Wright MGF certificate from independent sub-Gaussian coordinates.

theorem LeanPool.HansonWright.hasHansonWrightMGF_of_bounded {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {n : ℕ} {A : Matrix (Fin n) (Fin n) ℝ} {X : Fin n → Ω → ℝ} {K C : ℝ} (hK : 0 ≤ K) (hX_meas : ∀ (i : Fin n), AEMeasurable (X i) μ) (hX_bound : ∀ (i : Fin n), ∀ᵐ (ω : Ω) ∂μ, |X i ω| ≤ K) (hC_bound : 2 * entrywiseL1Norm A ^ 2 ≤ C * frobeniusNorm A ^ 2) : HasHansonWrightMGF μ A X K C

A proved Hanson-Wright MGF certificate for bounded coordinates.

If each coordinate satisfies |Xᵢ| ≤ K almost surely, then the quadratic form lies in the interval [-K²‖A‖₁, K²‖A‖₁]. The centered quadratic form is therefore bounded by 2K²‖A‖₁; the local bounded MGF lemma above gives a quadratic CGF estimate. The explicit side condition compares this bounded-coordinate constant with the Frobenius-scale constant used by the Hanson-Wright tail statement.

theorem LeanPool.HansonWright.hanson_wright_inequality {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {n : ℕ} {A : Matrix (Fin n) (Fin n) ℝ} {X : Fin n → Ω → ℝ} {K C t : ℝ} (hK : 0 < K) (hC_offdiag_quad : 64 * Real.exp 1 ^ 2 ≤ C) (hF : 0 < frobeniusNorm A) (hOp : 0 < operatorNorm A) (h_indep : ProbabilityTheory.iIndepFun X μ) (hX_subG : ∀ (i : Fin n), ProbabilityTheory.HasSubgaussianMGF (X i) ⟨K ^ 2, ⋯⟩ μ) (ht : 0 ≤ t) : (μ {ω : Ω | t ≤ |centeredQuadraticForm μ A X ω|}).toReal ≤ 2 * Real.exp (-(1 / (4 * C)) * min (t ^ 2 / (K ^ 4 * frobeniusNorm A ^ 2)) (t / (K ^ 2 * operatorNorm A)))

Hanson-Wright tail bound with the MGF certificate proved from sub-Gaussian coordinates.

This theorem does not take HasHansonWrightMGF as a hypothesis. Instead it proves that certificate from independence and coordinate sub-Gaussian MGF bounds, then optimizes the resulting Chernoff bound.

theorem LeanPool.HansonWright.hanson_wright_inequality_hdp_explicit {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {n : ℕ} {A : Matrix (Fin n) (Fin n) ℝ} {X : Fin n → Ω → ℝ} {K C t : ℝ} (hK_def : K = maxSubGaussianPsi2Norm X μ) (hK : 0 < K) (hC_offdiag_quad : 64 * Real.exp 1 ^ 2 ≤ C) (hF : 0 < frobeniusNorm A) (hOp : 0 < operatorNorm A) (h_indep : ProbabilityTheory.iIndepFun X μ) (hX_finite : ∀ (i : Fin n), HasFiniteSubGaussianPsi2Norm (X i) μ) (ht : 0 ≤ t) : (μ {ω : Ω | t ≤ |centeredQuadraticForm μ A X ω|}).toReal ≤ 2 * Real.exp (-(1 / (4 * C)) * min (t ^ 2 / (K ^ 4 * frobeniusNorm A ^ 2)) (t / (K ^ 2 * operatorNorm A)))

Hanson-Wright inequality in the HDP normalization.

The scale K is the maximum coordinate least global-MGF sub-Gaussian scale. The proof expands this definition into the exact MGF bounds required by hanson_wright_inequality.

theorem LeanPool.HansonWright.hanson_wright_inequality_hdp {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {n : ℕ} {A : Matrix (Fin n) (Fin n) ℝ} {X : Fin n → Ω → ℝ} {K : ℝ} (hK_def : K = maxSubGaussianPsi2Norm X μ) (hK : 0 < K) (hF : 0 < frobeniusNorm A) (hOp : 0 < operatorNorm A) (h_indep : ProbabilityTheory.iIndepFun X μ) (hX_finite : ∀ (i : Fin n), HasFiniteSubGaussianPsi2Norm (X i) μ) (t : ℝ) : 0 ≤ t → (μ {ω : Ω | t ≤ |centeredQuadraticForm μ A X ω|}).toReal ≤ 2 * Real.exp (-(1 / (256 * Real.exp 1 ^ 2)) * min (t ^ 2 / (K ^ 4 * frobeniusNorm A ^ 2)) (t / (K ^ 2 * operatorNorm A)))

Hanson-Wright inequality in the nondegenerate form of Theorem 6.2.2 of HDP.

For independent coordinates and K equal to their positive maximum least global-MGF sub-Gaussian scale, this gives the usual two-regime tail bound with the fixed universal coefficient 1 / (256 * exp 1 ^ 2). The MGF hypothesis implied by finiteness of the coordinate scales also forces the coordinates to have mean zero.