Reference · Finite types, distributions and Markov chains

rainbow.math.finite.signed-expectation

Finite types, distributions and Markov chainssrc/rainbow/math/finite/signed_expectation.clj2 definitions, 3 theorems

Normalized finite expectation for exact signed-rational outcomes. Transition weights are signed rationals with explicit nonnegativity and normalization premises. The expectation is a finite weighted sum over a finset enumeration. It is monotone, adding a constant exposes total mass, and normalized expectation preserves pointwise additive epsilon bounds. This is reusable stochastic proof infrastructure for signed rewards and costs. Native, kernel-checked, and axiom-free on D63.

Depends onmath.rational.signed.map-sum-algebra

probability/signed-total-mass.{u} :
  (A : Type u) (source : Finset A) (x₁ : A → ℚ)
  → ℚ

probability/signed-expectation.{u} :
  (A : Type u) (source : Finset A) (mass x₁ : A → ℚ)
  → ℚ

probability/signed-expectation-monotone.{u} :
  (A : Type u) (source : Finset A) (mass lower-value upper-value : A → ℚ)
  (mass-nonnegative : ∀ (item : A), 0 ≤ mass item)
  (pointwise : ∀ (item : A), lower-value item ≤ upper-value item)
  → expectation lower-value ≤ expectation upper-value
  where expectation := probability/signed-expectation A source mass

probability/signed-expectation-add-constant.{u} :
  (A : Type u) (source : Finset A) (mass value : A → ℚ) (epsilon : ℚ)
  → expectation (fun item => value item + epsilon) = expectation value + probability/signed-total-mass A source mass · epsilon
  where expectation := probability/signed-expectation A source mass

probability/signed-expectation-additive-upper-bound-normalized.{u} :
  (A : Type u) (source : Finset A) (mass : A → ℚ)
  (mass-nonnegative : ∀ (item : A), 0 ≤ mass item)
  (normalized : probability/signed-total-mass A source mass = 1)
  (lower-value upper-value : A → ℚ) (epsilon : ℚ)
  (pointwise : ∀ (item : A), lower-value item ≤ upper-value item + epsilon)
  → expectation lower-value ≤ expectation upper-value + epsilon
  where expectation := probability/signed-expectation A source mass