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