A continuous family of linear maps applied to an integrable map is integrable on a compact set

Proved

JHolomorphic.IntegrableOn.continuousOn_clm_apply

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

sobolev-spacesweak-derivatives

Let $K\subseteq\mathbb{C}$ be compact, let $A:\mathbb{C}\to\mathrm{L}(E,F)$ be continuous on $K$ and let $f:\mathbb{C}\to E$ be integrable on $K$ . Then $z\mapsto A(z)\,f(z)$ is integrable on $K$ .

Formalization Note $E,F$ are finite-dimensional real normed spaces; $A$ is ℂ → E →L[ℝ] F; integrability is IntegrableOn · K for Lebesgue measure.

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

/-- If `A` is a continuous family of linear maps on a compact set `K` and `f` is integrable on
`K`, then `z ↦ A(z) f(z)` is integrable on `K`. -/
theorem IntegrableOn.continuousOn_clm_apply {E F : Type*} [NormedAddCommGroup E]
    [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F]
    [FiniteDimensional ℝ F] {K : Set ℂ} (hK : IsCompact K) {A : ℂ → E →L[ℝ] F}
    (hA : ContinuousOn A K) {f : ℂ → E} (hf : IntegrableOn f K) :
    IntegrableOn (fun z => A z (f z)) K := by
  sorry

end JHolomorphic

Source

Standard (weak derivatives and distribution theory).

View graph