Reference · Non-negative rationals

rainbow.math.rational.nnrat.null-scaling

Non-negative rationalssrc/rainbow/math/rational/nnrat/null_scaling.clj0 definitions, 1 theorems

Scaling a null sequence by a bounded constant preserves convergence to zero: analysis/rate-null-scaled : c <= 1 -> rate-null s M -> rate-null (\n. c * s n) M Composes three earlier results: nnrat/multiply-right-monotone (c <= 1 => c*s n <= 1*s n), nnrat/multiply-one-left (1*s n ~ s n), transported by nnrat/at-most-respects-equivalence, then rate-null of s. Lets a geometric/harmonic error bound absorb a bounded prefactor. Native and axiom-free; chains nnrat-harmonic-convergence, nnrat-multiply-right-monotone, and nnrat-distributive on d63.

Depends onmath.rational.nnrat.harmonic-convergencemath.rational.nnrat.multiply-right-monotonemath.rational.nnrat.distributive

analysis/rate-null-scaled :
  (c : ℚ≥0) (s : ℕ → ℚ≥0) (M : ℕ → ℕ)
  (hc : c ≤ 1)
  (hs : analysis/rate-null s M)
  → analysis/rate-null (fun n => c · s n) M