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

A function $f$ is Hamming-Lipschitz if $|f(x) - f(y)|$ is at most the Hamming distance between $x$ and $y$ (the number of coordinates where they differ).

def TalagrandCertifiable.UpperLevelCertifiable {n : ℕ} {Ω : Fin n → Type u_1} [(i : Fin n) → DecidableEq (Ω i)] (f : ((i : Fin n) → Ω i) → ℝ) (r : ℝ) (s : ℕ) : Prop

The upper level set $\{x : f(x) \geq r\}$ is $s$-certifiable (Definition 9.5.20).

theorem TalagrandCertifiable.certifiable_convexDist_bound {n : ℕ} {Ω : Fin n → Type u_1} [(i : Fin n) → DecidableEq (Ω i)] (f : ((i : Fin n) → Ω i) → ℝ) (s : ℕ) (hs : 0 < s) (hf_lip : IsHammingLipschitz f) (r t : ℝ) (ht : 0 ≤ t) (hcert : UpperLevelCertifiable f r s) (y : (i : Fin n) → Ω i) (hfy : f y ≥ r) : TalagrandWeightedCertificates.convexDist y {x : (i : Fin n) → Ω i | f x ≤ r - t} ≥ t / √↑s

Key lemma for Talagrand's certifiable functions inequality: if $\{f \geq r\}$ is $s$-certifiable, $f$ is Hamming-Lipschitz, and $f(y) \geq r$, then the convex distance from $y$ to $\{f \leq r - t\}$ is at least $t / \sqrt{s}$.

theorem TalagrandCertifiable.talagrand_certifiable {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) → ℝ) (hf_lip : IsHammingLipschitz f) (r : ℝ) (s : ℕ) (hs : 0 < s) (hcert : UpperLevelCertifiable f r s) (t : ℝ) (ht : 0 ≤ t) : ((MeasureTheory.Measure.pi μ) {x : (i : Fin n) → Ω i | f x ≤ r - t}).toReal * ((MeasureTheory.Measure.pi μ) {x : (i : Fin n) → Ω i | f x ≥ r}).toReal ≤ Real.exp (-t ^ 2 / (4 * ↑s))

Talagrand's inequality for $s$-certifiable Hamming-Lipschitz functions (Theorem 9.5.21): $\mathbb{P}(f \leq r - t) \cdot \mathbb{P}(f \geq r) \leq \exp(-t^2 / (4s))$.

def TalagrandCertifiable.IsMedianPi {n : ℕ} {Ω : Fin n → Type u_2} [(i : Fin n) → MeasurableSpace (Ω i)] (μ : (i : Fin n) → MeasureTheory.Measure (Ω i)) (f : ((i : Fin n) → Ω i) → ℝ) (m : ℝ) : Prop

$m$ is a median of $f$ under the product measure $\prod_i \mu_i$: both $\{f \leq m\}$ and $\{f \geq m\}$ have probability at least $1/2$.

theorem TalagrandCertifiable.talagrand_certifiable_corollary {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) → ℝ) (hf_lip : IsHammingLipschitz f) (m : ℝ) (hm : IsMedianPi μ f m) (hm_pos : 1 ≤ m) (hcert : ∀ (r : ℝ), 0 < r → UpperLevelCertifiable f r ⌊r⌋₊) (t : ℝ) (ht : 0 ≤ t) : ((MeasureTheory.Measure.pi μ) {x : (i : Fin n) → Ω i | f x ≤ m - t}).toReal ≤ 2 * Real.exp (-t ^ 2 / (4 * m)) ∧ ((MeasureTheory.Measure.pi μ) {x : (i : Fin n) → Ω i | f x ≥ m + t}).toReal ≤ 2 * Real.exp (-t ^ 2 / (4 * (m + t)))

Corollary 9.5.22: two-sided concentration around the median for Hamming-Lipschitz functions whose upper level sets are $\lfloor r \rfloor$-certifiable: $\mathbb{P}(f \leq m - t) \leq 2\exp(-t^2/(4m))$ and $\mathbb{P}(f \geq m + t) \leq 2\exp(-t^2/(4(m+t)))$.

theorem TalagrandCertifiable.tail_sum_small (K : ℝ) (hK : 0 < K) (ε : ℝ) (hε : 0 < ε) : ∃ (C : ℝ), 0 < C ∧ 2 * Real.exp (-C ^ 2 / (4 * K)) + 2 * Real.exp (-C ^ 2 / (4 * (K + C))) ≤ ε

Technical lemma: for any $K > 0$ and $\varepsilon > 0$, one can choose $C$ large enough that $2\exp(-C^2/(4K)) + 2\exp(-C^2/(4(K+C))) \leq \varepsilon$.

theorem TalagrandCertifiable.lis_concentration {n : ℕ} (hn : 1 ≤ n) {Ω : Fin n → Type u_2} [(i : Fin n) → MeasurableSpace (Ω i)] (μ : (i : Fin n) → MeasureTheory.Measure (Ω i)) [∀ (i : Fin n), MeasureTheory.IsProbabilityMeasure (μ i)] (f : ((i : Fin n) → Ω i) → ℝ) (m : ℝ) (hm_pos : 1 ≤ m) (K : ℝ) (hK : 0 < K) (hm_bound : m ≤ K * √↑n) (h_lower : ∀ (t : ℝ), 0 ≤ t → ((MeasureTheory.Measure.pi μ) {x : (i : Fin n) → Ω i | f x ≤ m - t}).toReal ≤ 2 * Real.exp (-t ^ 2 / (4 * m))) (h_upper : ∀ (t : ℝ), 0 ≤ t → ((MeasureTheory.Measure.pi μ) {x : (i : Fin n) → Ω i | f x ≥ m + t}).toReal ≤ 2 * Real.exp (-t ^ 2 / (4 * (m + t)))) (ε : ℝ) (hε : 0 < ε) : ∃ (C : ℝ), 0 < C ∧ ((MeasureTheory.Measure.pi μ) {x : (i : Fin n) → Ω i | |f x - m| > C * ↑n ^ (1 / 4)}).toReal ≤ ε

Concentration of the longest-increasing-subsequence-type statistic: if the median $m$ of $f$ satisfies $m \leq K\sqrt{n}$ and the Talagrand tail bounds hold, then for every $\varepsilon > 0$ there exists $C$ such that $\mathbb{P}(|f - m| > C n^{1/4}) \leq \varepsilon$.