Prove2Me

An LpL^p bound for the derivative of the lift z↦(u(z),Du(z)e)z\mapsto(u(z),Du(z)e) on a compact set

Proved
JHolomorphic.eLpNorm_fderiv_lift_le

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

calculussobolev-spaces

Let EE be a finite-dimensional real normed space, U⊆CU\subseteq\mathbb{C} open, u:U→Eu:U\to E smooth, 1≤p<∞1\le p<\infty, e∈Ce\in\mathbb{C} with ∣e∣≤1|e|\le1, and K⊆UK\subseteq U compact. If ∥Du∥Lp(K)≤C1\|Du\|_{L^p(K)}\le C_1 and ∥D2u∥Lp(K)≤C2\|D^2u\|_{L^p(K)}\le C_2, then the map v(w)=(u(w),Du(w)e)v(w)=\bigl(u(w),Du(w)e\bigr) satisfies

∥Dv∥Lp(K)≤C1+C2.\|Dv\|_{L^p(K)}\le C_1+C_2.

This bound transfers W2,pW^{2,p} bounds on uu to W1,pW^{1,p} bounds on its tangent lifts.

Formalization Note The hypotheses are ContDiffOn ℝ ∞ u U, IsOpen U, K' ⊆ U, IsCompact K' and 1 ≤ p. The norms are eLpNorm _ (ENNReal.ofReal p) (volume.restrict K') of fderiv ℝ u, fderiv ℝ (fderiv ℝ u) and fderiv ℝ (fun z => (u z, fderiv ℝ u z e)), with C₁ C₂ : ℝ≥0.

Preamble
import Definitions.Def_JHolomorphic_Setting
import Mathlib.Analysis.Normed.Operator.Prod
Formal statement
namespace JHolomorphic

open MeasureTheory Metric Filter Topology
open scoped ContDiff ENNReal NNReal

/-- Let `1 ≤ p` and let `u` be `C^∞` on an open set `U ⊆ ℂ`. For `‖e‖ ≤ 1` and a compact
`K ⊆ U`, the `L^p(K)` norm of the derivative of the lift `z ↦ (u(z), Du(z) e)` is at most
`C₁ + C₂` whenever `‖Du‖_{L^p(K)} ≤ C₁` and `‖D²u‖_{L^p(K)} ≤ C₂`. -/
theorem eLpNorm_fderiv_lift_le {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    [FiniteDimensional ℝ E] (p : ℝ) (hp : 1 ≤ p) (U : Set ℂ) (hU : IsOpen U) (u : ℂ → E)
    (hu : ContDiffOn ℝ ∞ u U) (e : ℂ) (he : ‖e‖ ≤ 1) (K' : Set ℂ) (hK'U : K' ⊆ U)
    (hK' : IsCompact K') (C₁ C₂ : ℝ≥0)
    (h1 : eLpNorm (fderiv ℝ u) (ENNReal.ofReal p) (volume.restrict K') ≤ C₁)
    (h2 : eLpNorm (fderiv ℝ (fderiv ℝ u)) (ENNReal.ofReal p) (volume.restrict K') ≤ C₂) :
    eLpNorm (fderiv ℝ (fun z => (u z, fderiv ℝ u z e))) (ENNReal.ofReal p)
      (volume.restrict K') ≤ (C₁ + C₂ : ℝ≥0) := by
  sorry

end JHolomorphic
Source
Elementary differential calculus; used for C. Wendl, Lectures on Symplectic Field Theory, arXiv:1612.01009, Lecture 2, Theorem 2.22

View graph