Expectations that only see the support

An ℝ≥0∞-valued expectation ∑' a, p a * f a under p : PMF α depends only on the values of f on p.support. These lemmas package the off-support case split (p a = 0) that otherwise recurs whenever a coupled-state invariant holds only on the support, such as a pinned abstract state in the randomized state-transition certificates.

Main results

• Cslib.Probability.PMF.tsum_mul_congr_support: expectations of functions agreeing on the support are equal.
• Cslib.Probability.PMF.tsum_mul_add_of_support: a summand that is constant on the support leaves the expectation as that constant.
• Cslib.Probability.PMF.tsum_mul_le_of_support: an integrand bounded on the support has expectation at most that bound.

theorem Cslib.Probability.PMF.tsum_mul_congr_support {α : Type u_1} (p : PMF α) {f g : α → ENNReal} (h : ∀ a ∈ p.support, f a = g a) : ∑' (a : α), p a * f a = ∑' (a : α), p a * g a

An expectation depends only on the values of the integrand on the support.

theorem Cslib.Probability.PMF.tsum_mul_add_of_support {α : Type u_1} (p : PMF α) {g f : α → ENNReal} {c : ENNReal} (hg : ∀ a ∈ p.support, g a = c) : ∑' (a : α), p a * (g a + f a) = c + ∑' (a : α), p a * f a

A summand equal to the constant c on the support contributes exactly c to the expectation.

theorem Cslib.Probability.PMF.tsum_mul_le_of_support {α : Type u_1} (p : PMF α) {f : α → ENNReal} {c : ENNReal} (h : ∀ a ∈ p.support, f a ≤ c) : ∑' (a : α), p a * f a ≤ c

An integrand bounded by c on the support has expectation at most c. This is the support-restricted form of Cslib.Probability.PMF.tsum_mul_le_of_forall_le.