English
Bernoulli(p,h) depends only on p; if p = p' then Bernoulli(p,h) = Bernoulli(p',h).
Русский
Распределение Бернулли зависит только от p; если p = p', то Bernoulli(p,h) = Bernoulli(p',h).
LaTeX
$$$ p = p' \Rightarrow \mathrm{bernoulli}(p,h) = \mathrm{bernoulli}(p',h) $$$
Lean4
theorem integral_eq_tsum (p : PMF α) (f : α → E) (hf : Integrable f p.toMeasure) :
∫ a, f a ∂(p.toMeasure) = ∑' a, (p a).toReal • f a :=
calc
_ = ∫ a in p.support, f a ∂(p.toMeasure) := by rw [restrict_toMeasure_support p]
_ = ∑' (a : support p), (p.toMeasure { a.val }).toReal • f a :=
by
apply integral_countable f p.support_countable
rwa [IntegrableOn, restrict_toMeasure_support p]
_ = ∑' (a : support p), (p a).toReal • f a := by
congr with x; congr 2
apply PMF.toMeasure_apply_singleton p x (MeasurableSet.singleton _)
_ = ∑' a, (p a).toReal • f a :=
tsum_subtype_eq_of_support_subset <|
calc
(fun a ↦ (p a).toReal • f a).support ⊆ (fun a ↦ (p a).toReal).support := Function.support_smul_subset_left _ _
_ ⊆ support p := fun x h1 h2 => h1 (by simp [h2])
