toOuterMeasure_ofMultiset_apply — Mathlib

English

For any set t, the outer 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).toOuterMeasure)\; t = \\frac{\\sum\\limits_{x} (s.filter(\\cdot \\in t)).\\mathrm{count}(x)}{\\mathrm{card}(s)} $$$$

Lean4

@[simp]
theorem toOuterMeasure_ofMultiset_apply :
    (ofMultiset s hs).toOuterMeasure t = (∑' x, (s.filter (· ∈ t)).count x : ℝ≥0∞) / (Multiset.card s) :=
  by
  simp_rw [div_eq_mul_inv, ← ENNReal.tsum_mul_right, toOuterMeasure_apply]
  refine tsum_congr fun x => ?_
  by_cases hx : x ∈ t <;> simp [Set.indicator, hx, div_eq_mul_inv]

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