Expectation under a probability mass function
DefinitionExpectation under a probability mass function#✓fully proved
Let \(\alpha\) be a type carrying a σ-algebra in which singletons are measurable, let \(p\) be a probability mass function on \(\alpha\) and let \(f : \alpha \to \mathbb{R}\). The expectation of \(f\) under \(p\) is the Bochner integral \(\int f \, d\mu_p\), where \(\mu_p\) is the probability measure on \(\alpha\) associated to \(p\).
On a finite type it equals the finite sum \(\sum_{a \in \alpha} p(a) f(a)\), with each mass \(p(a)\) read as a real number. As a Bochner integral it is \(0\) when \(f\) is not integrable; nonnegative or natural-valued observables should use the extended nonnegative expectation, whose value in \([0, \infty]\) can be \(\infty\).
noncomputable def expect (p : PMF α) (f : α → ℝ) : ℝ :=
∫ a, f a ∂p.toMeasureUsed by 14
TheoremExpectation as a series#✓fully proved
Let \(p\) be a probability mass function on a measurable space \(\alpha\) in which singletons are measurable, and let \(f : \alpha \to \mathbb{R}\) be integrable with respect to the probability measure associated to \(p\). Then the expectation of \(f\) under \(p\) equals the unordered sum \(\sum_{a \in \alpha} p(a) f(a)\).
theorem expect_eq_tsum (hf : MeasureTheory.Integrable f p.toMeasure) :
p.expect f = ∑' a, (p a).toReal • f aUses 1
TheoremExpectation on a finite type#✓fully proved
Let \(p\) be a probability mass function on a finite measurable space \(\alpha\) in which singletons are measurable, and let \(f : \alpha \to \mathbb{R}\). Then the expectation of \(f\) under \(p\) equals the finite sum \(\sum_{a \in \alpha} p(a) f(a)\).
Uses 1 · Used by 10
TheoremExpectation of a constant on a finite type#✓fully proved
Let \(\alpha\) be a finite set with a \(\sigma\)-algebra in which singletons are measurable and let \(p\) be a probability mass function on \(\alpha\). For every \(c \in \mathbb{R}\), the expectation of the constant function \(a \mapsto c\) under \(p\) is \(c\).
Uses 2
TheoremExpectation under the uniform distribution#✓fully proved
Let \(\alpha\) be a nonempty finite type carrying a σ-algebra in which singletons are measurable. For every function \(f : \alpha \to \mathbb{R}\), the expectation of \(f\) under the uniform distribution on \(\alpha\) equals the average \(\frac{1}{|\alpha|} \sum_{a \in \alpha} f(a)\).
theorem expect_uniformOfFintype [Fintype α] [Nonempty α] (f : α → ℝ) :
(PMF.uniformFintype α).expect f =
(Fintype.card α : ℝ)⁻¹ * ∑ a, f anoncomputable def uniformFintype (α : Type*) [Fintype α] [Nonempty α] : PMF α :=
ofFintype (fun _ => (Fintype.card α : ℝ≥0∞)⁻¹) (by
simp only [Finset.sum_const, Finset.card_univ, nsmul_eq_mul]
have h : (Fintype.card α : ℝ≥0∞) ≠ 0 := by
simpa only [Ne, Nat.cast_eq_zero] using (Fintype.card_ne_zero (α := α))
exact ENNReal.mul_inv_cancel h (ENNReal.natCast_ne_top (Fintype.card α)))MathlibExt/Probability/ProbabilityMassFunction/Uniform.lean:68
Uses 3
TheoremAdditivity of expectation on a finite type#✓fully proved
Let \(\alpha\) be a finite set with a \(\sigma\)-algebra in which singletons are measurable, let \(p\) be a probability mass function on \(\alpha\), and write \(\mathbb{E}_p[h]\) for the expectation of \(h : \alpha \to \mathbb{R}\) under \(p\). For all \(f, g : \alpha \to \mathbb{R}\), \(\mathbb{E}_p[f + g] = \mathbb{E}_p[f] + \mathbb{E}_p[g]\).
No integrability hypothesis is needed.
theorem expect_add [Fintype α] : p.expect (f + g) = p.expect f + p.expect gUses 2
TheoremExpectation of a finite sum#✓fully proved
Let \(p\) be a probability mass function on a finite type \(\alpha\) carrying a σ-algebra in which singletons are measurable, and write \(\mathbb{E}_p[g]\) for the expectation of \(g : \alpha \to \mathbb{R}\) under \(p\). For every finite subset \(s\) of an index type \(\iota\) and every family of functions \(f_i : \alpha \to \mathbb{R}\), \(i \in \iota\), we have \(\mathbb{E}_p[a \mapsto \sum_{i \in s} f_i(a)] = \sum_{i \in s} \mathbb{E}_p[f_i]\).
theorem expect_sum [Fintype α] (s : Finset ι) (f : ι → α → ℝ) :
p.expect (fun a => ∑ i ∈ s, f i a) = ∑ i ∈ s, p.expect (f i)Uses 2
TheoremHomogeneity of expectation on a finite type#✓fully proved
Let \(\alpha\) be a finite set with a \(\sigma\)-algebra in which singletons are measurable, let \(p\) be a probability mass function on \(\alpha\), and write \(\mathbb{E}_p[h]\) for the expectation of \(h : \alpha \to \mathbb{R}\) under \(p\). For every \(c \in \mathbb{R}\) and \(f : \alpha \to \mathbb{R}\), the function \(a \mapsto c\,f(a)\) has expectation \(c\,\mathbb{E}_p[f]\).
theorem expect_const_mul [Fintype α] (c : ℝ) (f : α → ℝ) :
p.expect (fun a => c * f a) = c * p.expect fUses 2 · Used by 1
TheoremExpectation of a scalar multiple#✓fully proved
Let \(p\) be a probability mass function on a finite measurable space \(\alpha\) in which singletons are measurable, let \(c \in \mathbb{R}\) and let \(f : \alpha \to \mathbb{R}\). The expectation under \(p\) of the scalar multiple \(c f\) (the function \(a \mapsto c \cdot f(a)\)) equals \(c\) times the expectation of \(f\) under \(p\).
theorem expect_smul [Fintype α] (c : ℝ) (f : α → ℝ) :
p.expect (c • f) = c * p.expect fUses 2
TheoremNonnegativity of expectation#✓fully proved
Let \(p\) be a probability mass function on a finite measurable space \(\alpha\) in which singletons are measurable, and let \(f : \alpha \to \mathbb{R}\) satisfy \(f(a) \ge 0\) for every \(a \in \alpha\). Then the expectation of \(f\) under \(p\) is nonnegative.
theorem expect_nonneg [Fintype α] (hf : ∀ a, 0 ≤ f a) : 0 ≤ p.expect fUses 2
TheoremMonotonicity of expectation#✓fully proved
Let \(p\) be a probability mass function on a finite measurable space \(\alpha\) in which singletons are measurable, and let \(f, g : \alpha \to \mathbb{R}\) satisfy \(f(a) \le g(a)\) for every \(a \in \alpha\). Then the expectation of \(f\) under \(p\) is at most the expectation of \(g\) under \(p\).
theorem expect_le_expect [Fintype α] (hfg : ∀ a, f a ≤ g a) :
p.expect f ≤ p.expect gUses 2
TheoremExpectation of a finitely supported distribution#✓fully proved
Let \(p\) be a probability mass function on a measurable space \(\alpha\) in which singletons are measurable, and let \(s\) be a finite subset of \(\alpha\) such that \(p(a) = 0\) for every \(a \notin s\). Then for every function \(f : \alpha \to \mathbb{R}\), the expectation of \(f\) under \(p\) equals \(\sum_{a \in s} p(a) f(a)\).
No integrability hypothesis on \(f\) and no finiteness assumption on \(\alpha\) is needed.
theorem expect_eq_sum_of_finite_support (s : Finset α)
(hs : ∀ a ∉ s, p a = 0) (f : α → ℝ) :
p.expect f = ∑ a ∈ s, (p a).toReal * f aUses 1 · Used by 1
TheoremChange of variables for expectation#✓fully proved
Let \(p\) be a probability mass function on a finite measurable space \(\alpha\) in which singletons are measurable, let \(\beta\) be a measurable space in which singletons are measurable, and let \(g : \alpha \to \beta\) and \(f : \beta \to \mathbb{R}\). Write \(g_* p\) for the pushforward of \(p\) along \(g\), which gives each \(b \in \beta\) the mass \(\sum_{a :\, g(a) = b} p(a)\). Then the expectation of \(f\) under \(g_* p\) equals the expectation of \(f \circ g\) under \(p\).
theorem expect_map [Fintype α] [MeasurableSpace β]
[MeasurableSingletonClass β] (g : α → β) (f : β → ℝ) :
(p.map g).expect f = p.expect (f ∘ g)Uses 3
TheoremExpectation of an indicator#✓fully proved
Let \(p\) be a probability mass function on a finite measurable space \(\alpha\) in which singletons are measurable, and let \(q\) be a property of elements of \(\alpha\). The expectation under \(p\) of the function equal to \(1\) where \(q\) holds and \(0\) elsewhere is \(\sum_{a \in \alpha,\ q(a)} p(a)\), the total mass of the elements satisfying \(q\).
theorem expect_indicator_decide [Fintype α] (q : α → Prop)
[DecidablePred q] :
p.expect (fun a => if q a then 1 else 0) =
∑ a ∈ Finset.univ.filter q, (p a).toRealUses 2
DefinitionExtended expectation#✓fully proved
For a probability mass function \(p\) on a type \(\alpha\) and a function \(f : \alpha \to [0, \infty]\), the extended expectation of \(f\) under \(p\) is the unordered sum \(\sum_{a \in \alpha} p(a) f(a)\) in \([0, \infty]\), which always exists.
Unlike the real-valued expectation, it needs no measurability or integrability hypothesis and takes the value \(\infty\) when the expected value diverges, rather than collapsing to \(0\).
noncomputable def expectENN (p : PMF α) (f : α → ℝ≥0∞) : ℝ≥0∞ :=
∑' a, p a * f aUsed by 14
TheoremExtended expectation on a finite set#✓fully proved
Let \(p\) be a probability mass function on a finite set \(\alpha\). For every \(f : \alpha \to [0, \infty]\), the extended expectation of \(f\) under \(p\) equals the finite sum \(\sum_{a \in \alpha} p(a)\, f(a)\).
Uses 1 · Used by 2
TheoremExtended expectation of a constant#✓fully proved
Let \(p\) be a probability mass function on a set \(\alpha\). For every \(c \in [0, \infty]\), the extended expectation of the constant function \(a \mapsto c\) under \(p\) is \(c\).
The set \(\alpha\) need not be finite.
theorem expectENN_const (p : PMF α) (c : ℝ≥0∞) :
p.expectENN (fun _ => c) = cUses 1 · Used by 1
TheoremExtended expectation under the uniform distribution#✓fully proved
Let \(\alpha\) be a nonempty finite type and \(f : \alpha \to [0, \infty]\). The extended expectation of \(f\) under the uniform distribution on \(\alpha\) equals \(|\alpha|^{-1} \sum_{a \in \alpha} f(a)\), computed in \([0, \infty]\).
theorem expectENN_uniformOfFintype [Fintype α] [Nonempty α]
(f : α → ℝ≥0∞) :
(PMF.uniformFintype α).expectENN f =
(Fintype.card α : ℝ≥0∞)⁻¹ * ∑ a, f anoncomputable def uniformFintype (α : Type*) [Fintype α] [Nonempty α] : PMF α :=
ofFintype (fun _ => (Fintype.card α : ℝ≥0∞)⁻¹) (by
simp only [Finset.sum_const, Finset.card_univ, nsmul_eq_mul]
have h : (Fintype.card α : ℝ≥0∞) ≠ 0 := by
simpa only [Ne, Nat.cast_eq_zero] using (Fintype.card_ne_zero (α := α))
exact ENNReal.mul_inv_cancel h (ENNReal.natCast_ne_top (Fintype.card α)))MathlibExt/Probability/ProbabilityMassFunction/Uniform.lean:68
Uses 3 · Used by 2
TheoremAdditivity of extended expectation#✓fully proved
Let \(p\) be a probability mass function on a set \(\alpha\), and write \(\overline{\mathbb{E}}_p[h]\) for the extended expectation of \(h : \alpha \to [0, \infty]\) under \(p\). For all \(f, g : \alpha \to [0, \infty]\), \(\overline{\mathbb{E}}_p[f + g] = \overline{\mathbb{E}}_p[f] + \overline{\mathbb{E}}_p[g]\).
No finiteness or integrability hypothesis is needed: sums of terms in \([0, \infty]\) always converge.
theorem expectENN_add (p : PMF α) (f g : α → ℝ≥0∞) :
p.expectENN (f + g) = p.expectENN f + p.expectENN gUses 1
TheoremExtended expectation of a finite sum#✓fully proved
Let \(p\) be a probability mass function on a set \(\alpha\), and write \(\overline{\mathbb{E}}_p[h]\) for the extended expectation of \(h : \alpha \to [0, \infty]\) under \(p\). For every index set \(\iota\), finite subset \(s \subseteq \iota\) and family of functions \(f_i : \alpha \to [0, \infty]\) (\(i \in \iota\)), \(\overline{\mathbb{E}}_p\bigl[a \mapsto \sum_{i \in s} f_i(a)\bigr] = \sum_{i \in s} \overline{\mathbb{E}}_p[f_i]\).
The set \(\alpha\) need not be finite.
theorem expectENN_sum (p : PMF α) (s : Finset ι) (f : ι → α → ℝ≥0∞) :
p.expectENN (fun a => ∑ i ∈ s, f i a) =
∑ i ∈ s, p.expectENN (f i)Uses 1
TheoremExtended expectation under a finitely supported distribution#✓fully proved
Let \(p\) be a probability mass function on a set \(\alpha\), and let \(s \subseteq \alpha\) be a finite set with \(p(a) = 0\) for every \(a \notin s\). For every \(f : \alpha \to [0, \infty]\), the extended expectation of \(f\) under \(p\) equals \(\sum_{a \in s} p(a)\, f(a)\).
The set \(\alpha\) itself need not be finite.
theorem expectENN_eq_sum_of_finite_support (p : PMF α) (s : Finset α)
(hs : ∀ a ∉ s, p a = 0) (f : α → ℝ≥0∞) :
p.expectENN f = ∑ a ∈ s, p a * f aUses 1
TheoremChange of variables for extended expectation#✓fully proved
Let \(p\) be a probability mass function on a set \(\alpha\), let \(g : \alpha \to \beta\) be a map to a set \(\beta\), and let \(g_* p\) be the pushforward of \(p\) along \(g\), the probability mass function \(b \mapsto \sum_{a : g(a) = b} p(a)\). For every \(f : \beta \to [0, \infty]\), the extended expectation of \(f\) under \(g_* p\) equals the extended expectation of \(f \circ g\) under \(p\).
No finiteness or measurability hypothesis is needed: both sides are sums of terms in \([0, \infty]\), whose order of summation can be interchanged freely.
theorem expectENN_map (p : PMF α) (g : α → β) (f : β → ℝ≥0∞) :
(p.map g).expectENN f = p.expectENN (f ∘ g)Uses 1 · Used by 2
TheoremExtended and real expectations agree on natural-valued functions#✓fully proved
Let \(\alpha\) be a finite set with a \(\sigma\)-algebra in which singletons are measurable, let \(p\) be a probability mass function on \(\alpha\), and let \(g : \alpha \to \mathbb{N}\). Let \(x \in [0, \infty]\) be the extended expectation of \(g\), viewed as a function to \([0, \infty]\), under \(p\), and send \(x\) to \(\mathbb{R}\) by the map that is the identity on \([0, \infty)\) and sends \(\infty\) to \(0\). The result is the expectation of \(g\), viewed as a real-valued function, under \(p\).
theorem expectENN_natCast_toReal [Fintype α] (p : PMF α) (g : α → ℕ) :
(p.expectENN (fun a => (g a : ℝ≥0∞))).toReal =
p.expect (fun a => (g a : ℝ))Uses 4
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.