English
Given s ⊆ t, almost everywhere f = 0 on t \ s, strong measurability of f, and integrability of f on t, the integral over t equals the integral over s.
Русский
Пусть s ⊆ t, почти всюду f = 0 на t \ s, f сильно измерим и интегрируем на t. Тогда ∫_t f = ∫_s f.
LaTeX
$$$$ \int_{x \in t} f(x) \, d\mu = \int_{x \in s} f(x) \, d\mu $$$$
Lean4
theorem setIntegral_eq_of_subset_of_ae_diff_eq_zero_aux (hts : s ⊆ t) (h't : ∀ᵐ x ∂μ, x ∈ t \ s → f x = 0)
(haux : StronglyMeasurable f) (h'aux : IntegrableOn f t μ) : ∫ x in t, f x ∂μ = ∫ x in s, f x ∂μ :=
by
let k := f ⁻¹' {0}
have hk : MeasurableSet k := by borelize E; exact haux.measurable (measurableSet_singleton _)
calc
∫ x in t, f x ∂μ = ∫ x in t ∩ k, f x ∂μ + ∫ x in t \ k, f x ∂μ := by rw [integral_inter_add_diff hk h'aux]
_ = ∫ x in t \ k, f x ∂μ := by rw [setIntegral_eq_zero_of_forall_eq_zero fun x hx => ?_, zero_add]; exact hx.2
_ = ∫ x in s \ k, f x ∂μ := by
apply setIntegral_congr_set
filter_upwards [h't] with x hx
change (x ∈ t \ k) = (x ∈ s \ k)
simp only [eq_iff_iff, and_congr_left_iff, mem_diff]
intro h'x
by_cases xs : x ∈ s
· simp only [xs, hts xs]
· simp only [xs, iff_false]
intro xt
exact h'x (hx ⟨xt, xs⟩)
_ = ∫ x in s ∩ k, f x ∂μ + ∫ x in s \ k, f x ∂μ :=
by
have : ∀ x ∈ s ∩ k, f x = 0 := fun x hx => hx.2
rw [setIntegral_eq_zero_of_forall_eq_zero this, zero_add]
_ = ∫ x in s, f x ∂μ := by rw [integral_inter_add_diff hk (h'aux.mono hts le_rfl)]
