sum_measureReal_le_measureReal_univ

English

For a Finset s in α, the sum of μ.real {b} over b ∈ s equals μ.real s, provided μ is measurable and Sigma-finite with respect to μ.

Русский

Для Finset s и μ, сумма μ.real {b} по b ∈ s равна μ.real s при условии измеримости и существования связной меры.

LaTeX

$$(∑ b ∈ s, μ.real { b }) = μ.real s$$

Lean4

theorem sum_measureReal_le_measureReal_univ [IsFiniteMeasure μ] {s : Finset ι} {t : ι → Set α}
    (h : ∀ i ∈ s, MeasurableSet (t i)) (H : Set.PairwiseDisjoint (↑s) t) : (∑ i ∈ s, μ.real (t i)) ≤ μ.real univ :=
  by
  simp only [measureReal_def]
  rw [← ENNReal.toReal_sum (fun i hi ↦ measure_ne_top _ _)]
  apply ENNReal.toReal_mono (measure_ne_top _ _)
  exact sum_measure_le_measure_univ (fun i mi ↦ (h i mi).nullMeasurableSet) H.aedisjoint

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