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} {ω : Ω | vS, (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) :
{ω : Ω | vS, P v ω} = vS, {ω : Ω | 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 : vS, 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 : vS, 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 : } ( : 0 σsq) (hsg : vS, 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 : } ( : 0 σsq) (hsg : vS, 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 : } ( : 0 σsq) (hsg : vS, 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 : } ( : 0 σsq) (hsg : vS, 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} {ω : Ω | vS, |(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 : vS, 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 : } ( : 0 σsq) (hsg : vS, 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 : vS, 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 : vS, 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 : } ( : 0 σsq) (hsg : vS, 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 : } ( : 0 σsq) (hsg : vS, 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.