measure_iUnion_toReal — Mathlib

English

If ι is finite and π is a prepartition of I, then the real-measure of the iUnion equals the sum of the real-measures of the pieces: μ.real(π.iUnion) = ∑_{J∈π.boxes} μ.real(J).

Русский

Если ι конечен и π — предразбиение I, то мера μ.real по объединению равно сумме мер μ.real по элементам разбиения: μ.real(π.iUnion) = ∑ μ.real(J).

LaTeX

$$$\\mu^{\\mathrm{real}}(\\pi.iUnion) = \\sum_{J \\in \\pi.boxes} \\mu^{\\mathrm{real}}(J)$$$

Lean4

theorem measure_iUnion_toReal [Finite ι] {I : Box ι} (π : Prepartition I) (μ : Measure (ι → ℝ))
    [IsLocallyFiniteMeasure μ] : μ.real π.iUnion = ∑ J ∈ π.boxes, μ.real J :=
  by
  simp only [measureReal_def]
  rw [← ENNReal.toReal_sum (fun J _ => (J.measure_coe_lt_top μ).ne), π.iUnion_def]
  simp only [← mem_boxes]
  rw [measure_biUnion_finset π.pairwiseDisjoint]
  exact fun J _ => J.measurableSet_coe

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