English
If s is locally closed, then local integrability on s is equivalent to integrability on every compact subset of s.
Русский
Если s локально замкнуто, то локальная интегрируемость на s эквивалентна интегрируемости на каждой компактной подмножество s.
LaTeX
$$$\\text{LocallyIntegrableOn}(f,s,μ) \\iff \\forall k\\subset s\\;\\text{IsCompact}(k)\\;\\text{IntegrableOn}(f,k,μ)$$$
Lean4
/-- If `s` is locally closed (e.g. open or closed), then `f` is locally integrable on `s` iff it is
integrable on every compact subset contained in `s`. -/
theorem locallyIntegrableOn_iff [PseudoMetrizableSpace ε] [LocallyCompactSpace X] (hs : IsLocallyClosed s) :
LocallyIntegrableOn f s μ ↔ ∀ (k : Set X), k ⊆ s → IsCompact k → IntegrableOn f k μ :=
by
refine ⟨fun hf k hk ↦ hf.integrableOn_compact_subset hk, fun hf x hx ↦ ?_⟩
rcases hs with ⟨U, Z, hU, hZ, rfl⟩
rcases exists_compact_subset hU hx.1 with ⟨K, hK, hxK, hKU⟩
rw [nhdsWithin_inter_of_mem (nhdsWithin_le_nhds <| hU.mem_nhds hx.1)]
refine ⟨Z ∩ K, inter_mem_nhdsWithin _ (mem_interior_iff_mem_nhds.1 hxK), ?_⟩
exact hf (Z ∩ K) (fun y hy ↦ ⟨hKU hy.2, hy.1⟩) (.inter_left hK hZ)
