Reference · Non-negative rationals

rainbow.math.rational.nnrat.harmonic-convergence

Non-negative rationalssrc/rainbow/math/rational/nnrat/harmonic_convergence.clj2 definitions, 3 theorems

A CONCRETE convergence theorem: the harmonic sequence 1/(n+1) converges to zero, with an explicit modulus. This is the first fully worked null sequence and it makes the convergence toolkit usable. Convergence-to-zero is formulated over the positive-rational ladder 1/(k+1) (rather than quantifying eps over all nnrat, which would wrongly force eventual-zero): analysis/rate-null s M := forall k n, M k <= n -> s n <= 1/(k+1) nnrat/harmonic n := 1/(n+1) (= make 1 n) analysis/harmonic-rate-null : rate-null harmonic (identity) (n >= k => 1/(n+1) <= 1/(k+1)) analysis/rate-null-dominated: (forall n, t n <= s n) -> rate-null s M -> rate-null t M The harmonic bound reduces (nnrat/at-most-from-cross) to 1*(k+1) <= 1*(n+1), i.e. nat/multiply-left-monotone applied to succ k <= succ n, which follows from k <= n by a witness (proved here as nat/successor-monotone, absent from d63). Native and axiom-free; self-contained on d63.

analysis/rate-null :
  (x₁ : ℕ → ℚ≥0) (x₂ : ℕ → ℕ)
  → Prop

nnrat/harmonic :
  (x₁ : ℕ)
  → ℚ≥0

nat/successor-monotone :
  (k n : ℕ)
  (h : k ≤ n)
  → data/succ k ≤ data/succ n

analysis/harmonic-rate-null :
  → analysis/rate-null nnrat/harmonic (fun k => k)

analysis/rate-null-dominated :
  (s t : ℕ → ℚ≥0) (M : ℕ → ℕ)
  (dom : ∀ (n : ℕ), t n ≤ s n)
  (hs : analysis/rate-null s M)
  → analysis/rate-null t M