sum_restrict_disjointed_spanningSets

English

If ν is sigma-finite, then μ equals the sum over n of μ restricted to disjointed(spanningSets(ν), n).

Русский

Если ν сигма-конечна, тогда μ равно сумма μ, ограниченной на disjointed(spanningSets(ν), n) по all n.

LaTeX

$$$\sum_{n=0}^{\infty} \mu\restriction (\mathrm{disjointed}(\mathrm{spanningSets}(\nu), n)) = \mu$$$

Lean4

theorem sum_restrict_disjointed_spanningSets (μ ν : Measure α) [SigmaFinite ν] :
    sum (fun n ↦ μ.restrict (disjointed (spanningSets ν) n)) = μ := by
  rw [← restrict_iUnion (disjoint_disjointed _) (MeasurableSet.disjointed (measurableSet_spanningSets _)),
    iUnion_disjointed, iUnion_spanningSets, restrict_univ]

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