Reference · Non-negative rationals

rainbow.math.rational.nnrat.general-harmonic

Non-negative rationalssrc/rainbow/math/rational/nnrat/general_harmonic.clj1 definitions, 1 theorems

General harmonic null sequence, the bound that dominates any contraction rate gamma<1: nnrat/general-harmonic ap gp n := a / (a + n*g) with a = ap+1, g = gp+1 analysis/general-harmonic-null : rate-null (general-harmonic ap gp) (\k. a*k) a/(a+ng) -> 0: it is <= 1/(k+1) once a*k <= n (modulus M k = a*k), because the cross-product a*(k+1) <= a+ng reduces to a*k <= n*g, and a*k <= n <= n*g (g>=1). This is the reciprocal form of the Bernoulli bound gamma^n <= a/(a+n(b-a)) written with the gap g = b-a, letting arbitrary gamma = a/(a+g) < 1 be handled by domination. Native and axiom-free; chains nnrat-harmonic-convergence on d63.

Depends onmath.rational.nnrat.harmonic-convergence

nnrat/general-harmonic :
  (x₁ x₂ x₃ : ℕ)
  → ℚ≥0

analysis/general-harmonic-null :
  (ap gp : ℕ)
  → analysis/rate-null (nnrat/general-harmonic ap gp) (fun k => nat/multiply (data/succ ap) k)