Reference · Non-negative rationals

rainbow.math.rational.nnrat.general-contraction

Non-negative rationalssrc/rainbow/math/rational/nnrat/general_contraction.clj0 definitions, 3 theorems

Arbitrary-gamma contraction convergence. With a = ap+1, g = gp+1, gamma = a/(a+g) (any rational < 1) and the bound B n = a/(a+ng) = nnrat/general-harmonic ap gp n: nnrat/general-harmonic-step : gamma * B n <= B (n+1) analysis/general-contraction-error-below : e0 <= B 0 -> (forall n, e(n+1) <= gamma*e n) -> (forall n, e n <= B n) analysis/general-contraction-converges : ... -> rate-null e The step inequality reduces (at-most-from-cross) to a nat cross-product whose gap is exactly a*n*g^2: after a succ-expansion (succ n)*g = g + n*g and a combine-law denominator transport, the witness W = a*n*g^2 and nat-ring close it. The induction and the rate-null conclusion mirror the 1/2 case, with general-harmonic-null + null-dominated. Native and axiom-free; chains nnrat-general-harmonic, nnrat-multiply-monotone, nnrat-ring.

Depends onmath.rational.nnrat.general-harmonicmath.rational.nnrat.multiply-monotone

nnrat/general-harmonic-step :
  (ap gp n : ℕ)
  → nnrat/make (data/succ ap) (algebra/nat-add ap (data/succ gp)) · nnrat/general-harmonic ap gp n ≤ nnrat/general-harmonic ap gp (data/succ n)

analysis/general-contraction-error-below :
  (ap gp : ℕ) (e : ℕ → ℚ≥0)
  (e0 : e 0 ≤ nnrat/general-harmonic ap gp 0)
  (rec : ∀ (n : ℕ), e (data/succ n) ≤ nnrat/make (data/succ ap) (algebra/nat-add ap (data/succ gp)) · e n)
  (n : ℕ)
  → e n ≤ nnrat/general-harmonic ap gp n

analysis/general-contraction-converges :
  (ap gp : ℕ) (e : ℕ → ℚ≥0)
  (e0 : e 0 ≤ nnrat/general-harmonic ap gp 0)
  (rec : ∀ (n : ℕ), e (data/succ n) ≤ nnrat/make (data/succ ap) (algebra/nat-add ap (data/succ gp)) · e n)
  → analysis/rate-null e (fun k => nat/multiply (data/succ ap) k)