def Talagrand.cube01 (n : ℕ) : Set (Fin n → ℝ)

The Boolean cube $\{0, 1\}^n$ embedded in $\mathbb{R}^n$.

def Talagrand.cubePM (n : ℕ) : Set (Fin n → ℝ)

The signed cube $\{-1, +1\}^n$ embedded in $\mathbb{R}^n$.

def Talagrand.continuousCube01 (n : ℕ) : Set (Fin n → ℝ)

The continuous cube $[0,1]^n$ in $\mathbb{R}^n$.

theorem Talagrand.talagrand_convex_concentration {n : ℕ} (μ : MeasureTheory.Measure (Fin n → ℝ)) [MeasureTheory.IsProbabilityMeasure μ] (hμ : μ (cube01 n)ᶜ = 0) (A : Set (Fin n → ℝ)) (hA : Convex ℝ A) (t : ℝ) (ht : 0 ≤ t) : (μ A).toReal * (μ {x : Fin n → ℝ | t ≤ Metric.infDist x A}).toReal ≤ Real.exp (-t ^ 2 / 4)

Talagrand's inequality for convex sets (Theorem 9.5.3) on the Boolean cube $\{0,1\}^n$: if $A$ is convex, then $\mu(A) \cdot \mu(\{x : \operatorname{dist}(x, A) \geq t\}) \leq e^{-t^2/4}$.

theorem Talagrand.talagrand_convex_concentration_cubePM {n : ℕ} (μ : MeasureTheory.Measure (Fin n → ℝ)) [MeasureTheory.IsProbabilityMeasure μ] (hμ : μ (cubePM n)ᶜ = 0) (A : Set (Fin n → ℝ)) (hA : Convex ℝ A) (t : ℝ) (ht : 0 ≤ t) : (μ A).toReal * (μ {x : Fin n → ℝ | t ≤ Metric.infDist x A}).toReal ≤ Real.exp (-t ^ 2 / 4)

Talagrand's convex-set inequality on the signed cube $\{-1,+1\}^n$: $\mu(A) \cdot \mu(\{x : \operatorname{dist}(x, A) \geq t\}) \leq e^{-t^2/4}$.

theorem Talagrand.talagrand_convex_lipschitz {n : ℕ} (μ : MeasureTheory.Measure (Fin n → ℝ)) [MeasureTheory.IsProbabilityMeasure μ] (hμ : μ (cube01 n)ᶜ = 0) (f : (Fin n → ℝ) → ℝ) (hf_convex : ConvexOn ℝ Set.univ f) (hf_lip : LipschitzWith 1 f) (r t : ℝ) (ht : 0 ≤ t) (hne : {x : Fin n → ℝ | f x ≤ r}.Nonempty) : (μ {x : Fin n → ℝ | f x ≤ r}).toReal * (μ {x : Fin n → ℝ | r + t ≤ f x}).toReal ≤ Real.exp (-t ^ 2 / 4)

Corollary 9.5.6 (concentration for convex $1$-Lipschitz functions on the Boolean cube): $\mu(\{f \leq r\}) \cdot \mu(\{f \geq r + t\}) \leq e^{-t^2/4}$.

def Talagrand.IsMedian {n : ℕ} (μ : MeasureTheory.Measure (Fin n → ℝ)) (f : (Fin n → ℝ) → ℝ) (m : ℝ) : Prop

$m$ is a median of $f$ under $\mu$ if both $\mu(\{f \leq m\}) \geq 1/2$ and $\mu(\{f \geq m\}) \geq 1/2$.

theorem Talagrand.talagrand_upper_tail {n : ℕ} (μ : MeasureTheory.Measure (Fin n → ℝ)) [MeasureTheory.IsProbabilityMeasure μ] (hμ : μ (cube01 n)ᶜ = 0) (f : (Fin n → ℝ) → ℝ) (hf_convex : ConvexOn ℝ Set.univ f) (hf_lip : LipschitzWith 1 f) (m : ℝ) (hm : IsMedian μ f m) (t : ℝ) (ht : 0 ≤ t) (hne : {x : Fin n → ℝ | f x ≤ m}.Nonempty) : (μ {x : Fin n → ℝ | m + t ≤ f x}).toReal ≤ 2 * Real.exp (-t ^ 2 / 4)

Upper-tail concentration about the median for convex $1$-Lipschitz $f$: $\mu(\{f \geq m + t\}) \leq 2 e^{-t^2/4}$.

theorem Talagrand.talagrand_lower_tail {n : ℕ} (μ : MeasureTheory.Measure (Fin n → ℝ)) [MeasureTheory.IsProbabilityMeasure μ] (hμ : μ (cube01 n)ᶜ = 0) (f : (Fin n → ℝ) → ℝ) (hf_convex : ConvexOn ℝ Set.univ f) (hf_lip : LipschitzWith 1 f) (m : ℝ) (hm : IsMedian μ f m) (t : ℝ) (ht : 0 ≤ t) (hne : {x : Fin n → ℝ | f x ≤ m - t}.Nonempty) : (μ {x : Fin n → ℝ | f x ≤ m - t}).toReal ≤ 2 * Real.exp (-t ^ 2 / 4)

Lower-tail concentration about the median for convex $1$-Lipschitz $f$: $\mu(\{f \leq m - t\}) \leq 2 e^{-t^2/4}$.

theorem Talagrand.talagrand_median_concentration {n : ℕ} (μ : MeasureTheory.Measure (Fin n → ℝ)) [MeasureTheory.IsProbabilityMeasure μ] (hμ : μ (cube01 n)ᶜ = 0) (f : (Fin n → ℝ) → ℝ) (hf_convex : ConvexOn ℝ Set.univ f) (hf_lip : LipschitzWith 1 f) (m : ℝ) (hm : IsMedian μ f m) (t : ℝ) (ht : 0 ≤ t) (hne_m : {x : Fin n → ℝ | f x ≤ m}.Nonempty) (hne_mt : {x : Fin n → ℝ | f x ≤ m - t}.Nonempty) : (μ {x : Fin n → ℝ | t ≤ |f x - m|}).toReal ≤ 4 * Real.exp (-t ^ 2 / 4)

Corollary 9.5.8 (two-sided median concentration on the Boolean cube): for convex $1$-Lipschitz $f$ with median $m$, $\mu(\{|f - m| \geq t\}) \leq 4 e^{-t^2/4}$.

theorem Talagrand.talagrand_convex_concentration_continuousCube01 {n : ℕ} (μ : MeasureTheory.Measure (Fin n → ℝ)) [MeasureTheory.IsProbabilityMeasure μ] (hμ : μ (continuousCube01 n)ᶜ = 0) (A : Set (Fin n → ℝ)) (hA : Convex ℝ A) (t : ℝ) (ht : 0 ≤ t) : (μ A).toReal * (μ {x : Fin n → ℝ | t ≤ Metric.infDist x A}).toReal ≤ Real.exp (-t ^ 2 / 4)

Talagrand's convex-set inequality on the continuous cube $[0,1]^n$.

theorem Talagrand.talagrand_convex_lipschitz_continuousCube01 {n : ℕ} (μ : MeasureTheory.Measure (Fin n → ℝ)) [MeasureTheory.IsProbabilityMeasure μ] (hμ : μ (continuousCube01 n)ᶜ = 0) (f : (Fin n → ℝ) → ℝ) (hf_convex : ConvexOn ℝ Set.univ f) (hf_lip : LipschitzWith 1 f) (r t : ℝ) (ht : 0 ≤ t) (hne : {x : Fin n → ℝ | f x ≤ r}.Nonempty) : (μ {x : Fin n → ℝ | f x ≤ r}).toReal * (μ {x : Fin n → ℝ | r + t ≤ f x}).toReal ≤ Real.exp (-t ^ 2 / 4)

Concentration for convex $1$-Lipschitz $f$ on the continuous cube $[0,1]^n$: $\mu(\{f \leq r\}) \cdot \mu(\{f \geq r + t\}) \leq e^{-t^2/4}$.

theorem Talagrand.talagrand_convex_lipschitz_cubePM {n : ℕ} (μ : MeasureTheory.Measure (Fin n → ℝ)) [MeasureTheory.IsProbabilityMeasure μ] (hμ : μ (cubePM n)ᶜ = 0) (f : (Fin n → ℝ) → ℝ) (hf_convex : ConvexOn ℝ Set.univ f) (hf_lip : LipschitzWith 1 f) (r t : ℝ) (ht : 0 ≤ t) (hne : {x : Fin n → ℝ | f x ≤ r}.Nonempty) : (μ {x : Fin n → ℝ | f x ≤ r}).toReal * (μ {x : Fin n → ℝ | r + t ≤ f x}).toReal ≤ Real.exp (-t ^ 2 / 4)

Concentration for convex $1$-Lipschitz $f$ on the signed cube $\{-1,+1\}^n$: $\mu(\{f \leq r\}) \cdot \mu(\{f \geq r + t\}) \leq e^{-t^2/4}$.

theorem Talagrand.talagrand_median_concentration_cubePM {n : ℕ} (μ : MeasureTheory.Measure (Fin n → ℝ)) [MeasureTheory.IsProbabilityMeasure μ] (hμ : μ (cubePM n)ᶜ = 0) (f : (Fin n → ℝ) → ℝ) (hf_convex : ConvexOn ℝ Set.univ f) (hf_lip : LipschitzWith 1 f) (m : ℝ) (hm : IsMedian μ f m) (t : ℝ) (ht : 0 ≤ t) (hne_m : {x : Fin n → ℝ | f x ≤ m}.Nonempty) (hne_mt : {x : Fin n → ℝ | f x ≤ m - t}.Nonempty) : (μ {x : Fin n → ℝ | t ≤ |f x - m|}).toReal ≤ 4 * Real.exp (-t ^ 2 / 4)

Two-sided median concentration on the signed cube $\{-1,+1\}^n$: for convex $1$-Lipschitz $f$ with median $m$, $\mu(\{|f - m| \geq t\}) \leq 4 e^{-t^2/4}$.

theorem Talagrand.sq_sub_le_half_sq (t K : ℝ) : t ^ 2 / 2 - K ^ 2 ≤ (t - K) ^ 2

Elementary inequality: $t^2/2 - K^2 \leq (t - K)^2$ for all real $t, K$.

theorem Talagrand.subgaussian_shift_center {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (X : Ω → ℝ) (m a K : ℝ) (hK : |m - a| ≤ K) (C₁ c₁ : ℝ) (hC₁ : 1 ≤ C₁) (hc₁ : 0 < c₁) (hbound : ∀ (s : ℝ), 0 ≤ s → (μ {ω : Ω | s ≤ |X ω - m|}).toReal ≤ C₁ * Real.exp (-(c₁ * s ^ 2))) (t : ℝ) (ht : 0 ≤ t) : (μ {ω : Ω | t ≤ |X ω - a|}).toReal ≤ C₁ * Real.exp (c₁ * K ^ 2) * Real.exp (-(c₁ / 2 * t ^ 2))

Shifting the centering point of a sub-Gaussian tail bound: if $X$ concentrates about $m$ with constants $(C_1, c_1)$ and $|m - a| \leq K$, then $X$ concentrates about $a$ with adjusted constants, gaining a factor $e^{c_1 K^2}$.

theorem Talagrand.dist_subspace_convex_lipschitz {n : ℕ} (V : Submodule ℝ (Fin n → ℝ)) : (ConvexOn ℝ Set.univ fun (x : Fin n → ℝ) => Metric.infDist x ↑V) ∧ LipschitzWith 1 fun (x : Fin n → ℝ) => Metric.infDist x ↑V

The distance function $x \mapsto \operatorname{dist}(x, V)$ to a linear subspace $V$ is convex and $1$-Lipschitz.

theorem Talagrand.dist_subspace_median_bound {n : ℕ} (μ : MeasureTheory.Measure (Fin n → ℝ)) [MeasureTheory.IsProbabilityMeasure μ] (hμ : μ (cubePM n)ᶜ = 0) (V : Submodule ℝ (Fin n → ℝ)) (d : ℕ) (hd : Module.finrank ℝ ↥V = d) (hdn : d < n) : ∃ (m : ℝ), IsMedian μ (fun (x : Fin n → ℝ) => Metric.infDist x ↑V) m ∧ |m - √↑(n - d)| ≤ 1

For a $d$-dimensional subspace $V$ with $d < n$, the median $m$ of $x \mapsto \operatorname{dist}(x, V)$ on the signed cube satisfies $|m - \sqrt{n - d}| \leq 1$.

theorem Talagrand.dist_subspace_sublevel_nonempty {n : ℕ} (V : Submodule ℝ (Fin n → ℝ)) (r : ℝ) : {x : Fin n → ℝ | (fun (x : Fin n → ℝ) => Metric.infDist x ↑V) x ≤ r}.Nonempty

Any sublevel set $\{x : \operatorname{dist}(x, V) \leq r\}$ of the distance-to-subspace function is nonempty (it contains $0 \in V$).

theorem Talagrand.dist_subspace_concentration {n : ℕ} (μ : MeasureTheory.Measure (Fin n → ℝ)) [MeasureTheory.IsProbabilityMeasure μ] (hμ : μ (cubePM n)ᶜ = 0) (V : Submodule ℝ (Fin n → ℝ)) (d : ℕ) (hd : Module.finrank ℝ ↥V = d) (hdn : d < n) : ∃ (C : ℝ) (c : ℝ), 0 < C ∧ 0 < c ∧ ∀ (t : ℝ), 0 ≤ t → (μ {x : Fin n → ℝ | t ≤ |Metric.infDist x ↑V - √↑(n - d)|}).toReal ≤ C * Real.exp (-(c * t ^ 2))

Sub-Gaussian concentration of $\operatorname{dist}(x, V)$ about $\sqrt{n-d}$ on the signed cube $\{-1,+1\}^n$, for any $d$-dimensional subspace $V$ with $d < n$.

theorem Talagrand.talagrand_convex_set_concentration {n : ℕ} (μ : MeasureTheory.Measure (Fin n → ℝ)) [MeasureTheory.IsProbabilityMeasure μ] (hμ : μ (continuousCube01 n)ᶜ = 0) (A : Set (Fin n → ℝ)) (hA : Convex ℝ A) (t : ℝ) (ht : 0 ≤ t) : (μ A).toReal * (μ {x : Fin n → ℝ | t ≤ Metric.infDist x A}).toReal ≤ Real.exp (-t ^ 2 / 4)

Talagrand's convex-set inequality on the continuous cube $[0,1]^n$ (alias of talagrand_convex_concentration_continuousCube01).

theorem Talagrand.talagrand_convex_lipschitz_concentration {n : ℕ} (μ : MeasureTheory.Measure (Fin n → ℝ)) [MeasureTheory.IsProbabilityMeasure μ] (hμ : μ (continuousCube01 n)ᶜ = 0) (f : (Fin n → ℝ) → ℝ) (hf_convex : ConvexOn ℝ Set.univ f) (hf_lip : LipschitzWith 1 f) (m : ℝ) (hm : IsMedian μ f m) (t : ℝ) (ht : 0 ≤ t) : (μ {x : Fin n → ℝ | t ≤ |f x - m|}).toReal ≤ 4 * Real.exp (-t ^ 2 / 4)

Two-sided median concentration for convex $1$-Lipschitz $f$ on the continuous cube $[0,1]^n$: $\mu(\{|f - m| \geq t\}) \leq 4 e^{-t^2/4}$.

theorem Talagrand.talagrand_convex_lipschitz_combined {n : ℕ} (μ : MeasureTheory.Measure (Fin n → ℝ)) [MeasureTheory.IsProbabilityMeasure μ] (hμ : μ (continuousCube01 n)ᶜ = 0) (A : Set (Fin n → ℝ)) (hA : Convex ℝ A) (t : ℝ) (ht : 0 ≤ t) (f : (Fin n → ℝ) → ℝ) (hf_convex : ConvexOn ℝ Set.univ f) (hf_lip : LipschitzWith 1 f) (m : ℝ) (hm : IsMedian μ f m) : (μ A).toReal * (μ {x : Fin n → ℝ | t ≤ Metric.infDist x A}).toReal ≤ Real.exp (-t ^ 2 / 4) ∧ (μ {x : Fin n → ℝ | t ≤ |f x - m|}).toReal ≤ 4 * Real.exp (-t ^ 2 / 4)

Combined Talagrand inequality on $[0,1]^n$: the convex-set bound together with the median concentration for convex $1$-Lipschitz functions.