Reference · Non-negative rationals

rainbow.math.rational.nnrat.null-sequence

Non-negative rationalssrc/rainbow/math/rational/nnrat/null_sequence.clj1 definitions, 2 theorems

Real-analysis toward the OR payoff: null (converging-to-zero) sequences of nonnegative rationals, and the COMPARISON TEST -- a sequence dominated by a null sequence is null. analysis/null s M := forall eps n, M eps <= n -> s n <= eps analysis/null-dominated : (forall n, t n <= s n) -> null s M -> null t M Because nnrat values are >= 0, convergence to zero is one-sided (an upper bound that shrinks below every eps), so this needs NO signed arithmetic -- only nnrat order transitivity. This is the exact instrument behind contraction/value-iteration convergence: if the error e(n) <= gamma^n * C and gamma^n -> 0, then e -> 0. Native and axiom-free; chains rainbow.math.rational.nnrat.minmax on d63.

Depends onmath.rational.nnrat.minmax

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

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

analysis/null-max :
  (s t : ℕ → ℚ≥0) (M : ℚ≥0 → ℕ) (hs : analysis/null s M) (ht : analysis/null t M)
  → analysis/null (fun n => minmax/max (s n) (t n)) M