Documentation

Atlas.HighDimensionalStatistics.code.Chapter1.Thm_1_16

Helper lemmas #

theorem SubGaussianPolytope.polytope_sup_subset_vertex_sup {Ω : Type u_1} {E : Type u_2} [AddCommGroup E] [Module ℝ E] (g : Ω → E →ₗ[ℝ] ℝ) (S : Finset E) (t : ℝ) :
{ω : Ω | ∃ θ ∈ (convexHull ℝ) ↑S, (g ω) θ > t} ⊆ {ω : Ω | ∃ v ∈ S, (g ω) v > t}

For each outcome ω, if the linear functional g(ω) exceeds threshold t at some point θ in the convex hull of S, then by Lemma 1.15 it also exceeds t at some vertex v ∈ S.

theorem SubGaussianPolytope.setOf_bexists_eq_biUnion {Ω : Type u_1} {E : Type u_2} (S : Finset E) (P : E → Ω → Prop) :
{ω : Ω | ∃ v ∈ S, P v ω} = ⋃ v ∈ ↑S, {ω : Ω | P v ω}

Set-theoretic identity: {ω | ∃ v ∈ S, P v ω} = ⋃ v ∈ ↑S, {ω | P v ω}.

theorem SubGaussianPolytope.sup'_equivFin_eq {E : Type u_1} (S : Finset E) (hS : S.Nonempty) (f : E → ℝ) :
have this := ⋯; S.sup' hS f = Finset.univ.sup' ⋯ fun (i : Fin S.card) => f ↑(S.equivFin.symm i)

The sup' over a finset S equals the sup' over Finset.univ via S.equivFin.

Part (c): Tail probability bound #

theorem SubGaussianPolytope.tail_bound {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {E : Type u_2} [AddCommGroup E] [Module ℝ E] (g : Ω → E →ₗ[ℝ] ℝ) (S : Finset E) {σsq : ℝ} (hsg : ∀ v ∈ S, IsSubGaussian (fun (ω : Ω) => (g ω) v) σsq μ) (t : ℝ) (ht : 0 < t) :
μ {ω : Ω | ∃ θ ∈ (convexHull ℝ) ↑S, (g ω) θ > t} ≤ S.card • ENNReal.ofReal (Real.exp (-(t ^ 2 / (2 * σsq))))

Theorem 1.16(c): Sub-Gaussian tail bound over polytope. P(max_{θ ∈ conv(S)} g(ω)(θ) > t) ≤ N · exp(-t²/(2σ²))

theorem SubGaussianPolytope.tail_bound' {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {E : Type u_2} [AddCommGroup E] [Module ℝ E] (g : Ω → E →ₗ[ℝ] ℝ) (S : Finset E) {σsq : ℝ} (hsg : ∀ v ∈ S, IsSubGaussian (fun (ω : Ω) => (g ω) v) σsq μ) (t : ℝ) (ht : 0 < t) :
μ {ω : Ω | ∃ θ ∈ (convexHull ℝ) ↑S, (g ω) θ > t} ≤ ENNReal.ofReal (↑S.card * Real.exp (-(t ^ 2 / (2 * σsq))))

Theorem 1.16(c) (alternative formulation with ENNReal.ofReal (S.card * ...)).

Part (a): Expectation bound (one-sided) #

theorem SubGaussianPolytope.expectation_sup_parametric {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {E : Type u_2} [AddCommGroup E] [Module ℝ E] (g : Ω → E →ₗ[ℝ] ℝ) (S : Finset E) (hS : S.Nonempty) {σsq : ℝ} (hσ : 0 ≤ σsq) (hsg : ∀ v ∈ S, IsSubGaussian (fun (ω : Ω) => (g ω) v) σsq μ) (s : ℝ) (hs : 0 < s) :
∫ (ω : Ω), S.sup' hS fun (v : E) => (g ω) v ∂μ ≤ Real.log ↑S.card / s + σsq * s / 2

Parametric bound for sup over finset: for any s > 0, E[sup_{v ∈ S} g(ω)(v)] ≤ log(S.card)/s + σ²·s/2.

theorem SubGaussianPolytope.expectation_max_bound {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {E : Type u_2} [AddCommGroup E] [Module ℝ E] (g : Ω → E →ₗ[ℝ] ℝ) (S : Finset E) (hS : S.Nonempty) {σsq : ℝ} (hσ : 0 ≤ σsq) (hsg : ∀ v ∈ S, IsSubGaussian (fun (ω : Ω) => (g ω) v) σsq μ) :
∫ (ω : Ω), S.sup' hS fun (v : E) => (g ω) v ∂μ ≤ √σsq * √(2 * Real.log ↑S.card)

Theorem 1.16(a): E[max_{θ ∈ conv(S)} g(ω)(θ)] ≤ √σ² · √(2 log N).

Part (b): Expectation bound (absolute value) #

theorem SubGaussianPolytope.expectation_abs_sup_parametric {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {E : Type u_2} [AddCommGroup E] [Module ℝ E] (g : Ω → E →ₗ[ℝ] ℝ) (S : Finset E) (hS : S.Nonempty) {σsq : ℝ} (hσ : 0 ≤ σsq) (hsg : ∀ v ∈ S, IsSubGaussian (fun (ω : Ω) => (g ω) v) σsq μ) (s : ℝ) (hs : 0 < s) :
∫ (ω : Ω), S.sup' hS fun (v : E) => |(g ω) v| ∂μ ≤ Real.log (2 * ↑S.card) / s + σsq * s / 2

Parametric bound for abs-sup over finset: E[sup_{v ∈ S} |g(ω)(v)|] ≤ log(2·S.card)/s + σ²·s/2.

theorem SubGaussianPolytope.expectation_abs_max_bound {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {E : Type u_2} [AddCommGroup E] [Module ℝ E] (g : Ω → E →ₗ[ℝ] ℝ) (S : Finset E) (hS : S.Nonempty) {σsq : ℝ} (hσ : 0 ≤ σsq) (hsg : ∀ v ∈ S, IsSubGaussian (fun (ω : Ω) => (g ω) v) σsq μ) :
∫ (ω : Ω), S.sup' hS fun (v : E) => |(g ω) v| ∂μ ≤ √σsq * √(2 * Real.log (2 * ↑S.card))

Theorem 1.16(b): E[max_{θ ∈ conv(S)} |g(ω)(θ)|] ≤ √σ² · √(2 log(2N)).

Part (d): Absolute value tail probability bound #

theorem SubGaussianPolytope.polytope_abs_sup_subset_vertex_abs_sup {Ω : Type u_1} {E : Type u_2} [AddCommGroup E] [Module ℝ E] (g : Ω → E →ₗ[ℝ] ℝ) (S : Finset E) (t : ℝ) :
{ω : Ω | ∃ θ ∈ (convexHull ℝ) ↑S, |(g ω) θ| > t} ⊆ {ω : Ω | ∃ v ∈ S, |(g ω) v| > t}

For each outcome ω, if the absolute value |g(ω)(θ)| exceeds threshold t at some point θ in the convex hull of S, then |g(ω)(v)| also exceeds t at some vertex v ∈ S. This follows by case-splitting on the sign: if g(ω)(θ) > t, use Lemma 1.15 to find v with g(ω)(v) ≥ g(ω)(θ) > t; if g(ω)(θ) < -t, use Lemma 1.15 on -g(ω) to find v with g(ω)(v) ≤ g(ω)(θ) < -t.

theorem SubGaussianPolytope.abs_tail_bound {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {E : Type u_2} [AddCommGroup E] [Module ℝ E] (g : Ω → E →ₗ[ℝ] ℝ) (S : Finset E) {σsq : ℝ} (hsg : ∀ v ∈ S, IsSubGaussian (fun (ω : Ω) => (g ω) v) σsq μ) (t : ℝ) (ht : 0 < t) :
μ {ω : Ω | ∃ θ ∈ (convexHull ℝ) ↑S, |(g ω) θ| > t} ≤ ENNReal.ofReal (2 * ↑S.card * Real.exp (-(t ^ 2 / (2 * σsq))))

Theorem 1.16(d): Sub-Gaussian absolute-value tail bound over polytope. P(max_{θ ∈ conv(S)} |g(ω)(θ)| > t) ≤ 2N · exp(-t²/(2σ²))

Bundled theorem #

theorem SubGaussianPolytope.theorem_1_16 {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {E : Type u_2} [AddCommGroup E] [Module ℝ E] (g : Ω → E →ₗ[ℝ] ℝ) (S : Finset E) (hS : S.Nonempty) {σsq : ℝ} (hσ : 0 ≤ σsq) (hsg : ∀ v ∈ S, IsSubGaussian (fun (ω : Ω) => (g ω) v) σsq μ) (t : ℝ) (ht : 0 < t) :
∫ (ω : Ω), S.sup' hS fun (v : E) => (g ω) v ∂μ ≤ √σsq * √(2 * Real.log ↑S.card) ∧ ∫ (ω : Ω), S.sup' hS fun (v : E) => |(g ω) v| ∂μ ≤ √σsq * √(2 * Real.log (2 * ↑S.card)) ∧ μ {ω : Ω | ∃ θ ∈ (convexHull ℝ) ↑S, (g ω) θ > t} ≤ S.card • ENNReal.ofReal (Real.exp (-(t ^ 2 / (2 * σsq)))) ∧ μ {ω : Ω | ∃ θ ∈ (convexHull ℝ) ↑S, |(g ω) θ| > t} ≤ ENNReal.ofReal (2 * ↑S.card * Real.exp (-(t ^ 2 / (2 * σsq))))

Theorem 1.16 (Sub-Gaussian polytope bound).

Let P be a polytope with N vertices and X a sub-Gaussian random vector with variance proxy σ². Then:

  • (a) E[max_{θ∈P} θ⊤X] ≤ σ√(2 log N)
  • (b) E[max_{θ∈P} |θ⊤X|] ≤ σ√(2 log(2N))
  • (c) P(max_{θ∈P} θ⊤X > t) ≤ N · exp(-t²/(2σ²))
  • (d) P(max_{θ∈P} |θ⊤X| > t) ≤ 2N · exp(-t²/(2σ²))

Backward-compatible aliases for downstream files #

theorem theorem_1_16_polytope_subgaussian {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {E : Type u_2} [AddCommGroup E] [Module ℝ E] (g : Ω → E →ₗ[ℝ] ℝ) (S : Finset E) {σsq : ℝ} (hsg : ∀ v ∈ S, IsSubGaussian (fun (ω : Ω) => (g ω) v) σsq μ) (t : ℝ) (ht : 0 < t) :
μ {ω : Ω | ∃ θ ∈ (convexHull ℝ) ↑S, (g ω) θ > t} ≤ S.card • ENNReal.ofReal (Real.exp (-(t ^ 2 / (2 * σsq))))

Alias for SubGaussianPolytope.tail_bound.

theorem theorem_1_16_polytope_subgaussian' {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {E : Type u_2} [AddCommGroup E] [Module ℝ E] (g : Ω → E →ₗ[ℝ] ℝ) (S : Finset E) {σsq : ℝ} (hsg : ∀ v ∈ S, IsSubGaussian (fun (ω : Ω) => (g ω) v) σsq μ) (t : ℝ) (ht : 0 < t) :
μ {ω : Ω | ∃ θ ∈ (convexHull ℝ) ↑S, (g ω) θ > t} ≤ ENNReal.ofReal (↑S.card * Real.exp (-(t ^ 2 / (2 * σsq))))

Alias for SubGaussianPolytope.tail_bound'.

theorem theorem_1_16_expectation_max {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {E : Type u_2} [AddCommGroup E] [Module ℝ E] (g : Ω → E →ₗ[ℝ] ℝ) (S : Finset E) (hS : S.Nonempty) {σsq : ℝ} (hσ : 0 ≤ σsq) (hsg : ∀ v ∈ S, IsSubGaussian (fun (ω : Ω) => (g ω) v) σsq μ) :
∫ (ω : Ω), S.sup' hS fun (v : E) => (g ω) v ∂μ ≤ √σsq * √(2 * Real.log ↑S.card)

Alias for SubGaussianPolytope.expectation_max_bound.

theorem theorem_1_16_expectation_abs_max {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {E : Type u_2} [AddCommGroup E] [Module ℝ E] (g : Ω → E →ₗ[ℝ] ℝ) (S : Finset E) (hS : S.Nonempty) {σsq : ℝ} (hσ : 0 ≤ σsq) (hsg : ∀ v ∈ S, IsSubGaussian (fun (ω : Ω) => (g ω) v) σsq μ) :
∫ (ω : Ω), S.sup' hS fun (v : E) => |(g ω) v| ∂μ ≤ √σsq * √(2 * Real.log (2 * ↑S.card))

Alias for SubGaussianPolytope.expectation_abs_max_bound.