Even reflection preserves first-order Sobolev membership, including p = infinity

Proved

HunterPDE.Compactness.memW_evenReflection

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

extension-operatorreflectionsobolev-spacesweak-derivative

Let $H=\{x\in\mathbb R^{m+1}:x_{m+1}>0\}$ and let $1\le p\le\infty$ . Define $R(x',t)=(x',|t|)$ and $Ef=f\circ R$ . Then

f\in W^{1,p}(H)\quad\Longrightarrow\quad Ef\in W^{1,p}(\mathbb R^{m+1}).

This is the weak differentiability part of the reflection construction suggested before Hunter's Theorem 3.41. The tangential weak derivatives reflect evenly, while the normal weak derivative reflects oddly. In particular the gluing across the boundary creates no distribution supported on the boundary. The hypotheses control integrability up to the boundary; merely knowing local weak differentiability inside the open half-space would not suffice. The endpoint $p=\infty$ is included and must not be deduced from finite-p norm density.

Preamble

import Definitions.Def_HunterPDE_Compactness_Sobolev
import Definitions.Def_HunterPDE_Compactness_HalfSpace
open MeasureTheory
open scoped ENNReal NNReal
set_option autoImplicit false

Formal statement

theorem HunterPDE.Compactness.memW_evenReflection (m : ℕ) (p : ℝ≥0∞) (hp : 1 ≤ p)
    (f : EuclideanSpace ℝ (Fin (m + 1)) → ℝ)
    (hf : HunterPDE.Compactness.MemW 1 p (HunterPDE.Compactness.upperHalfSpace m) f) :
    HunterPDE.Compactness.MemW 1 p Set.univ (fun x : EuclideanSpace ℝ (Fin (m + 1)) =>
      f (WithLp.toLp 2 (fun i => if i = Fin.last m then |x i| else x i))) := by sorry

Source

Hunter, Notes on Partial Differential Equations (revised 6/18/2014), §3.9, pp. 71–72, reflection construction preceding Theorem 3.41. https://www.math.ucdavis.edu/~hunter/pdes/pde_notes.pdf . This is an auxiliary lemma for the indicated construction, not a separately numbered assertion in the source.

View graph