English
Same as above: closed-set restriction equivalence for local integrability.
Русский
То же самое: эквивалентность локальной интегрируемости при ограничении на замыкании.
LaTeX
$$$\\text{IsClosed } s \\Rightarrow (\\operatorname{LocallyIntegrableOn} f s \\mu \\iff \\operatorname{LocallyIntegrable} f (\\mu.restrict s))$$$
Lean4
/-- If `s` is closed, being locally integrable on `s` w.r.t. `μ` is equivalent to being locally
integrable with respect to `μ.restrict s`. For the one-way implication without assuming `s` closed,
see `locallyIntegrableOn_of_locallyIntegrable_restrict`. -/
theorem locallyIntegrableOn_iff_locallyIntegrable_restrict [OpensMeasurableSpace X] (hs : IsClosed s) :
LocallyIntegrableOn f s μ ↔ LocallyIntegrable f (μ.restrict s) :=
by
refine ⟨fun hf x => ?_, locallyIntegrableOn_of_locallyIntegrable_restrict⟩
by_cases h : x ∈ s
· obtain ⟨t, ht_nhds, ht_int⟩ := hf x h
obtain ⟨u, hu_o, hu_x, hu_sub⟩ := mem_nhdsWithin.mp ht_nhds
refine ⟨u, hu_o.mem_nhds hu_x, ?_⟩
rw [IntegrableOn, restrict_restrict hu_o.measurableSet]
exact ht_int.mono_set hu_sub
· rw [← isOpen_compl_iff] at hs
refine ⟨sᶜ, hs.mem_nhds h, ?_⟩
rw [IntegrableOn, restrict_restrict, inter_comm, inter_compl_self, ← IntegrableOn]
exacts [integrableOn_empty, hs.measurableSet]
