English
If μ is locally finite and f is LocallyIntegrableOn on s, then f is LocallyIntegrableOn on any subset A ⊆ s that is measurable.
Русский
Если μ локально конечна и f локально интегрируема на s, то на любом измеримом подмножестве A ⊆ s f локально интегрируемо.
LaTeX
$$$\text{LocallyIntegrableOn}(f, A, \mu)$$$
Lean4
theorem continuousOn_smul_of_subset [SecondCountableTopologyEither X 𝕜] {f : X → 𝕜} (hf : ContinuousOn f K) {g : X → E}
(hg : IntegrableOn g A μ) (hK : IsCompact K) (hA : MeasurableSet A) (hAK : A ⊆ K) :
IntegrableOn (fun x => f x • g x) A μ :=
by
rcases IsCompact.exists_bound_of_continuousOn hK hf with ⟨C, hC⟩
rw [IntegrableOn, ← memLp_one_iff_integrable] at hg ⊢
have : ∀ᵐ x ∂μ.restrict A, ‖f x • g x‖ ≤ C * ‖g x‖ :=
by
filter_upwards [ae_restrict_mem hA] with x hx
refine (norm_smul_le _ _).trans ?_
gcongr
exact hC x (hAK hx)
exact MemLp.of_le_mul hg (((hf.mono hAK).aestronglyMeasurable hA).smul hg.aestronglyMeasurable) this
