Reference · Signed rationals

rainbow.math.rational.signed.indexed-max-dominates

Signed rationalssrc/rainbow/math/rational/signed/indexed_max_dominates.clj0 definitions, 1 theorems

Full dominance for the index-aware max: every index below n is bounded by the aggregate. signed/indexed-max-from-dominates : forall env init n i, strict-below i n -> env i <= indexed-max-from env init n. The argmax semantic property in full. By induction on n: n=0 is vacuous (strict-below i 0 is refuted); n=succ m splits strict-below i (succ m) via nat/strict-below-successor-split into (i < m -> use IH, then max-upper-left) or (i = m -> max-upper-right, transported along i=m). Off the trusted base (a property of the self-contained indexed-max aggregation).

Depends onmath.rational.signed.indexed-maxmath.nat.strict-below-split

signed/indexed-max-from-dominates :
  (env : ℕ → ℚ) (init : ℚ) (n i : ℕ) (h : nat/strict-below i n)
  → env i ≤ signed/indexed-max-from env init n