def GaussianIsoperimetric.IsHalfSpace {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (H : Set E) : Prop

A set $H \subseteq E$ is a half-space if it has the form $\{x : \langle v, x \rangle \leq c\}$ for some nonzero $v$ and real $c$.

theorem GaussianIsoperimetric.gaussian_isoperimetric_inequality {n : ℕ} {A H : Set (EuclideanSpace ℝ (Fin n))} (hA : MeasurableSet A) (hH : IsHalfSpace H) (hAH : (ProbabilityTheory.stdGaussian (EuclideanSpace ℝ (Fin n))) A = (ProbabilityTheory.stdGaussian (EuclideanSpace ℝ (Fin n))) H) {t : ℝ} (ht : 0 ≤ t) : (ProbabilityTheory.stdGaussian (EuclideanSpace ℝ (Fin n))) (Metric.cthickening t A) ≥ (ProbabilityTheory.stdGaussian (EuclideanSpace ℝ (Fin n))) (Metric.cthickening t H)

Gaussian isoperimetric inequality (Theorem 9.4.15): among all measurable sets $A$ of a given standard Gaussian measure, half-spaces minimize the Gaussian measure of the $t$-thickening. That is, if $\gamma(A) = \gamma(H)$ for a half-space $H$, then $\gamma(A_t) \geq \gamma(H_t)$ for every $t \geq 0$.

theorem GaussianIsoperimetric.gaussian_concentration_lipschitz {n : ℕ} (f : EuclideanSpace ℝ (Fin n) → ℝ) (hf : LipschitzWith 1 f) : ∃ (m : ℝ), ∀ (t : ℝ), 0 ≤ t → (ProbabilityTheory.stdGaussian (EuclideanSpace ℝ (Fin n))) {z : EuclideanSpace ℝ (Fin n) | t ≤ |f z - m|} ≤ ENNReal.ofReal (2 * Real.exp (-t ^ 2 / 2))

Gaussian concentration for Lipschitz functions (Corollary 9.4.16): if $f$ is $1$-Lipschitz on $\mathbb{R}^n$ and $Z$ is a standard Gaussian vector, there exists a median $m$ such that $\mathbb{P}(|f(Z) - m| \geq t) \leq 2e^{-t^2/2}$ for all $t \geq 0$.