Reference · Finite types, distributions and Markov chains

rainbow.math.finite.rational-expectation

Finite types, distributions and Markov chainssrc/rainbow/math/finite/rational_expectation.clj2 definitions, 2 theorems

Finite nonnegative-rational folds and expectations with congruence proofs.

list/nnrat-map-sum.{u} :
  (A : Type u) (mapping : A → ℚ≥0) (x₁ : List A)
  → ℚ≥0

probability/nnrat-expectation.{u} :
  (A : Type u) (source : Finset A) (mass value : A → ℚ≥0)
  → ℚ≥0

list/nnrat-map-sum-respects-equivalence.{u} :
  (A : Type u) (left right : A → ℚ≥0)
  (same : ∀ (value : A), left value = right value)
  (source : List A)
  → (fun source₁ => nnrat/map-sum A left source₁ = nnrat/map-sum A right source₁) source

nnrat/finite-expectation-respects-equivalence.{u} :
  (A : Type u) (source : Finset A)
  (mass equivalent-mass value equivalent-value : A → ℚ≥0)
  (same-mass : ∀ (state : A), mass state = equivalent-mass state)
  (same-value : ∀ (state : A), value state = equivalent-value state)
  → probability/nnrat-expectation A source mass value = probability/nnrat-expectation A source equivalent-mass equivalent-value