Reference · Finite types, distributions and Markov chains

rainbow.math.finite.expectation

Finite types, distributions and Markov chainssrc/rainbow/math/finite/expectation.clj5 definitions, 4 theorems

Executable finite natural mass and expectation numerators. This is the exact arithmetic substrate for finite probability. Natural masses plus an explicit normalization scale avoid introducing floating-point semantics or pretending that raw fractions already form a quotient field.

nat/multiply :
  (x₁ x₂ : ℕ)
  → ℕ

list/nat-map-sum.{u} :
  (A : Type u) (mapping : A → ℕ) (x₁ : List A)
  → ℕ

probability/weight-total.{u} :
  (A : Type u) (source : Finset A) (mass : A → ℕ)
  → ℕ

probability/normalized-at.{u} :
  (A : Type u) (scale : ℕ) (source : Finset A) (mass : A → ℕ)
  → Prop

probability/expectation-numerator.{u} :
  (A : Type u) (source : Finset A) (mass value : A → ℕ)
  → ℕ

list/nat-map-sum-zero.{u} :
  (A : Type u) (source : List A)
  → list/nat-map-sum A (fun x₃ => 0) source = 0

probability/expectation-zero.{u} :
  (A : Type u) (source : Finset A) (mass : A → ℕ)
  → probability/expectation-numerator A source mass (fun x₂ => 0) = 0

nat/one-times :
  (value : ℕ)
  → nat/multiply 1 value = value

nat/times-zero :
  (value : ℕ)
  → nat/multiply value 0 = 0