English
If s is locally closed and f is LocallyIntegrableOn f on s μ, then the product with a locally integrable scalar function is LocallyIntegrableOn.
Русский
Если s локально замкнуто и f локально интегрируема на s, то произведение на локально интегрируемую скалярную функцию тоже локально интегрируемо.
LaTeX
$$$\text{LocallyIntegrableOn}(f\cdot g, s, \mu)$$$
Lean4
theorem continuousOn_mul_of_subset (hg : ContinuousOn g K) (hg' : IntegrableOn g' A μ) (hK : IsCompact K)
(hA : MeasurableSet A) (hAK : A ⊆ K) : IntegrableOn (fun x => g x * g' x) A μ :=
by
rcases IsCompact.exists_bound_of_continuousOn hK hg with ⟨C, hC⟩
rw [IntegrableOn, ← memLp_one_iff_integrable] at hg' ⊢
have : ∀ᵐ x ∂μ.restrict A, ‖g x * g' x‖ ≤ C * ‖g' x‖ :=
by
filter_upwards [ae_restrict_mem hA] with x hx
refine (norm_mul_le _ _).trans ?_
gcongr
exact hC x (hAK hx)
exact MemLp.of_le_mul hg' (((hg.mono hAK).aestronglyMeasurable hA).mul hg'.aestronglyMeasurable) this
