@[reducible, inline]

noncomputable abbrev SecondMoment.Var {Ω : Type u_1} {mΩ : MeasurableSpace Ω} (X : Ω → ℝ) (μ : MeasureTheory.Measure Ω) : ℝ

Shorthand for the variance $\mathrm{Var}(X) = \mathbb{E}[(X - \mathbb{E}X)^2]$ of a random variable $X$ with respect to a measure $\mu$.

theorem ProbabilityTheory.chebyshev_inequality {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : Ω → ℝ} (hX : MeasureTheory.MemLp X 2 μ) {t : ℝ} (ht : 0 < t) : μ {ω : Ω | t ≤ |X ω - ∫ (x : Ω), X x ∂μ|} ≤ ENNReal.ofReal (variance X μ / t ^ 2)

Chebyshev's inequality. For an $L^2$ random variable $X$ and any $t > 0$, $$\mathbb{P}\bigl(|X - \mathbb{E}X| \ge t\bigr) \le \frac{\mathrm{Var}(X)}{t^2}.$$

theorem ProbabilityTheory.prob_eq_zero_le_variance_div_sq {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : Ω → ℝ} (hX : MeasureTheory.MemLp X 2 μ) (hE : 0 < ∫ (ω : Ω), X ω ∂μ) : μ {ω : Ω | X ω = 0} ≤ ENNReal.ofReal (variance X μ / (∫ (ω : Ω), X ω ∂μ) ^ 2)

Second moment bound on the probability of vanishing. If $X \in L^2$ and $\mathbb{E}X > 0$, then $\mathbb{P}(X = 0) \le \mathrm{Var}(X) / (\mathbb{E}X)^2$. This is Lemma 4.2.4 (Corollary 4.1.7) in Probabilistic Methods in Combinatorics.

theorem ProbabilityTheory.tendsto_prob_eq_zero_of_variance_div_sq_tendsto {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : ℕ → Ω → ℝ} (hX : ∀ (n : ℕ), MeasureTheory.MemLp (X n) 2 μ) (hE : ∀ (n : ℕ), 0 < ∫ (ω : Ω), X n ω ∂μ) (hVar : Filter.Tendsto (fun (n : ℕ) => variance (X n) μ / (∫ (ω : Ω), X n ω ∂μ) ^ 2) Filter.atTop (nhds 0)) : Filter.Tendsto (fun (n : ℕ) => μ {ω : Ω | X n ω = 0}) Filter.atTop (nhds 0)

Asymptotic second moment method (single measure). If a sequence $(X_n)$ of $L^2$ random variables on a common probability space has $\mathbb{E}X_n > 0$ and $\mathrm{Var}(X_n) / (\mathbb{E}X_n)^2 \to 0$, then $\mathbb{P}(X_n = 0) \to 0$.

theorem ProbabilityTheory.second_moment_method {Ω : ℕ → Type u_1} [(n : ℕ) → MeasurableSpace (Ω n)] {μ : (n : ℕ) → MeasureTheory.Measure (Ω n)} [∀ (n : ℕ), MeasureTheory.IsProbabilityMeasure (μ n)] {X : (n : ℕ) → Ω n → ℝ} (hX : ∀ (n : ℕ), MeasureTheory.MemLp (X n) 2 (μ n)) (hμ_pos : ∀ (n : ℕ), 0 < ∫ (x : Ω n), X n x ∂μ n) (hVar : Filter.Tendsto (fun (n : ℕ) => variance (X n) (μ n) / (∫ (x : Ω n), X n x ∂μ n) ^ 2) Filter.atTop (nhds 0)) : Filter.Tendsto (fun (n : ℕ) => (μ n) {ω : Ω n | X n ω = 0}) Filter.atTop (nhds 0)

Second moment method (Corollary 4.1.8). Given a sequence of probability spaces $(\Omega_n, \mu_n)$ and $L^2$ random variables $X_n$ with $\mathbb{E}_{\mu_n}[X_n] > 0$, if $\mathrm{Var}(X_n) / (\mathbb{E}X_n)^2 \to 0$ then $\mu_n(X_n = 0) \to 0$.