toMeasure_ofMultiset_apply — Mathlib

English

For any measurable t, the measure of t under the PMF from s equals the sum of multiplicities of elements of s lying in t, divided by card(s).

Русский

Для измеримого множества t мера PMF, построенного из s, равна сумме кратностей элементов s, лежащих в t, деленной на card(s).

LaTeX

$$$$ (\\mathrm{ofMultiset}(s, hs).toMeasure\\; t) = \\frac{\\sum\\limits_{x} (s.filter(\\cdot \\in t)).\\mathrm{count}(x)}{\\mathrm{card}(s)} $$$$

Lean4

@[simp]
theorem toMeasure_ofMultiset_apply [MeasurableSpace α] (ht : MeasurableSet t) :
    (ofMultiset s hs).toMeasure t = (∑' x, (s.filter (· ∈ t)).count x : ℝ≥0∞) / (Multiset.card s) :=
  (toMeasure_apply_eq_toOuterMeasure_apply _ ht).trans (toOuterMeasure_ofMultiset_apply hs t)

Похожие утверждения