Continuous maps on a compact subset of $\mathbb{C}$ are in $L^p$

Proved

JHolomorphic.memLp_of_continuousOn_compact

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

measure-theoryreal-analysis

Let $K\subset\mathbb{C}$ be compact, $X$ a normed group, $0<p\le\infty$ , and $f:\mathbb{C}\to X$ continuous on $K$ . Then $f\in L^p(K)$ for Lebesgue measure restricted to $K$ .

A convenience statement used to verify local integrability hypotheses for continuous data.

Formalization Note Membership is MemLp f p (volume.restrict K) with p : ℝ≥0∞; continuity is ContinuousOn f K.

Preamble

import Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
import Mathlib.Analysis.Calculus.ContDiff.Defs
import Mathlib.MeasureTheory.Integral.IntegrableOn
import Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
import Mathlib.Analysis.Complex.Basic
import Mathlib.MeasureTheory.Measure.Lebesgue.Complex

Formal statement

namespace JHolomorphic

open MeasureTheory Metric Filter Topology Set
open scoped ContDiff ENNReal

/-- A map that is continuous on a compact `K ⊆ ℂ` lies in `L^p(K)` for every `p`. -/
theorem memLp_of_continuousOn_compact {X : Type*} [NormedAddCommGroup X] {K : Set ℂ}
    (hK : IsCompact K) {p : ℝ≥0∞} {f : ℂ → X} (hf : ContinuousOn f K) :
    MemLp f p (volume.restrict K) := by
  sorry

end JHolomorphic

Source

Standard; Used for C. Wendl, Lectures on Symplectic Field Theory, arXiv:1612.01009, Lecture 2, Theorem 2.26

View graph

Continuous maps on a compact subset of C\mathbb{C}C are in LpL^pLp

Continuous maps on a compact subset of $\mathbb{C}$ are in $L^p$