English
If f is locally integrable and g is continuous with compact support, then the product f • g is integrable.
Русский
Если f локально интегрируема и g непрерывна с компактной опорой, то произведение f · g интегрируемо.
LaTeX
$$$\operatorname{LocallyIntegrable}(f, \mu) \land \operatorname{Continuous}(g) \land \operatorname{HasCompactSupport}(g) \Rightarrow \operatorname{Integrable}(x \mapsto f(x) \cdot g(x), \mu)$$$
Lean4
/-- If `f` is locally integrable and `g` is continuous with compact support,
then `f • g` is integrable. -/
theorem integrable_smul_right_of_hasCompactSupport {𝕜 : Type*} [NormedRing 𝕜] [Module 𝕜 E] [IsBoundedSMul 𝕜 E]
[OpensMeasurableSpace X] [T2Space X] {f : X → 𝕜} (hf : LocallyIntegrable f μ) {g : X → E} (hg : Continuous g)
(h'g : HasCompactSupport g) : Integrable (fun x ↦ f x • g x) μ :=
by
let K := tsupport g
have hK : IsCompact K := h'g
have : K.indicator (fun x ↦ f x • g x) = (fun x ↦ f x • g x) :=
by
apply indicator_eq_self.2
apply support_subset_iff'.2
intro x hx
simp [image_eq_zero_of_notMem_tsupport hx]
rw [← this, indicator_smul_left]
apply Integrable.smul_of_top_left
· rw [integrable_indicator_iff hK.measurableSet]
exact hf.integrableOn_isCompact hK
· exact hg.memLp_top_of_hasCompactSupport h'g μ
