@[reducible, inline]

abbrev LipschitzFunctions.IsLipschitz {X : Type u_1} {Y : Type u_2} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] (C : NNReal) (f : X → Y) : Prop

Definition 9.4.7 (Lipschitz functions). A function $f : X \to Y$ is $C$-Lipschitz iff $d(f(x), f(y)) \le C \cdot d(x, y)$ for all $x, y \in X$.

theorem LipschitzFunctions.concentration_equivalence {Ω : Type u_1} [PseudoMetricSpace Ω] [MeasurableSpace Ω] [BorelSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {t : ℝ} (ht : 0 ≤ t) {ε : ENNReal} : (∀ (A : Set Ω), MeasurableSet A → μ A ≥ 1 / 2 → μ (Metric.cthickening t A) ≥ 1 - ε) ↔ ∀ (f : Ω → ℝ) (m : ℝ), LipschitzWith 1 f → Measurable f → μ {x : Ω | f x ≤ m} ≥ 1 / 2 → μ {x : Ω | f x > m + t} ≤ ε

Theorem 9.4.8 (concentration equivalence). For a probability measure on a metric space and any $t \ge 0$, the set-expansion concentration statement $\mu(A) \ge 1/2 \Rightarrow \mu(A_t) \ge 1 - \varepsilon$ is equivalent to the median concentration statement $\mu(f \le m) \ge 1/2 \Rightarrow \mu(f > m + t) \le \varepsilon$ for all $1$-Lipschitz $f$, where $A_t$ is the closed $t$-thickening of $A$.