English
Locally integrable on a closed set is equivalent to locally integrable with restricted measure on that set.
Русский
Локальная интегрируемость на замыкании равна локальной интегрируемости при ограниченной мере на этом множестве.
LaTeX
$$$\\text{IsClosed } s \\Rightarrow (\\operatorname{LocallyIntegrableOn} f s \\mu \\iff \\operatorname{LocallyIntegrable} f (\\mu.restrict s))$$$
Lean4
/-- If `f` is locally integrable with respect to `μ.restrict s`, it is locally integrable on `s`.
(See `locallyIntegrableOn_iff_locallyIntegrable_restrict` for an iff statement when `s` is
closed.) -/
theorem locallyIntegrableOn_of_locallyIntegrable_restrict [OpensMeasurableSpace X]
(hf : LocallyIntegrable f (μ.restrict s)) : LocallyIntegrableOn f s μ :=
by
intro x _
obtain ⟨t, ht_mem, ht_int⟩ := hf x
obtain ⟨u, hu_sub, hu_o, hu_mem⟩ := mem_nhds_iff.mp ht_mem
refine ⟨_, inter_mem_nhdsWithin s (hu_o.mem_nhds hu_mem), ?_⟩
simpa only [IntegrableOn, Measure.restrict_restrict hu_o.measurableSet, inter_comm] using ht_int.mono_set hu_sub
