Stat.Concentration.BoundedVariation.SignMGF
The uniform law on Boolean sign vectors gives the basic sub-Gaussian estimate used in the bounded-variation path maximal inequality.
SignMGF 1 core · 0 supporting The uniform law on Boolean sign vectors gives the basic sub-Gaussian estimate used in the bounded-variation path maximal inequality. ★ signMGF_le
Exponential moment of a finite signed sum
The uniform law on Boolean sign vectors gives the basic sub-Gaussian estimate used in the bounded-variation path maximal inequality.
theorem signMGF_le reviewed
⚑ flagged
Causalean.Stat.Concentration.BoundedVariation
The sign-average exponential moment of a finite Rademacher sum is at most the Gaussian exponential moment with variance equal to the sum of squared coefficients.
Formal statement
Proof (Lean source)
theorem signMGF_le {n : ℕ} (a : Fin n → ℝ) (t : ℝ) :
(∑ σ : Fin n → Bool,
exp (t * ∑ j, (if σ j then (1 : ℝ) else -1) * a j)) /
(2 ^ n : ℝ) ≤
exp (t ^ 2 / 2 * ∑ j, (a j) ^ 2) := by
classical
have hfactor :
(∑ σ : Fin n → Bool,
exp (t * ∑ j, (if σ j then (1 : ℝ) else -1) * a j)) /
(2 ^ n : ℝ) = ∏ j, cosh (t * a j) := by
have hsum :
(∑ σ : Fin n → Bool,
exp (t * ∑ j, (if σ j then (1 : ℝ) else -1) * a j)) =
∏ j, ∑ b : Bool, exp (t * (if b then (1 : ℝ) else -1) * a j) := by
simp_rw [Finset.mul_sum, Real.exp_sum, mul_assoc]
simpa only [mul_assoc] using
(Fintype.prod_sum fun j : Fin n =>
fun b : Bool => exp (t * (if b then (1 : ℝ) else -1) * a j)).symm
rw [hsum]
have htwo : (2 ^ n : ℝ) = ∏ _j : Fin n, (2 : ℝ) := by simp
rw [htwo, ← Finset.prod_div_distrib]
apply Finset.prod_congr rfl
intro j hj
rw [Fintype.sum_bool, Real.cosh_eq]
simp
rw [hfactor]
calc
(∏ j, cosh (t * a j)) ≤ ∏ j, exp ((t * a j) ^ 2 / 2) := by
apply Finset.prod_le_prod
· intro j hj
exact (Real.cosh_pos _).le
· intro j hj
exact Real.cosh_le_exp_half_sq _
_ = exp (t ^ 2 / 2 * ∑ j, (a j) ^ 2) := by
rw [← Real.exp_sum]
congr 1
rw [Finset.mul_sum]
apply Finset.sum_congr rfl
intro j hj
ring
Bilinear 2 core · 1 supporting This module bounds the exponential and nonnegative power moments of bilinear forms in two independent finite Boolean sign vectors. ★ bilinearSignPowAverage_le
Double Rademacher averages for finite matrices
This module bounds the exponential and nonnegative power moments of bilinear forms in two independent finite Boolean sign vectors. The matrix may be banded or fully non-diagonal.
def bilinearSign reviewed
⚑ flagged
Causalean.Stat.Concentration.BoundedVariation.SignMGF
Given a finite real matrix and two Boolean sign vectors, the bilinear signed matrix sum is the sum of each entry weighted by its row and column signs.
theorem bilinearSignPowAverage_le reviewed
⚑ flagged
Causalean.Stat.Concentration.BoundedVariation.SignMGF
Given a finite real matrix whose total absolute coefficient mass is at most one, for every nonnegative integer n, the uniform average over both sign vectors of the n-th power of one plus the bilinear signed matrix sum is at most exp((n^2/2) times the sum over columns of the squared column sums of absolute entries).
Formal statement
Proof (Lean source)
theorem bilinearSignPowAverage_le {r c n : ℕ} (A : Fin r → Fin c → ℝ)
(hmass : ∑ j : Fin c, ∑ i : Fin r, |A i j| ≤ 1) :
(∑ σ : Fin r → Bool, ∑ τ : Fin c → Bool,
(1 + bilinearSign A σ τ) ^ n) /
((2 : ℝ) ^ r * (2 : ℝ) ^ c) ≤
exp ((n : ℝ) ^ 2 / 2 *
∑ j : Fin c, (∑ i : Fin r, |A i j|) ^ 2) := by
classical
have hbil (σ : Fin r → Bool) (τ : Fin c → Bool) :
|bilinearSign A σ τ| ≤ ∑ j : Fin c, ∑ i : Fin r, |A i j| := by
calc
|bilinearSign A σ τ| ≤
∑ j : Fin c, |(if τ j then (1 : ℝ) else -1) *
∑ i, A i j * (if σ i then (1 : ℝ) else -1)| := by
unfold bilinearSign
exact Finset.abs_sum_le_sum_abs _ _
_ = ∑ j : Fin c,
|∑ i : Fin r, A i j * (if σ i then (1 : ℝ) else -1)| := by
apply Finset.sum_congr rfl
intro j hj
simp only [abs_mul]
split_ifs <;> simp
_ ≤ ∑ j : Fin c, ∑ i : Fin r, |A i j| := by
apply Finset.sum_le_sum
intro j hj
calc
_ ≤ ∑ i : Fin r, |A i j * (if σ i then (1 : ℝ) else -1)| :=
Finset.abs_sum_le_sum_abs _ _
_ = ∑ i : Fin r, |A i j| := by
apply Finset.sum_congr rfl
intro i hi
simp only [abs_mul]
split_ifs <;> simp
have hpoint (σ : Fin r → Bool) (τ : Fin c → Bool) :
(1 + bilinearSign A σ τ) ^ n ≤
exp ((n : ℝ) * bilinearSign A σ τ) := by
have hnonneg : 0 ≤ 1 + bilinearSign A σ τ := by
have habs := (hbil σ τ).trans hmass
have hneg := neg_abs_le (bilinearSign A σ τ)
linarith
calc
_ ≤ exp (bilinearSign A σ τ) ^ n := by
apply pow_le_pow_left₀ hnonneg
simpa only [add_comm] using Real.add_one_le_exp (bilinearSign A σ τ)
_ = exp ((n : ℝ) * bilinearSign A σ τ) :=
(Real.exp_nat_mul (bilinearSign A σ τ) n).symm
calc
_ ≤ (∑ σ : Fin r → Bool, ∑ τ : Fin c → Bool,
exp ((n : ℝ) * bilinearSign A σ τ)) /
((2 : ℝ) ^ r * (2 : ℝ) ^ c) := by
apply div_le_div_of_nonneg_right _ (by positivity)
apply Finset.sum_le_sum
intro σ hσ
exact Finset.sum_le_sum (fun τ hτ => hpoint σ τ)
_ ≤ _ := bilinearSignMGF_le A n
1 supporting declaration (lemmas, instances)
-
bilinearSignMGF_letheorem — Given a finite real matrix and a real scale, the double-sign exponential average is bounded by a Gaussian exponential whose variance proxy is the sum of squared column ℓ1 norms.hypothesesProof (Lean source)
theorem bilinearSignMGF_le {r c : ℕ} (A : Fin r → Fin c → ℝ) (t : ℝ) : (∑ σ : Fin r → Bool, ∑ τ : Fin c → Bool, exp (t * bilinearSign A σ τ)) / ((2 : ℝ) ^ r * (2 : ℝ) ^ c) ≤ exp (t ^ 2 / 2 * ∑ j : Fin c, (∑ i : Fin r, |A i j|) ^ 2) := by classical let B (σ : Fin r → Bool) (j : Fin c) : ℝ := ∑ i, A i j * (if σ i then (1 : ℝ) else -1) let V : ℝ := ∑ j : Fin c, (∑ i : Fin r, |A i j|) ^ 2 have hcol (σ : Fin r → Bool) (j : Fin c) : |B σ j| ≤ ∑ i : Fin r, |A i j| := by calc |B σ j| ≤ ∑ i : Fin r, |A i j * (if σ i then (1 : ℝ) else -1)| := Finset.abs_sum_le_sum_abs _ _ _ = ∑ i : Fin r, |A i j| := by apply Finset.sum_congr rfl intro i hi simp only [abs_mul] split_ifs <;> simp have hsq (σ : Fin r → Bool) : (∑ j : Fin c, (B σ j) ^ 2) ≤ V := by apply Finset.sum_le_sum intro j hj have h := pow_le_pow_left₀ (abs_nonneg (B σ j)) (hcol σ j) 2 simpa only [sq_abs] using h have hσ (σ : Fin r → Bool) : (∑ τ : Fin c → Bool, exp (t * bilinearSign A σ τ)) / (2 : ℝ) ^ c ≤ exp (t ^ 2 / 2 * V) := by calc _ = (∑ τ : Fin c → Bool, exp (t * ∑ j, (if τ j then (1 : ℝ) else -1) * B σ j)) / (2 : ℝ) ^ c := rfl _ ≤ exp (t ^ 2 / 2 * ∑ j, (B σ j) ^ 2) := signMGF_le (B σ) t _ ≤ exp (t ^ 2 / 2 * V) := by apply Real.exp_le_exp.mpr exact mul_le_mul_of_nonneg_left (hsq σ) (by positivity) have hdenr : (0 : ℝ) < 2 ^ r := by positivity calc _ = (∑ σ : Fin r → Bool, (∑ τ : Fin c → Bool, exp (t * bilinearSign A σ τ)) / (2 : ℝ) ^ c) / (2 : ℝ) ^ r := by rw [← Finset.sum_div] ring _ ≤ (∑ _σ : Fin r → Bool, exp (t ^ 2 / 2 * V)) / (2 : ℝ) ^ r := by apply div_le_div_of_nonneg_right _ hdenr.le exact Finset.sum_le_sum (fun σ _ => hσ σ) _ = exp (t ^ 2 / 2 * V) := by simp [Fintype.card_bool]