sum_left — Mathlib

English

If μ_i have Lebesgue decomposition with respect to ν for a countable index set, then their sum has Lebesgue decomposition with respect to ν.

Русский

Если для счётной family μ_i существует разложение Лебега относительно ν, тогда сумма μ = ∑ μ_i имеет разложение относительно ν.

LaTeX

$$∀ μ_i, [HaveLebesgueDecomposition (μ_i) ν] → HaveLebesgueDecomposition (∑ μ_i) ν$$

Lean4

instance sum_left {ι : Type*} [Countable ι] (μ : ι → Measure α) [∀ i, HaveLebesgueDecomposition (μ i) ν] :
    HaveLebesgueDecomposition (.sum μ) ν :=
  ⟨(.sum fun i ↦ (μ i).singularPart ν, ∑' i, rnDeriv (μ i) ν), by dsimp only; fun_prop, by
    simp [mutuallySingular_singularPart], by
    simp [withDensity_tsum, measurable_rnDeriv, Measure.sum_add_sum, singularPart_add_rnDeriv]⟩

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