Representative-level W^{1,p}

Adapted from PDEFoundation (EllipticRegularity, 2026) with the author's permission. This independent port stores concrete value and gradient representatives and uses the CKN weak-gradient API.

Main definitions

• MemLpOn and GradMemLpOn: scalar and coordinatewise L^p membership.
• W1pFunction: a concrete representative with a chosen weak gradient.
• MemW1p: representative-level membership in W^{1,p}.

Main results

• W1pFunction.restrict: restriction to an open subset.

@[reducible, inline]

abbrev CKN.MemLpOn {d : ℕ} (U : Set (Vec d)) (p : ENNReal) (u : Vec d → ℝ) : Prop

Scalar L^p membership on a restricted domain.

Equations

• CKN.MemLpOn U p u = MeasureTheory.MemLp u p (CKN.volumeOn U)

def CKN.GradMemLpOn {d : ℕ} (U : Set (Vec d)) (p : ENNReal) (Du : Vec d → Vec d) : Prop

Coordinatewise gradient L^p membership on a restricted domain.

Equations

• CKN.GradMemLpOn U p Du = ∀ (i : Fin d), CKN.MemLpOn U p fun (x : CKN.Vec d) => Du x i

structure CKN.W1pFunction {d : ℕ} (U : Set (Vec d)) (p : ENNReal) : Type

A concrete representative and a chosen coordinate weak gradient.

• toFun : Vec d → ℝ

  Chosen scalar representative of the W¹ᵖ function.

• grad : Vec d → Vec d

  Chosen weak gradient of the W¹ᵖ representative.

• memLp : MemLpOn U p self.toFun
• gradMemLp : GradMemLpOn U p self.grad
• hasWeakGradient : HasWeakGradientOn U self.toFun self.grad

@[instance_reducible]

instance CKN.instCoeFunW1pFunctionForallVecReal {d : ℕ} {U : Set (Vec d)} {p : ENNReal} : CoeFun (W1pFunction U p) fun (x : W1pFunction U p) => Vec d → ℝ

Equations

• CKN.instCoeFunW1pFunctionForallVecReal = { coe := fun (u : CKN.W1pFunction U p) => u.toFun }

def CKN.MemW1p {d : ℕ} (U : Set (Vec d)) (p : ENNReal) (u : Vec d → ℝ) : Prop

Representative-level membership of a concrete function in W^{1,p}.

Equations

• CKN.MemW1p U p u = ∃ (v : CKN.W1pFunction U p), v.toFun = u

theorem CKN.memLpOn_mono {d : ℕ} {U V : Set (Vec d)} {p : ENNReal} {u : Vec d → ℝ} (hVU : V ⊆ U) (hu : MemLpOn U p u) : MemLpOn V p u

Restriction preserves scalar L^p membership.

theorem CKN.gradMemLpOn_mono {d : ℕ} {U V : Set (Vec d)} {p : ENNReal} {Du : Vec d → Vec d} (hVU : V ⊆ U) (hDu : GradMemLpOn U p Du) : GradMemLpOn V p Du

Restriction preserves coordinatewise gradient L^p membership.

theorem CKN.W1pFunction.ext {d : ℕ} {U : Set (Vec d)} {p : ENNReal} {u v : W1pFunction U p} (htoFun : u.toFun = v.toFun) (hgrad : u.grad = v.grad) : u = v

theorem CKN.W1pFunction.ext_iff {d : ℕ} {U : Set (Vec d)} {p : ENNReal} {u v : W1pFunction U p} : u = v ↔ u.toFun = v.toFun ∧ u.grad = v.grad

theorem CKN.W1pFunction.hasWeakPartialDerivOn {d : ℕ} {U : Set (Vec d)} {p : ENNReal} (u : W1pFunction U p) (i : Fin d) : HasWeakPartialDerivOn U i u.toFun fun (x : Vec d) => u.grad x i

The chosen coordinate weak derivative stored in a W1p representative.

theorem CKN.W1pFunction.grad_memLp {d : ℕ} {U : Set (Vec d)} {p : ENNReal} (u : W1pFunction U p) (i : Fin d) : MemLpOn U p fun (x : Vec d) => u.grad x i

The ith chosen gradient component belongs to L^p(U).

theorem CKN.W1pFunction.memW1p {d : ℕ} {U : Set (Vec d)} {p : ENNReal} (u : W1pFunction U p) : MemW1p U p u.toFun

The underlying representative belongs to representative-level W^{1,p}.

def CKN.W1pFunction.restrict {d : ℕ} {U V : Set (Vec d)} {p : ENNReal} (u : W1pFunction U p) (hVOpen : IsOpen V) (hVU : V ⊆ U) : W1pFunction V p

Restrict a representative-level Sobolev function to an open subset.

Equations

• u.restrict hVOpen hVU = { toFun := u.toFun, grad := u.grad, memLp := ⋯, gradMemLp := ⋯, hasWeakGradient := ⋯ }