English
If f vanishes almost everywhere on t and is strongly measurable, then the integral over s ∪ t equals the integral over s, given integrability on s ∪ t.
Русский
Если f нулeвая почти повсюду на t и сильно измерима, то интеграл по s ∪ t равен интегралу по s при интегрируемости на s ∪ t.
LaTeX
$$$$ \int_{x \in s \cup t} f(x) \, d\mu = \int_{x \in s} f(x) \, d\mu $$$$
Lean4
theorem integral_union_eq_left_of_ae_aux (ht_eq : ∀ᵐ x ∂μ.restrict t, f x = 0) (haux : StronglyMeasurable f)
(H : IntegrableOn f (s ∪ t) μ) : ∫ x in s ∪ 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 _)
have h's : IntegrableOn f s μ := H.mono subset_union_left le_rfl
have A : ∀ u : Set X, ∫ x in u ∩ k, f x ∂μ = 0 := fun u => setIntegral_eq_zero_of_forall_eq_zero fun x hx => hx.2
rw [← integral_inter_add_diff hk h's, ← integral_inter_add_diff hk H, A, A, zero_add, zero_add, union_diff_distrib,
union_comm]
apply setIntegral_congr_set
rw [union_ae_eq_right]
apply measure_mono_null diff_subset
rw [measure_eq_zero_iff_ae_notMem]
filter_upwards [ae_imp_of_ae_restrict ht_eq] with x hx h'x using h'x.2 (hx h'x.1)
