Reference · Natural numbers

rainbow.math.nat.order

Natural numberssrc/rainbow/math/nat/order.clj0 definitions, 11 theorems

Constructive monotonicity for Nat arithmetic and finite expectation.

nat/at-most-reflexive :
  (value : ℕ)
  → value ≤ value

nat/at-most-transitive :
  (left middle right : ℕ)
  (first : left ≤ middle)
  (second : middle ≤ right)
  → left ≤ right

nat/at-most-successor :
  (value : ℕ)
  → value ≤ data/succ value

nat/add-left-monotone :
  (prefix left right : ℕ)
  (ordered : left ≤ right)
  → algebra/nat-add prefix left ≤ algebra/nat-add prefix right

nat/add-right-monotone :
  (suffix left right : ℕ)
  (ordered : left ≤ right)
  → algebra/nat-add left suffix ≤ algebra/nat-add right suffix

nat/add-monotone :
  (left-a right-a left-b right-b : ℕ)
  (ordered-a : left-a ≤ right-a)
  (ordered-b : left-b ≤ right-b)
  → algebra/nat-add left-a left-b ≤ algebra/nat-add right-a right-b

nat/multiply-add-left :
  (left right factor : ℕ)
  → nat/multiply (algebra/nat-add left right) factor = algebra/nat-add (nat/multiply left factor) (nat/multiply right factor)

nat/multiply-right-monotone :
  (factor left right : ℕ)
  (ordered : left ≤ right)
  → nat/multiply left factor ≤ nat/multiply right factor

nat/multiply-left-monotone :
  (factor left right : ℕ)
  (ordered : left ≤ right)
  → nat/multiply factor left ≤ nat/multiply factor right

list/nat-map-sum-monotone.{u} :
  (A : Type u) (left right : A → ℕ)
  (ordered : ∀ (value : A), left value ≤ right value)
  (source : List A)
  → list/nat-map-sum A left source ≤ list/nat-map-sum A right source

probability/expectation-monotone.{u} :
  (A : Type u) (source : Finset A) (mass left right : A → ℕ)
  (ordered : ∀ (state : A), left state ≤ right state)
  → numerator left ≤ numerator right
  where numerator := probability/expectation-numerator A source mass