Reference · Natural numbers

rainbow.math.nat.contraction

Natural numberssrc/rainbow/math/nat/contraction.clj0 definitions, 10 theorems

Natural multiplication laws needed by finite metric contraction proofs.

nat/multiply-successor-right :
  (value factor : ℕ)
  → nat/multiply value (data/succ factor) = algebra/nat-add value (nat/multiply value factor)

nat/multiply-commutative :
  (left right : ℕ)
  → nat/multiply left right = nat/multiply right left

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

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

nat/at-most-rewrite-right :
  (left right replacement : ℕ)
  (same : right = replacement)
  (ordered : left ≤ right)
  → left ≤ replacement

list/nat-map-sum-distance-bound.{u} :
  (A : Type u) (left right : A → ℕ) (epsilon : ℕ)
  (pointwise : ∀ (value : A), nat/distance (left value) (right value) ≤ epsilon)
  (source : List A)
  → nat/distance (list/nat-map-sum A left source) (list/nat-map-sum A right source) ≤ nat/multiply (list/length A source) epsilon

nat/at-most-rewrite-left :
  (left replacement right : ℕ)
  (same : left = replacement)
  (ordered : replacement ≤ right)
  → left ≤ right

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

list/nat-map-sum-multiply-right.{u} :
  (A : Type u) (mapping : A → ℕ) (factor : ℕ) (source : List A)
  → list/nat-map-sum A (fun value => nat/multiply (mapping value) factor) source = nat/multiply (list/nat-map-sum A mapping source) factor

probability/expectation-distance-bound.{u} :
  (A : Type u) (source : Finset A) (mass left right : A → ℕ) (epsilon : ℕ)
  (pointwise : ∀ (state : A), nat/distance (left state) (right state) ≤ epsilon)
  → nat/distance (numerator₁) (numerator) ≤ nat/multiply (probability/weight-total A source mass) epsilon
  where numerator := probability/expectation-numerator A source mass right
  where numerator₁ := probability/expectation-numerator A source mass left