Probabilistic exponential concentration

The engine behind exponential concentration of quantum kernels (Thanasilp et al. 2022): a [0,1]-valued random variable with an exponentially small mean has an exponentially small variance, and hence (by Chebyshev) concentrates exponentially around its mean. Quantum-free; built on Mathlib's variance and Chebyshev inequality.

theorem QuantumAlg.variance_le_mean {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : Ω → ℝ} (hX : MeasureTheory.MemLp X 2 μ) (h0 : 0 ≤ᵐ[μ] X) (h1 : X ≤ᵐ[μ] 1) : ProbabilityTheory.variance X μ ≤ ∫ (ω : Ω), X ω ∂μ

For a [0,1]-valued random variable on a probability space, the variance is at most the mean (since X² ≤ X).

def QuantumAlg.ExpConcentratedProb {Ω : ℕ → Type u_2} [(n : ℕ) → MeasurableSpace (Ω n)] (μ : (n : ℕ) → MeasureTheory.Measure (Ω n)) (X : (n : ℕ) → Ω n → ℝ) : Prop

Probabilistic exponential concentration of a family of random variables X n : Ω n → ℝ (each on a probability space μ n): the probability of deviating from the mean by δ is at most C / (bⁿ δ²) for some b > 1.

Equations

• One or more equations did not get rendered due to their size.

theorem QuantumAlg.expConcentratedProb_of_variance_le {Ω : ℕ → Type u_2} [(n : ℕ) → MeasurableSpace (Ω n)] (μ : (n : ℕ) → MeasureTheory.Measure (Ω n)) [∀ (n : ℕ), MeasureTheory.IsProbabilityMeasure (μ n)] (X : (n : ℕ) → Ω n → ℝ) (hmem : ∀ (n : ℕ), MeasureTheory.MemLp (X n) 2 (μ n)) {b : ℝ} (hb : 1 < b) {C : ℝ} (hC : 0 ≤ C) (hvar : ∀ (n : ℕ), ProbabilityTheory.variance (X n) (μ n) ≤ C / b ^ n) : ExpConcentratedProb μ X

An exponentially small variance gives probabilistic exponential concentration (Chebyshev applied uniformly in n).

theorem QuantumAlg.expConcentratedProb_of_mean_le {Ω : ℕ → Type u_2} [(n : ℕ) → MeasurableSpace (Ω n)] (μ : (n : ℕ) → MeasureTheory.Measure (Ω n)) [∀ (n : ℕ), MeasureTheory.IsProbabilityMeasure (μ n)] (X : (n : ℕ) → Ω n → ℝ) (hmem : ∀ (n : ℕ), MeasureTheory.MemLp (X n) 2 (μ n)) (h0 : ∀ (n : ℕ), 0 ≤ᵐ[μ n] X n) (h1 : ∀ (n : ℕ), X n ≤ᵐ[μ n] 1) {b : ℝ} (hb : 1 < b) {C : ℝ} (hC : 0 ≤ C) (hmean : ∀ (n : ℕ), ∫ (ω : Ω n), X n ω ∂μ n ≤ C / b ^ n) : ExpConcentratedProb μ X

A [0,1]-valued family with exponentially small mean concentrates exponentially.

theorem QuantumAlg.ExpConcentratedProb.tendsto_zero {Ω : ℕ → Type u_2} [(n : ℕ) → MeasurableSpace (Ω n)] {μ : (n : ℕ) → MeasureTheory.Measure (Ω n)} {X : (n : ℕ) → Ω n → ℝ} (h : ExpConcentratedProb μ X) {δ : ℝ} (hδ : 0 < δ) : Filter.Tendsto (fun (n : ℕ) => (μ n) {ω : Ω n | δ ≤ |X n ω - ∫ (x : Ω n), X n x ∂μ n|}) Filter.atTop (nhds 0)

Under exponential concentration, the deviation probability vanishes as n → ∞ (for each fixed δ > 0): the landscape becomes flat and a polynomial shot budget cannot resolve the kernel.