theorem Thresholds.variance_isLittleO_of_deltaStar_isLittleO {μ Δstar V : ℕ → ℝ} (hμ_pos : ∀ᶠ (n : ℕ) in Filter.atTop, 0 < μ n) (hμ_tendsto : Filter.Tendsto μ Filter.atTop Filter.atTop) (hΔstar_littleO : Δstar =o[Filter.atTop] μ) (hV_nonneg : ∀ᶠ (n : ℕ) in Filter.atTop, 0 ≤ V n) (hV_bound : ∀ᶠ (n : ℕ) in Filter.atTop, V n ≤ μ n + μ n * Δstar n) : V =o[Filter.atTop] fun (n : ℕ) => μ n ^ 2

Variance smallness from $\Delta^ = o(\mu)$.* If the mean $\mu_n \to \infty$, the auxiliary quantity $\Delta^*_n = o(\mu_n)$, and $V_n \le \mu_n + \mu_n \Delta^*_n$, then $V_n = o(\mu_n^2)$. This is the variance-bound input to the second moment method.

theorem Thresholds.positive_whp_of_deltaStar_isLittleO {μ Δstar V : ℕ → ℝ} (hμ_pos : ∀ᶠ (n : ℕ) in Filter.atTop, 0 < μ n) (hμ_tendsto : Filter.Tendsto μ Filter.atTop Filter.atTop) (hΔstar_littleO : Δstar =o[Filter.atTop] μ) (hV_nonneg : ∀ᶠ (n : ℕ) in Filter.atTop, 0 ≤ V n) (hV_bound : ∀ᶠ (n : ℕ) in Filter.atTop, V n ≤ μ n + μ n * Δstar n) {Ω : ℕ → Type u_1} [(n : ℕ) → MeasurableSpace (Ω n)] {μ_meas : (n : ℕ) → MeasureTheory.Measure (Ω n)} [∀ (n : ℕ), MeasureTheory.IsProbabilityMeasure (μ_meas n)] {X : (n : ℕ) → Ω n → ℝ} (hX : ∀ (n : ℕ), MeasureTheory.MemLp (X n) 2 (μ_meas n)) (hμ_pos_all : ∀ (n : ℕ), 0 < ∫ (x : Ω n), X n x ∂μ_meas n) (hE : ∀ (n : ℕ), ∫ (x : Ω n), X n x ∂μ_meas n = μ n) (hVar_eq : ∀ (n : ℕ), ProbabilityTheory.variance (X n) (μ_meas n) = V n) : Filter.Tendsto (fun (n : ℕ) => (μ_meas n) {ω : Ω n | X n ω = 0}) Filter.atTop (nhds 0)

Positivity w.h.p. via the second moment method. Given mean $\mu_n \to \infty$ and $\Delta^*_n = o(\mu_n)$ with $V_n \le \mu_n + \mu_n \Delta^*_n$, a sequence of $L^2$ random variables $X_n$ with $\mathbb{E}X_n = \mu_n$ and $\mathrm{Var}(X_n) = V_n$ satisfies $\mathbb{P}(X_n = 0) \to 0$.