Expectations under a FintypePMF

trueExpectation is the expectation of an ℝ-valued function under a FintypePMF; boolTestExpectation is the specialisation to indicator (Bool-valued) tests via the embedding if · then 1 else 0. The indicator form is [0, 1]-bounded and evaluates to the sample-average on an empirical PMF; these are the bricks used by the TV-based transfer principle in the next shard.

def ProbabilityTheory.FintypePMF.trueExpectation {α : Type u_1} [Fintype α] (p : FintypePMF α) (f : α → ℝ) : ℝ

Expected value ∑ h, p.prob h * f h of a real-valued test under a FintypePMF.

Equations

• p.trueExpectation f = ∑ a : α, p.prob a * f a

def ProbabilityTheory.FintypePMF.boolTestExpectation {α : Type u_1} [Fintype α] (p : FintypePMF α) (f : α → Bool) : ℝ

Expected value of a Bool-valued test under a FintypePMF via the indicator embedding if f a then 1 else 0.

Equations

• p.boolTestExpectation f = p.trueExpectation fun (a : α) => if f a = true then 1 else 0

theorem ProbabilityTheory.FintypePMF.boolTestExpectation_nonneg {α : Type u_1} [Fintype α] (p : FintypePMF α) (f : α → Bool) : 0 ≤ p.boolTestExpectation f

theorem ProbabilityTheory.FintypePMF.boolTestExpectation_le_one {α : Type u_1} [Fintype α] (p : FintypePMF α) (f : α → Bool) : p.boolTestExpectation f ≤ 1

theorem ProbabilityTheory.FintypePMF.boolTestExpectation_empirical_eq_avg {α : Type u_1} [Fintype α] [DecidableEq α] {T : ℕ} (hT : 0 < T) (rs : Fin T → α) (f : α → Bool) : (empirical hT rs).boolTestExpectation f = (∑ t : Fin T, if f (rs t) = true then 1 else 0) / ↑T

Expectation of a Bool-valued test under an empirical FintypePMF equals the sample average along the underlying sequence. Bridges the distributional view to the sample-average view used by the MWU argument.