Extended-nonnegative-real expectation on ProbComp

Expected value Cslib.ProbComp.expect m f = ∑' a, (eval m) a * f a for a closed probabilistic program m : ProbComp α and cost function f : α → ℝ≥0∞.

Working in ℝ≥0∞ makes expectation total without [Fintype α], [MeasurableSpace α], or summability hypotheses. Every PMF has countable support, while program state spaces such as machine configurations with infinite memory ℕ → ℕ need not be finite or carry a measurable space. Unbounded or faulting branches naturally evaluate to ⊤.

Main definitions

• Cslib.ProbComp.expect: ℝ≥0∞-valued expectation ∑' a, (eval m) a * f a over ProbComp.

Main results

• Cslib.ProbComp.expect_pure, Cslib.ProbComp.expect_bind, Cslib.ProbComp.expect_map: monadic laws for expect (return, tower/law of total expectation, and postprocessing).
• Cslib.ProbComp.expect_const, Cslib.ProbComp.expect_add, Cslib.ProbComp.expect_mul_left, Cslib.ProbComp.expect_mul_right: linearity over ℝ≥0∞.
• Cslib.ProbComp.expect_congr_on_support, Cslib.ProbComp.expect_mono_on_support, Cslib.ProbComp.expect_eq_top_of_mem_support: support-localized congruence, monotonicity, and divergence propagation.
• Cslib.ProbComp.expect_unifFin, Cslib.ProbComp.expect_uniform: uniform finite averages.

References

• M. Mitzenmacher and E. Upfal, Probability and Computing

noncomputable def Cslib.ProbComp.expect {α : Type} (m : ProbComp α) (f : α → ENNReal) : ENNReal

Expected value of f : α → ℝ≥0∞ under a closed ProbComp computation.

@[simp]

theorem Cslib.ProbComp.expect_pure {α : Type} (a : α) (f : α → ENNReal) : (pure a).expect f = f a

@[simp]

theorem Cslib.ProbComp.expect_const {α : Type} (m : ProbComp α) (c : ENNReal) : (m.expect fun (x : α) => c) = c

theorem Cslib.ProbComp.expect_zero {α : Type} (m : ProbComp α) : (m.expect fun (x : α) => 0) = 0

theorem Cslib.ProbComp.expect_add {α : Type} (m : ProbComp α) (f g : α → ENNReal) : (m.expect fun (a : α) => f a + g a) = m.expect f + m.expect g

theorem Cslib.ProbComp.expect_mul_left {α : Type} (m : ProbComp α) (c : ENNReal) (f : α → ENNReal) : (m.expect fun (a : α) => c * f a) = c * m.expect f

theorem Cslib.ProbComp.expect_mul_right {α : Type} (m : ProbComp α) (f : α → ENNReal) (c : ENNReal) : (m.expect fun (a : α) => f a * c) = m.expect f * c

theorem Cslib.ProbComp.expect_bind {α β : Type} (m : ProbComp α) (k : α → ProbComp β) (f : β → ENNReal) : (m >>= k).expect f = m.expect fun (a : α) => (k a).expect f

theorem Cslib.ProbComp.expect_map {α β : Type} (g : α → β) (m : ProbComp α) (f : β → ENNReal) : (g <$> m).expect f = m.expect fun (a : α) => f (g a)

theorem Cslib.ProbComp.expect_congr_on_support {α : Type} {m : ProbComp α} {f g : α → ENNReal} (h : ∀ a ∈ OracleComp.support m, f a = g a) : m.expect f = m.expect g

theorem Cslib.ProbComp.expect_mono_on_support {α : Type} {m : ProbComp α} {f g : α → ENNReal} (h : ∀ a ∈ OracleComp.support m, f a ≤ g a) : m.expect f ≤ m.expect g

theorem Cslib.ProbComp.expect_mono {α : Type} {m : ProbComp α} {f g : α → ENNReal} (h : ∀ (a : α), f a ≤ g a) : m.expect f ≤ m.expect g

theorem Cslib.ProbComp.expect_le_of_forall_support {α : Type} {m : ProbComp α} {f : α → ENNReal} {B : ENNReal} (h : ∀ a ∈ OracleComp.support m, f a ≤ B) : m.expect f ≤ B

theorem Cslib.ProbComp.expect_eq_top_of_mem_support {α : Type} {m : ProbComp α} {f : α → ENNReal} {a : α} (ha : a ∈ OracleComp.support m) (hf : f a = ⊤) : m.expect f = ⊤

theorem Cslib.ProbComp.expect_unifFin (n : ℕ) (f : Fin (n + 1) → ENNReal) : (unifFin n).expect f = (∑ k : Fin (n + 1), f k) / (↑n + 1)

theorem Cslib.ProbComp.expect_uniform {α : Type} [Fintype α] [Nonempty α] (f : α → ENNReal) : (uniform α).expect f = (∑ a : α, f a) / ↑(Fintype.card α)