Prove2Me

A sup bound for compactly supported W1,pW^{1,p} maps on a disc, p>2p>2

Proved
JHolomorphic.enorm_le_of_hasWeakPartialsOn_ball

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

sobolev-embeddingsobolev-spaces

Let p>2p>2 and let EE be a finite-dimensional real normed space. There is a constant CC with the following property. Let c∈Cc\in\mathbb{C}, ρ>0\rho>0, and let ξ:C→E\xi:\mathbb{C}\to E be continuous with tsupport⁡ξ⊆B(c,ρ)\operatorname{tsupport}\xi\subseteq B(c,\rho), whose weak partial derivatives ξs,ξt\xi_s,\xi_t on B(c,ρ)B(c,\rho) lie in Lp(B(c,ρ))L^p(B(c,\rho)). Then for every z∈Cz\in\mathbb{C}

∣ξ(z)∣≤C ρ1−2/p(∥ξs∥Lp(B(c,ρ))+∥ξt∥Lp(B(c,ρ))).|\xi(z)|\le C\,\rho^{1-2/p}\bigl(\|\xi_s\|_{L^p(B(c,\rho))}+\|\xi_t\|_{L^p(B(c,\rho))}\bigr).

This is the scale-invariant form of the embedding W01,p⊂L∞W^{1,p}_0\subset L^\infty in two dimensions for p>2p>2.

Formalization Note Weak partial derivatives are HasWeakPartialsOn on the open disc ball c ρ, tested against real C∞C^\infty functions with compact support in it; ξs\xi_s is the derivative in the direction 11 and ξt\xi_t in the direction ii. The left side is the extended norm ‖ξ z‖ₑ; the norms on the right are eLpNorm _ (ENNReal.ofReal p) for the Lebesgue measure restricted to the disc, and the factor is ENNReal.ofReal (C * ρ ^ (1 - 2 / p)). The constant CC depends only on pp and EE.

Preamble
import Definitions.Def_JHolomorphic_Setting
Formal statement
namespace JHolomorphic

open MeasureTheory Metric
open scoped ContDiff

/-- Let `p > 2`. There is a constant `C` such that for every disc `B(c, ρ) ⊆ ℂ` and every
continuous `ξ : ℂ → E` with `tsupport ξ ⊆ B(c, ρ)` whose weak partials `ξₛ`, `ξₜ` on the disc lie in
`L^p(B(c, ρ))`, one has `‖ξ(z)‖ ≤ C ρ^{1-2/p} (‖ξₛ‖_{L^p} + ‖ξₜ‖_{L^p})` for every `z ∈ ℂ`. -/
theorem enorm_le_of_hasWeakPartialsOn_ball {E : Type*} [NormedAddCommGroup E]
    [NormedSpace ℝ E] [FiniteDimensional ℝ E] (p : ℝ) (hp : 2 < p) :
    ∃ C : ℝ, ∀ (c : ℂ) (ρ : ℝ), 0 < ρ → ∀ ξ ξs ξt : ℂ → E, Continuous ξ →
      tsupport ξ ⊆ ball c ρ → HasWeakPartialsOn (ball c ρ) ξ ξs ξt →
      MemLp ξs (ENNReal.ofReal p) (volume.restrict (ball c ρ)) →
      MemLp ξt (ENNReal.ofReal p) (volume.restrict (ball c ρ)) →
      ∀ z, ‖ξ z‖ₑ ≤ ENNReal.ofReal (C * ρ ^ (1 - 2 / p)) *
        (eLpNorm ξs (ENNReal.ofReal p) (volume.restrict (ball c ρ)) +
          eLpNorm ξt (ENNReal.ofReal p) (volume.restrict (ball c ρ))) := by
  sorry

end JHolomorphic
Source
Morrey's inequality; see L. C. Evans, Partial Differential Equations, §5.6.2, and D. Gilbarg, N. Trudinger, Elliptic PDE of Second Order, Theorem 7.10 and Theorem 7.17

View graph