def SubGaussian.IsSubGaussian {Ω : Type u_1} [MeasurableSpace Ω] (X : Ω → ℝ) (K : ℝ) (μ : MeasureTheory.Measure Ω) : Prop

Definition 9.4.17 ($K$-sub-Gaussian random variable). A real-valued random variable $X$ is $K$-sub-Gaussian if for every $t \ge 0$, $\mathbb{P}(|X - \mathbb{E} X| \ge t) \le 2 \exp(-t^2 / K^2)$.

def SubGaussian.HasSubGaussianTail {Ω : Type u_1} [MeasurableSpace Ω] (X : Ω → ℝ) (m K : ℝ) (μ : MeasureTheory.Measure Ω) : Prop

Sub-Gaussian tail bound around an arbitrary center $m$: for every $t \ge 0$, $\mathbb{P}(|X - m| \ge t) \le 2 \exp(-t^2 / K^2)$.

def SubGaussian.IsMedian {Ω : Type u_1} [MeasurableSpace Ω] (X : Ω → ℝ) (med : ℝ) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] : Prop

$\mathrm{med}$ is a median of $X$ if $\mathbb{P}(X \ge \mathrm{med}) \ge 1/2$ and $\mathbb{P}(X \le \mathrm{med}) \ge 1/2$.

theorem SubGaussian.log2_lt_one : Real.log 2 < 1

Numerical fact $\log 2 < 1$.

theorem SubGaussian.two_mul_exp_neg_lt_half {r : ℝ} (hr : 2 * Real.log 2 < r) : 2 * Real.exp (-r) < 1 / 2

For $r > 2 \log 2$, we have $2 \exp(-r) < 1/2$.

theorem SubGaussian.one_le_two_mul_exp_neg {r : ℝ} (hr : r ≤ Real.log 2) : 1 ≤ 2 * Real.exp (-r)

For $r \le \log 2$, we have $1 \le 2 \exp(-r)$.

theorem SubGaussian.median_close_to_center {Ω : Type u_1} [MeasurableSpace Ω] {X : Ω → ℝ} {m K : ℝ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (hK : 0 < K) (htail : HasSubGaussianTail X m K μ) {med : ℝ} (hmed : IsMedian X med μ) : |med - m| ≤ √(2 * Real.log 2) * K

Lemma 9.4.20 (first part). For a $K$-sub-Gaussian tail bound about a point $m$, any median $\mathrm{med}$ of $X$ satisfies $|\mathrm{med} - m| \le \sqrt{2 \log 2} \cdot K$.

theorem SubGaussian.mean_close_to_center {Ω : Type u_1} [MeasurableSpace Ω] {X : Ω → ℝ} {m K : ℝ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (hK : 0 < K) (htail : HasSubGaussianTail X m K μ) (hX_int : MeasureTheory.Integrable X μ) (hX_mble : AEMeasurable (fun (ω : Ω) => |X ω - m|) μ) : |∫ (ω : Ω), X ω ∂μ - m| ≤ √Real.pi * K

Lemma 9.4.20 (second part). For a $K$-sub-Gaussian tail bound about $m$, $|\mathbb{E}[X] - m| \le \sqrt{\pi} \cdot K$. The proof integrates the Gaussian tail bound.

theorem SubGaussian.moment_bound_of_tail {Ω : Type u_1} [MeasurableSpace Ω] {X : Ω → ℝ} {m K : ℝ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (hK : 0 < K) (htail : HasSubGaussianTail X m K μ) (p : ℝ) (hp : 1 ≤ p) (hX_int : MeasureTheory.Integrable (fun (ω : Ω) => |X ω - m| ^ p) μ) : ∫ (ω : Ω), |X ω - m| ^ p ∂μ ≤ (3 * K * √p) ^ p

Moment bound for sub-Gaussian random variables: $\mathbb{E}|X - m|^p \le (3K\sqrt{p})^p$ for every $p \ge 1$.

theorem SubGaussian.lp_norm_close_to_center {Ω : Type u_1} [MeasurableSpace Ω] {X : Ω → ℝ} {m K : ℝ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (hK : 0 < K) (htail : HasSubGaussianTail X m K μ) : ∃ (C : ℝ), 0 < C ∧ ∀ (p : ℝ), 1 ≤ p → MeasureTheory.Integrable (fun (ω : Ω) => |X ω - m| ^ p) μ → (∫ (ω : Ω), |X ω - m| ^ p ∂μ) ^ (1 / p) ≤ C * K * √p

$L^p$ form of the sub-Gaussian moment bound: $\| X - m \|_{L^p} \le C K \sqrt{p}$ for an absolute constant $C$.

theorem SubGaussian.tail_recentering {Ω : Type u_1} [MeasurableSpace Ω] {X : Ω → ℝ} {m K : ℝ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (hK : 0 < K) (htail : HasSubGaussianTail X m K μ) (A : ℝ) (hA : 0 < A) : ∃ (c : ℝ), 0 < c ∧ ∀ (m' : ℝ), |m' - m| ≤ A * K → ∀ (t : ℝ), 0 ≤ t → μ {ω : Ω | t ≤ |X ω - m'|} ≤ ENNReal.ofReal (2 * Real.exp (-(c * t ^ 2 / K ^ 2)))

Recentering a sub-Gaussian tail bound: if $X$ has a $K$-sub-Gaussian tail about $m$ and $|m' - m| \le AK$, then $X$ also has a sub-Gaussian tail about $m'$ with a constant $c > 0$ depending on $A$.

theorem SubGaussian.lemma_9_4_20 {Ω : Type u_1} [MeasurableSpace Ω] {X : Ω → ℝ} {m K : ℝ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (hK : 0 < K) (htail : HasSubGaussianTail X m K μ) : (∀ (med : ℝ), IsMedian X med μ → |med - m| ≤ √(2 * Real.log 2) * K) ∧ (MeasureTheory.Integrable X μ → AEMeasurable (fun (ω : Ω) => |X ω - m|) μ → |∫ (ω : Ω), X ω ∂μ - m| ≤ √Real.pi * K) ∧ (∃ (C : ℝ), 0 < C ∧ ∀ (p : ℝ), 1 ≤ p → MeasureTheory.Integrable (fun (ω : Ω) => |X ω - m| ^ p) μ → (∫ (ω : Ω), |X ω - m| ^ p ∂μ) ^ (1 / p) ≤ C * K * √p) ∧ ∀ (A : ℝ), 0 < A → ∃ (c : ℝ), 0 < c ∧ ∀ (m' : ℝ), |m' - m| ≤ A * K → ∀ (t : ℝ), 0 ≤ t → μ {ω : Ω | t ≤ |X ω - m'|} ≤ ENNReal.ofReal (2 * Real.exp (-(c * t ^ 2 / K ^ 2)))

Lemma 9.4.20 (combined statement). For a $K$-sub-Gaussian tail bound about $m$: (i) any median is within $\sqrt{2 \log 2}\, K$ of $m$; (ii) the mean is within $\sqrt{\pi}\, K$ of $m$; (iii) the $L^p$ norm $\|X - m\|_{L^p}$ is bounded by $C K \sqrt{p}$; (iv) the tail bound persists when recentering to any nearby $m'$.