def TalagrandWeightedCertificates.weightedHammingDist {n : ℕ} {Ω : Fin n → Type u_1} [(i : Fin n) → DecidableEq (Ω i)] (α : Fin n → ℝ) (x y : (i : Fin n) → Ω i) : ℝ

The weighted Hamming distance between $x$ and $y$ with weights $α$: $d_α(x, y) = \sum_{i : x_i \neq y_i} α_i$.

noncomputable def TalagrandWeightedCertificates.eucNorm {n : ℕ} (α : Fin n → ℝ) : ℝ

The Euclidean ($ℓ^2$) norm of the weight vector $α$: $\|α\|_2 = \sqrt{\sum_i α_i^2}$.

noncomputable def TalagrandWeightedCertificates.weightedDistToSet {n : ℕ} {Ω : Fin n → Type u_1} [(i : Fin n) → DecidableEq (Ω i)] (α : Fin n → ℝ) (x : (i : Fin n) → Ω i) (A : Set ((i : Fin n) → Ω i)) : ℝ

The weighted Hamming distance from $x$ to a set $A$: $d_α(x, A) = \inf_{y \in A} d_α(x, y)$.

noncomputable def TalagrandWeightedCertificates.convexDist {n : ℕ} {Ω : Fin n → Type u_1} [(i : Fin n) → DecidableEq (Ω i)] (x : (i : Fin n) → Ω i) (A : Set ((i : Fin n) → Ω i)) : ℝ

Talagrand's convex distance from $x$ to $A$, defined as the supremum of the weighted distances $d_α(x, A)$ over all unit-norm weight vectors: $d_T(x, A) = \sup_{\|α\|_2 = 1} d_α(x, A)$.

def TalagrandWeightedCertificates.HasWeightedCertificates {n : ℕ} {Ω : Fin n → Type u_1} [(i : Fin n) → DecidableEq (Ω i)] (f : ((i : Fin n) → Ω i) → ℝ) (K : ℝ) : Prop

The function $f$ admits weighted certificates with constant $K$: for every $x$ there exist nonnegative weights $α(x)$ with $\|α(x)\|_2 \leq K/2$ such that for all $y$, $f(y) \geq f(x) - \sum_{i : x_i \neq y_i} α_i(x)$.

theorem TalagrandWeightedCertificates.talagrand_convex_distance_inequality {n : ℕ} {Ω : Fin n → Type u_2} [(i : Fin n) → DecidableEq (Ω i)] [(i : Fin n) → MeasurableSpace (Ω i)] (μ : (i : Fin n) → MeasureTheory.Measure (Ω i)) [∀ (i : Fin n), MeasureTheory.IsProbabilityMeasure (μ i)] (A : Set ((i : Fin n) → Ω i)) (t : ℝ) (ht : 0 ≤ t) : ((MeasureTheory.Measure.pi μ) A).toReal * ((MeasureTheory.Measure.pi μ) {x : (i : Fin n) → Ω i | convexDist x A ≥ t}).toReal ≤ Real.exp (-t ^ 2 / 4)

Talagrand's convex-distance inequality (Theorem 9.5.11): for any product probability measure on $\prod_i Ω_i$ and any set $A$, $\mu(A) \cdot \mu(\{x : d_T(x, A) \geq t\}) \leq e^{-t^2 / 4}$.

theorem TalagrandWeightedCertificates.certificate_convexDist_bound {n : ℕ} {Ω : Fin n → Type u_2} [(i : Fin n) → DecidableEq (Ω i)] (f : ((i : Fin n) → Ω i) → ℝ) (K : ℝ) (hK : 0 < K) (hcert : HasWeightedCertificates f K) (x : (i : Fin n) → Ω i) (r t : ℝ) (hfx : f x ≥ r) : convexDist x {y : (i : Fin n) → Ω i | f y ≤ r - t} ≥ 2 * t / K

If $f$ has weighted certificates with constant $K$ and $f(x) \geq r$, then the convex distance from $x$ to the sublevel set $\{f \leq r - t\}$ is at least $2t/K$.

theorem TalagrandWeightedCertificates.median_argument (prob_le_m prob_ge_mt prob_le_mt prob_ge_m K t : ℝ) (hprod1 : prob_le_m * prob_ge_mt ≤ Real.exp (-t ^ 2 / K ^ 2)) (hprod2 : prob_le_mt * prob_ge_m ≤ Real.exp (-t ^ 2 / K ^ 2)) (hmed_le : prob_le_m ≥ 1 / 2) (hmed_ge : prob_ge_m ≥ 1 / 2) : prob_ge_mt + prob_le_mt ≤ 4 * Real.exp (-t ^ 2 / K ^ 2)

Combining the two one-sided product bounds with the median property $\mathbb{P}(f \leq m), \mathbb{P}(f \geq m) \geq 1/2$ yields the two-sided tail bound $\mathbb{P}(f \geq m+t) + \mathbb{P}(f \leq m-t) \leq 4 e^{-t^2 / K^2}$.

theorem TalagrandWeightedCertificates.talagrand_weighted_certificates {n : ℕ} {Ω : Fin n → Type u_2} [(i : Fin n) → DecidableEq (Ω i)] [(i : Fin n) → MeasurableSpace (Ω i)] (μ : (i : Fin n) → MeasureTheory.Measure (Ω i)) [∀ (i : Fin n), MeasureTheory.IsProbabilityMeasure (μ i)] (f : ((i : Fin n) → Ω i) → ℝ) (K : ℝ) (hK : 0 < K) (hcert : HasWeightedCertificates f K) (m : ℝ) (hmed_le : ((MeasureTheory.Measure.pi μ) {x : (i : Fin n) → Ω i | f x ≤ m}).toReal ≥ 1 / 2) (hmed_ge : ((MeasureTheory.Measure.pi μ) {x : (i : Fin n) → Ω i | f x ≥ m}).toReal ≥ 1 / 2) (t : ℝ) (ht : 0 ≤ t) : ((MeasureTheory.Measure.pi μ) {x : (i : Fin n) → Ω i | |f x - m| ≥ t}).toReal ≤ 4 * Real.exp (-t ^ 2 / K ^ 2)

Theorem 9.5.14 (Talagrand's inequality with weighted certificates): if $f$ has weighted certificates with constant $K$ and $m$ is a median of $f$, then $\mu(\{x : |f(x) - m| \geq t\}) \leq 4 e^{-t^2 / K^2}$.