English
If t is measurable and f vanishes on the complement of s inside t (for all x in t \ s), then the integral over t equals the integral over s.
Русский
Если t измеримо, и f = 0 на t \ s для всех x, то интеграл по t равен интегралу по s.
LaTeX
$$$$ \int_{x \in t} f(x) \, d\mu = \int_{x \in s} f(x) \, d\mu $$$$
Lean4
theorem integral_union_eq_left_of_ae (ht_eq : ∀ᵐ x ∂μ.restrict t, f x = 0) : ∫ x in s ∪ t, f x ∂μ = ∫ x in s, f x ∂μ :=
by
have ht : IntegrableOn f t μ := by apply integrableOn_zero.congr_fun_ae; symm; exact ht_eq
by_cases H : IntegrableOn f (s ∪ t) μ; swap
· rw [integral_undef H, integral_undef]; simpa [integrableOn_union, ht] using H
let f' := H.1.mk f
calc
∫ x : X in s ∪ t, f x ∂μ = ∫ x : X in s ∪ t, f' x ∂μ := integral_congr_ae H.1.ae_eq_mk
_ = ∫ x in s, f' x ∂μ :=
by
apply integral_union_eq_left_of_ae_aux _ H.1.stronglyMeasurable_mk (H.congr_fun_ae H.1.ae_eq_mk)
filter_upwards [ht_eq, ae_mono (Measure.restrict_mono subset_union_right le_rfl) H.1.ae_eq_mk] with x hx h'x
rw [← h'x, hx]
_ = ∫ x in s, f x ∂μ :=
integral_congr_ae (ae_mono (Measure.restrict_mono subset_union_left le_rfl) H.1.ae_eq_mk.symm)
