English
If support of f is contained in s, integrability on s is equivalent to integrability of f on all of α.
Русский
Если поддержка f⊆s, интегрируемость на s эквивалентна интегрируемости на всё множество.
LaTeX
$$support f ⊆ s → IntegrableOn f s μ ↔ Integrable f μ$$
Lean4
/-- If a function is integrable on a set `s`, and its enorm vanishes on `t \ s`,
then it is integrable on `t` if `t` is null-measurable. -/
theorem of_ae_diff_eq_zero {f : α → ε'} (hf : IntegrableOn f s μ) (ht : NullMeasurableSet t μ)
(h't : ∀ᵐ x ∂μ, x ∈ t \ s → f x = 0) : IntegrableOn f t μ :=
by
let u := {x ∈ s | f x ≠ 0}
have hu : IntegrableOn f u μ := hf.mono_set fun x hx => hx.1
let v := toMeasurable μ u
have A : IntegrableOn f v μ := by
rw [IntegrableOn, hu.restrict_toMeasurable]
· exact hu
· intro x hx; simpa using hx.2
have B : IntegrableOn f (t \ v) μ := by
apply integrableOn_zero.congr
filter_upwards [ae_restrict_of_ae h't,
ae_restrict_mem₀ (ht.diff (measurableSet_toMeasurable μ u).nullMeasurableSet)] with x hxt hx
by_cases h'x : x ∈ s
· by_contra H
exact hx.2 (subset_toMeasurable μ u ⟨h'x, Ne.symm H⟩)
· exact (hxt ⟨hx.1, h'x⟩).symm
apply (A.union B).mono_set _
rw [union_diff_self]
exact subset_union_right
