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