Geometric-product tail bounds for finite adaptive processes

Per-state, history-dependent strict-progress bounds imply the same exponential upper-tail product as independent geometric waiting times. The proof is direct: derive a one-step contraction of a killed product potential and iterate it over the finite probability tree. No independent waiting-time coupling or final tail bound is assumed.

noncomputable def LeanPool.SingleCopyStabilizer.GeometricDomination.geometricFactor (p : ℕ → ℝ) (lambda : ℝ) (j : ℕ) : ℝ

The geometric moment-generating factor, in the parameterization q = 1/(1-λ).

Equations

• LeanPool.SingleCopyStabilizer.GeometricDomination.geometricFactor p lambda j = (1 - lambda / p j)⁻¹

noncomputable def LeanPool.SingleCopyStabilizer.GeometricDomination.productPotential (p : ℕ → ℝ) (lambda : ℝ) (r : ℕ) : ℝ

Product over the positive ranks up to and including r.

Equations

• LeanPool.SingleCopyStabilizer.GeometricDomination.productPotential p lambda r = ∏ j ∈ Finset.range r, LeanPool.SingleCopyStabilizer.GeometricDomination.geometricFactor p lambda (j + 1)

noncomputable def LeanPool.SingleCopyStabilizer.GeometricDomination.killedPotential (p : ℕ → ℝ) (lambda : ℝ) (r : ℕ) : ℝ

Set the potential to zero at the terminal rank.

Equations

• LeanPool.SingleCopyStabilizer.GeometricDomination.killedPotential p lambda r = if r = 0 then 0 else LeanPool.SingleCopyStabilizer.GeometricDomination.productPotential p lambda r

@[simp]

theorem LeanPool.SingleCopyStabilizer.GeometricDomination.productPotential_zero (p : ℕ → ℝ) (lambda : ℝ) : productPotential p lambda 0 = 1

@[simp]

theorem LeanPool.SingleCopyStabilizer.GeometricDomination.killedPotential_zero (p : ℕ → ℝ) (lambda : ℝ) : killedPotential p lambda 0 = 0

theorem LeanPool.SingleCopyStabilizer.GeometricDomination.productPotential_succ (p : ℕ → ℝ) (lambda : ℝ) (r : ℕ) : productPotential p lambda (r + 1) = productPotential p lambda r * geometricFactor p lambda (r + 1)

theorem LeanPool.SingleCopyStabilizer.GeometricDomination.factor_denominator_pos (p : ℕ → ℝ) (lambda : ℝ) (hlambda : 0 ≤ lambda) (hrate : ∀ (j : ℕ), 0 < j → lambda < p j) (j : ℕ) (hj : 0 < j) : 0 < 1 - lambda / p j

theorem LeanPool.SingleCopyStabilizer.GeometricDomination.one_le_geometricFactor (p : ℕ → ℝ) (lambda : ℝ) (hlambda : 0 ≤ lambda) (hrate : ∀ (j : ℕ), 0 < j → lambda < p j) (j : ℕ) (hj : 0 < j) : 1 ≤ geometricFactor p lambda j

theorem LeanPool.SingleCopyStabilizer.GeometricDomination.one_le_productPotential (p : ℕ → ℝ) (lambda : ℝ) (hlambda : 0 ≤ lambda) (hrate : ∀ (j : ℕ), 0 < j → lambda < p j) (r : ℕ) : 1 ≤ productPotential p lambda r

theorem LeanPool.SingleCopyStabilizer.GeometricDomination.productPotential_nonneg (p : ℕ → ℝ) (lambda : ℝ) (hlambda : 0 ≤ lambda) (hrate : ∀ (j : ℕ), 0 < j → lambda < p j) (r : ℕ) : 0 ≤ productPotential p lambda r

theorem LeanPool.SingleCopyStabilizer.GeometricDomination.productPotential_mono (p : ℕ → ℝ) (lambda : ℝ) (hlambda : 0 ≤ lambda) (hrate : ∀ (j : ℕ), 0 < j → lambda < p j) : Monotone (productPotential p lambda)

theorem LeanPool.SingleCopyStabilizer.GeometricDomination.killedPotential_nonneg (p : ℕ → ℝ) (lambda : ℝ) (hlambda : 0 ≤ lambda) (hrate : ∀ (j : ℕ), 0 < j → lambda < p j) (r : ℕ) : 0 ≤ killedPotential p lambda r

theorem LeanPool.SingleCopyStabilizer.GeometricDomination.killedPotential_le_productPotential (p : ℕ → ℝ) (lambda : ℝ) (hlambda : 0 ≤ lambda) (hrate : ∀ (j : ℕ), 0 < j → lambda < p j) {a b : ℕ} (hab : a ≤ b) : killedPotential p lambda a ≤ productPotential p lambda b

theorem LeanPool.SingleCopyStabilizer.GeometricDomination.productPotential_recurrence (p : ℕ → ℝ) (lambda : ℝ) (hlambda : 0 ≤ lambda) (hrate : ∀ (j : ℕ), 0 < j → lambda < p j) (r : ℕ) : (1 - p (r + 1)) * productPotential p lambda (r + 1) + p (r + 1) * productPotential p lambda r = (1 - lambda) * productPotential p lambda (r + 1)

The defining product has exactly the one-step recurrence of a geometric waiting-time generating function at each positive rank.

theorem LeanPool.SingleCopyStabilizer.GeometricDomination.product_potential_drift (p : ℕ → ℝ) (lambda : ℝ) (hlambda : 0 ≤ lambda) (hrate : ∀ (j : ℕ), 0 < j → lambda < p j) {S : Type u_1} {Ω : Type u_2} [Fintype Ω] (P : AdaptiveProcess.RankedProcess S Ω) (hprogress : ∀ (s : S), 0 < P.rank s → p (P.rank s) ≤ P.progressMass s) (s : S) : ∑ o : Ω, P.weight s o * killedPotential p lambda (P.rank (P.next s o)) ≤ (1 - lambda) * killedPotential p lambda (P.rank s)

History-conditioned progress gives contraction of the product potential at every state of the finite tree.

theorem LeanPool.SingleCopyStabilizer.GeometricDomination.failure_probability_le_product (p : ℕ → ℝ) (lambda : ℝ) (hlambda : 0 ≤ lambda) (hrate : ∀ (j : ℕ), 0 < j → lambda < p j) {S : Type u_1} {Ω : Type u_2} [Fintype Ω] (P : AdaptiveProcess.RankedProcess S Ω) (hlambda1 : lambda ≤ 1) (hprogress : ∀ (s : S), 0 < P.rank s → p (P.rank s) ≤ P.progressMass s) (t : ℕ) (s : S) : P.failureProbability t s ≤ productPotential p lambda (P.rank s) * (1 - lambda) ^ t

The product-geometric tail inequality for a fully adaptive finite tree. Only local kernel/progress hypotheses are used.