A compactly supported continuous weight times a locally integrable map is integrable

Proved

JHolomorphic.integrable_smul_of_integrableOn_compact

by Mazecto · Oct 21, 2026 · Mathlib 0df444a (Lean v4.33.1)

sobolev-spacesweak-derivatives

Let $U\subseteq\mathbb{C}$ , let $f:\mathbb{C}\to E$ be integrable on every compact subset of $U$ , and let $g:\mathbb{C}\to\mathbb{R}$ be continuous on $U$ with compact support contained in $U$ . Then $z\mapsto g(z)\,f(z)$ is integrable on $\mathbb{C}$ .

Formalization Note $E$ is a real normed space; the support condition is HasCompactSupport g and tsupport g ⊆ U; continuity is ContinuousOn g U; integrability is with respect to Lebesgue measure on $\mathbb{C}$ .

Preamble

import Definitions.Def_JHolomorphic_Setting
import Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff
import Mathlib.Analysis.Calculus.FDeriv.Symmetric
import Mathlib.Analysis.Calculus.FDeriv.Mul
import Mathlib.Analysis.Calculus.ContDiff.Operations
import Mathlib.Analysis.Calculus.ContDiff.Comp

Formal statement

namespace JHolomorphic

open MeasureTheory Filter Topology
open scoped ContDiff

/-- A real function that is continuous on `U` and has compact support in `U`, times a map that is
integrable on every compact subset of `U`, is integrable on `ℂ`. -/
theorem integrable_smul_of_integrableOn_compact {E : Type*} [NormedAddCommGroup E]
    [NormedSpace ℝ E] {U : Set ℂ} {f : ℂ → E} (hf : ∀ K ⊆ U, IsCompact K → IntegrableOn f K)
    {g : ℂ → ℝ} (hg : ContinuousOn g U) (hgc : HasCompactSupport g) (hgU : tsupport g ⊆ U) :
    Integrable (fun z => g z • f z) := by
  sorry

end JHolomorphic

Source

Standard (weak derivatives and distribution theory).

View graph