sum_left — Mathlib

English

The mutual singularity of a sum of measures with ν is equivalent to mutual singularity with each summand: sum μ ⟂ₘ ν iff ∀ i, μ i ⟂ₘ ν.

Русский

Взаимная несоединимость суммы мер с ν эквивалентна взаимной несоединимости каждого слагаемого: ∑ μ_i ⟂ₘ ν ⇔ ∀ i, μ_i ⟂ₘ ν.

LaTeX

$$$\\bigl(\\text{sum } \\mu \\bigr) \\perp_m \\nu \\quad\\iff\\quad \\forall i, \\mu_i \\perp_m \\nu$$$

Lean4

@[simp]
theorem sum_left {ι : Type*} [Countable ι] {μ : ι → Measure α} : sum μ ⟂ₘ ν ↔ ∀ i, μ i ⟂ₘ ν :=
  by
  refine ⟨fun h i => h.mono (le_sum _ _) le_rfl, fun H => ?_⟩
  choose s hsm hsμ hsν using H
  refine ⟨⋂ i, s i, MeasurableSet.iInter hsm, ?_, ?_⟩
  · rw [sum_apply _ (MeasurableSet.iInter hsm), ENNReal.tsum_eq_zero]
    exact fun i => measure_mono_null (iInter_subset _ _) (hsμ i)
  · rwa [compl_iInter, measure_iUnion_null_iff]

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