English
If f vanishes on t \ s for all x in t \ s, then the integrals over t and s coincide.
Русский
Если 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
/-- If a function vanishes almost everywhere on `t \ s` with `s ⊆ t`, then its integrals on `s`
and `t` coincide if `t` is null-measurable. -/
theorem setIntegral_eq_of_subset_of_ae_diff_eq_zero (ht : NullMeasurableSet t μ) (hts : s ⊆ t)
(h't : ∀ᵐ x ∂μ, x ∈ t \ s → f x = 0) : ∫ x in t, f x ∂μ = ∫ x in s, f x ∂μ :=
by
by_cases h : IntegrableOn f t μ; swap
· have : ¬IntegrableOn f s μ := fun H => h (H.of_ae_diff_eq_zero ht h't)
rw [integral_undef h, integral_undef this]
let f' := h.1.mk f
calc
∫ x in t, f x ∂μ = ∫ x in t, f' x ∂μ := integral_congr_ae h.1.ae_eq_mk
_ = ∫ x in s, f' x ∂μ :=
by
apply setIntegral_eq_of_subset_of_ae_diff_eq_zero_aux hts _ h.1.stronglyMeasurable_mk (h.congr h.1.ae_eq_mk)
filter_upwards [h't, ae_imp_of_ae_restrict h.1.ae_eq_mk] with x hx h'x h''x
rw [← h'x h''x.1, hx h''x]
_ = ∫ x in s, f x ∂μ := by
apply integral_congr_ae
apply ae_restrict_of_ae_restrict_of_subset hts
exact h.1.ae_eq_mk.symm
