absolutelyContinuous_sum_right — Mathlib

English

If ν is absolutely continuous with respect to each μs(i) in a family, then ν is absolutely continuous with respect to the sum of the μs.

Русский

Если ν ≪ μs(i) для каждого i, то ν ≪ сумма μs.

LaTeX

$$∀ i, ν ≪ μs(i) → ν ≪ (∑ i μs(i))$$

Lean4

theorem absolutelyContinuous_sum_right {μs : ι → Measure α} (i : ι) (hνμ : ν ≪ μs i) : ν ≪ Measure.sum μs :=
  by
  refine AbsolutelyContinuous.mk fun s hs hs0 ↦ ?_
  simp only [sum_apply _ hs, ENNReal.tsum_eq_zero] at hs0
  exact hνμ (hs0 i)

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