absolutelyContinuous_sum_left — Mathlib

English

If each μs(i) is absolutely continuous with respect to ν, then the sum Measure.sum μs is absolutely continuous with respect to ν.

Русский

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

LaTeX

$$$\forall i,\; μ_s(i) \ll ν \;\Rightarrow \; (\sum_i μ_s(i)) \ll ν$$$

Lean4

theorem absolutelyContinuous_sum_left {μs : ι → Measure α} (hμs : ∀ i, μs i ≪ ν) : Measure.sum μs ≪ ν :=
  AbsolutelyContinuous.mk fun s hs hs0 ↦ by simp [sum_apply _ hs, fun i ↦ hμs i hs0]

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