Reference · Foundations

rainbow.math.real-analysis-foundation

Foundationssrc/rainbow/math/real_analysis_foundation.clj3 definitions, 2 theorems

FIRST brick of the real-analysis layer -- the gating foundation for frontier OR (convergence rates, GP regret, MDP contraction, LP duality all live over the reals). This module lays the sequence-order infrastructure that the monotone convergence theorem and Cauchy-real construction build on, using rational-valued sequences (nat -> nnrat) and the existing nnrat order. It proves the pieces reachable with order-REFLEXIVITY alone: analysis/sequence : nat -> nnrat analysis/nondecreasing s : forall n, s n <= s (succ n) analysis/bounded-above s B : forall n, s n <= B analysis/constant c : the constant sequence analysis/constant-nondecreasing : every constant sequence is nondecreasing analysis/constant-bounded-by-self : a constant sequence is bounded by its value ROADMAP (the remaining real-analysis bedrock, in dependency order -- each needs the next; see rainbow-real-analysis-roadmap memory): nat multiplicative at-most cancellation -> nnrat closure<->base order equivalence -> nnrat additive at-most cancellation -> signed order transitivity + add-monotone -> the epsilon-N convergence predicate + squeeze theorem -> monotone convergence / Cauchy completeness -> limits, continuity, derivatives. Native and axiom-free; self-contained on d63 (uses only nnrat/at-most-reflexive).

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

analysis/bounded-above :
  (x₁ : ℕ → ℚ≥0) (x₂ : ℚ≥0)
  → Prop

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

analysis/constant-nondecreasing :
  (c : ℚ≥0)
  → analysis/nondecreasing (analysis/constant c)

analysis/constant-bounded-by-self :
  (c : ℚ≥0)
  → analysis/bounded-above (analysis/constant c) c