Scalar Chernoff bounds for geometric-product potentials

These finite-product inequalities are independent of a stochastic model. GeometricDomination supplies the adaptive-process domination needed to interpret the final bound as a failure probability.

theorem LeanPool.SingleCopyStabilizer.GeometricTailBounds.reciprocal_one_sub_le_quadratic (x : ℝ) (_hx : 0 ≤ x) (hxhalf : x ≤ 1 / 2) : (1 - x)⁻¹ ≤ 1 + x + 2 * x ^ 2

A quadratic upper bound for a geometric-series factor.

theorem LeanPool.SingleCopyStabilizer.GeometricTailBounds.reciprocal_one_sub_le_exp (x : ℝ) (hx : 0 ≤ x) (hxhalf : x ≤ 1 / 2) : (1 - x)⁻¹ ≤ Real.exp (x + 2 * x ^ 2)

The same reciprocal factor is bounded by a quadratic exponential.

theorem LeanPool.SingleCopyStabilizer.GeometricTailBounds.geometric_factor_le_exp (p lam : ℝ) (hp : 1 / 4 ≤ p) (hlam : 0 ≤ lam) (hlammax : lam ≤ 1 / 8) : (1 - lam / p)⁻¹ ≤ Real.exp ((lam + 8 * lam ^ 2) / p)

Each geometric PGF factor has an exponential bound controlled by 1/p.

theorem LeanPool.SingleCopyStabilizer.GeometricTailBounds.product_le_exp {α : Type u_1} (indices : Finset α) (p : α → ℝ) (lam M : ℝ) (hp : ∀ i ∈ indices, 1 / 4 ≤ p i) (hlam : 0 ≤ lam) (hlammax : lam ≤ 1 / 8) (hmean : ∑ i ∈ indices, 1 / p i ≤ M) : ∏ i ∈ indices, (1 - lam / p i)⁻¹ ≤ Real.exp ((lam + 8 * lam ^ 2) * M)

The product of the geometric factors is bounded using their reciprocal sum.

theorem LeanPool.SingleCopyStabilizer.GeometricTailBounds.decay_le_exp (lam : ℝ) (T : ℕ) (hlammax : lam ≤ 1) : (1 - lam) ^ T ≤ Real.exp (-lam * ↑T)

The Bernoulli decay term is at most the corresponding exponential.

theorem LeanPool.SingleCopyStabilizer.GeometricTailBounds.product_decay_le_exp {α : Type u_1} (indices : Finset α) (p : α → ℝ) (lam M : ℝ) (T : ℕ) (hp : ∀ i ∈ indices, 1 / 4 ≤ p i) (hlam : 0 ≤ lam) (hlammax : lam ≤ 1 / 8) (hmean : ∑ i ∈ indices, 1 / p i ≤ M) : (∏ i ∈ indices, (1 - lam / p i)⁻¹) * (1 - lam) ^ T ≤ Real.exp ((lam + 8 * lam ^ 2) * M - lam * ↑T)

A finite-product Chernoff bound before choosing the exponential parameter.

noncomputable def LeanPool.SingleCopyStabilizer.GeometricTailBounds.chosenTilt (M s : ℝ) : ℝ

Parameter used for a deviation s above the reciprocal-sum bound M.

Equations

• LeanPool.SingleCopyStabilizer.GeometricTailBounds.chosenTilt M s = s / (16 * (M + s))

theorem LeanPool.SingleCopyStabilizer.GeometricTailBounds.chosenTilt_bounds (M s : ℝ) (hM : 0 < M) (hs : 0 ≤ s) : 0 ≤ chosenTilt M s ∧ chosenTilt M s ≤ 1 / 16

theorem LeanPool.SingleCopyStabilizer.GeometricTailBounds.chosenTilt_lt_rate (M s p : ℝ) (hM : 0 < M) (hs : 0 ≤ s) (hp : 1 / 4 ≤ p) : chosenTilt M s < p

The chosen tilt is strictly below every permitted progress rate.

theorem LeanPool.SingleCopyStabilizer.GeometricTailBounds.chosenTilt_exponent (M s T : ℝ) (hM : 0 < M) (hs : 0 ≤ s) (hT : M + s ≤ T) : (chosenTilt M s + 8 * chosenTilt M s ^ 2) * M - chosenTilt M s * T ≤ -(s ^ 2 / (32 * (M + s)))

The chosen tilt gives a quadratic-over-linear deviation exponent.

theorem LeanPool.SingleCopyStabilizer.GeometricTailBounds.sharp_tail_bound {α : Type u_1} (indices : Finset α) (p : α → ℝ) (M s : ℝ) (T : ℕ) (hM : 0 < M) (hs : 0 ≤ s) (hp : ∀ i ∈ indices, 1 / 4 ≤ p i) (hmean : ∑ i ∈ indices, 1 / p i ≤ M) (hT : M + s ≤ ↑T) : (∏ i ∈ indices, (1 - chosenTilt M s / p i)⁻¹) * (1 - chosenTilt M s) ^ T ≤ Real.exp (-(s ^ 2 / (32 * (M + s))))

Finite geometric-product Chernoff bound with leading term M.

noncomputable def LeanPool.SingleCopyStabilizer.GeometricTailBounds.confidenceDeviation (M L : ℝ) : ℝ

An explicit deviation of order sqrt(M L) + L.

Equations

• LeanPool.SingleCopyStabilizer.GeometricTailBounds.confidenceDeviation M L = 8 * √(M * L) + 64 * L

theorem LeanPool.SingleCopyStabilizer.GeometricTailBounds.confidenceDeviation_nonneg (M L : ℝ) (_hM : 0 ≤ M) (hL : 0 ≤ L) : 0 ≤ confidenceDeviation M L

theorem LeanPool.SingleCopyStabilizer.GeometricTailBounds.confidenceDeviation_exponent (M L : ℝ) (hM : 0 < M) (hL : 0 ≤ L) : L ≤ confidenceDeviation M L ^ 2 / (32 * (M + confidenceDeviation M L))

The explicit deviation makes the quadratic-over-linear exponent at least L.

theorem LeanPool.SingleCopyStabilizer.GeometricTailBounds.confidence_exp_bound {α : Type u_1} (indices : Finset α) (p : α → ℝ) (M L : ℝ) (T : ℕ) (hM : 0 < M) (hL : 0 ≤ L) (hp : ∀ i ∈ indices, 1 / 4 ≤ p i) (hmean : ∑ i ∈ indices, 1 / p i ≤ M) (hT : M + confidenceDeviation M L ≤ ↑T) : (∏ i ∈ indices, (1 - chosenTilt M (confidenceDeviation M L) / p i)⁻¹) * (1 - chosenTilt M (confidenceDeviation M L)) ^ T ≤ Real.exp (-L)

A square-root-plus-linear budget achieves tail exp(-L).

theorem LeanPool.SingleCopyStabilizer.GeometricTailBounds.confidence_tail_bound {α : Type u_1} (indices : Finset α) (p : α → ℝ) (M δ : ℝ) (T : ℕ) (hM : 0 < M) (hδ : 0 < δ) (hδmax : δ ≤ 1) (hp : ∀ i ∈ indices, 1 / 4 ≤ p i) (hmean : ∑ i ∈ indices, 1 / p i ≤ M) (hT : M + confidenceDeviation M (Real.log (1 / δ)) ≤ ↑T) : (∏ i ∈ indices, (1 - chosenTilt M (confidenceDeviation M (Real.log (1 / δ))) / p i)⁻¹) * (1 - chosenTilt M (confidenceDeviation M (Real.log (1 / δ)))) ^ T ≤ δ

The numerical confidence guarantee with L = log(1/δ).

noncomputable def LeanPool.SingleCopyStabilizer.GeometricTailBounds.confidenceBudget (M δ : ℝ) : ℕ

A natural-number budget with leading term M.

Equations

• LeanPool.SingleCopyStabilizer.GeometricTailBounds.confidenceBudget M δ = ⌈M + LeanPool.SingleCopyStabilizer.GeometricTailBounds.confidenceDeviation M (Real.log (1 / δ))⌉₊

theorem LeanPool.SingleCopyStabilizer.GeometricTailBounds.confidenceBudget_sufficient {α : Type u_1} (indices : Finset α) (p : α → ℝ) (M δ : ℝ) (hM : 0 < M) (hδ : 0 < δ) (hδmax : δ ≤ 1) (hp : ∀ i ∈ indices, 1 / 4 ≤ p i) (hmean : ∑ i ∈ indices, 1 / p i ≤ M) : (∏ i ∈ indices, (1 - chosenTilt M (confidenceDeviation M (Real.log (1 / δ))) / p i)⁻¹) * (1 - chosenTilt M (confidenceDeviation M (Real.log (1 / δ)))) ^ confidenceBudget M δ ≤ δ

theorem LeanPool.SingleCopyStabilizer.GeometricTailBounds.exact_rate_sum_bound (r n : ℕ) (hrn : r ≤ n) : ∑ j ∈ Finset.range r, 1 / FiniteProbability.progressProbability (j + 1) ≤ 2 * ↑n + 4

The exact learner's reciprocal progress sum is at most 2n + 4, even when its current rank r is smaller than the qubit count n.