setIntegral_neg_eq_setIntegral_nonpos

English

For a partition of space into measurable sets, the integral of f is the sum of integrals over the parts when f is integrable on the union.

Русский

Для разбиения пространства на измеримые части интеграл от f равен сумме интегралов по частям, если f интегрируем на объединении.

LaTeX

$$$$ \int f = \sum_i \int_{i} f $$$$

Lean4

theorem setIntegral_neg_eq_setIntegral_nonpos [PartialOrder E] {f : X → E} (hf : AEStronglyMeasurable f μ) :
    ∫ x in {x | f x < 0}, f x ∂μ = ∫ x in {x | f x ≤ 0}, f x ∂μ :=
  by
  have h_union : {x | f x ≤ 0} = {x | f x < 0} ∪ {x | f x = 0} := by simp_rw [le_iff_lt_or_eq, setOf_or]
  rw [h_union]
  have B : NullMeasurableSet {x | f x = 0} μ := hf.nullMeasurableSet_eq_fun aestronglyMeasurable_zero
  symm
  refine integral_union_eq_left_of_ae ?_
  filter_upwards [ae_restrict_mem₀ B] with x hx using hx

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