English
If measures and sets satisfy measurability, then the product of a function and a scalar-valued function is integrable on A with respect to μ.
Русский
Если множество и измерения удовлетворяют условию измеримости, то произведение функции на скалярную функцию интегрируемо на A по мере μ.
LaTeX
$$$\text{IntegrableOn}(f\cdot g, A, \mu)$$$
Lean4
theorem mul_continuousOn_of_subset (hg : IntegrableOn g A μ) (hg' : ContinuousOn g' K) (hA : MeasurableSet A)
(hK : IsCompact K) (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 ?_
rw [mul_comm]
gcongr
exact hC x (hAK hx)
exact MemLp.of_le_mul hg (hg.aestronglyMeasurable.mul <| (hg'.mono hAK).aestronglyMeasurable hA) this
