Representative-level H¹

Adapted from PDEFoundation (EllipticRegularity, 2026) with the author's permission. This port is the exact p = 2 facade over the independent CKN representative-level W1pFunction API.

Main definitions

• MemL2On and GradMemL2On: scalar and coordinatewise L² membership.
• H1Function: a concrete scalar representative with a chosen weak gradient.

Main results

• H1Function.restrict: restriction to an open subset.
• The conversion lemmas preserve values and gradients definitionally.

@[reducible, inline]

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

Scalar L² membership on a restricted domain.

Equations

• CKN.MemL2On U u = CKN.MemLpOn U 2 u

@[reducible, inline]

abbrev CKN.GradMemL2On {d : ℕ} (U : Set (Vec d)) (Du : Vec d → Vec d) : Prop

Coordinatewise gradient L² membership on a restricted domain.

Equations

• CKN.GradMemL2On U Du = CKN.GradMemLpOn U 2 Du

structure CKN.H1Function {d : ℕ} (U : Set (Vec d)) : Type

A concrete scalar representative and a chosen coordinate weak gradient in L²(U).

• toFun : Vec d → ℝ

  Chosen scalar representative of the H¹ function.

• grad : Vec d → Vec d

  Chosen weak gradient of the H¹ representative.

• memL2 : MemL2On U self.toFun
• gradMemL2 : GradMemL2On U self.grad
• hasWeakGradient : HasWeakGradientOn U self.toFun self.grad

@[instance_reducible]

instance CKN.instCoeFunH1FunctionForallVecReal {d : ℕ} {U : Set (Vec d)} : CoeFun (H1Function U) fun (x : H1Function U) => Vec d → ℝ

Equations

• CKN.instCoeFunH1FunctionForallVecReal = { coe := fun (u : CKN.H1Function U) => u.toFun }

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

Representative-level membership of a concrete function in H¹(U).

Equations

• CKN.MemH1 U u = ∃ (v : CKN.H1Function U), v.toFun = u

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

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

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

The coordinate weak-derivative identity stored in an H1Function.

theorem CKN.H1Function.grad_memL2 {d : ℕ} {U : Set (Vec d)} (u : H1Function U) (i : Fin d) : MemL2On U fun (x : Vec d) => u.grad x i

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

theorem CKN.H1Function.memH1 {d : ℕ} {U : Set (Vec d)} (u : H1Function U) : MemH1 U u.toFun

The underlying representative belongs to representative-level H¹(U).

def CKN.H1Function.toW1pFunction {d : ℕ} {U : Set (Vec d)} (u : H1Function U) : W1pFunction U 2

Regard an H1Function as the corresponding W1pFunction at p = 2.

Equations

• u.toW1pFunction = { toFun := u.toFun, grad := u.grad, memLp := ⋯, gradMemLp := ⋯, hasWeakGradient := ⋯ }

@[simp]

theorem CKN.H1Function.toW1pFunction_toFun {d : ℕ} {U : Set (Vec d)} (u : H1Function U) : u.toW1pFunction.toFun = u.toFun

@[simp]

theorem CKN.H1Function.toW1pFunction_grad {d : ℕ} {U : Set (Vec d)} (u : H1Function U) : u.toW1pFunction.grad = u.grad

@[simp]

theorem CKN.H1Function.toW1pFunction_apply {d : ℕ} {U : Set (Vec d)} (u : H1Function U) (x : Vec d) : u.toW1pFunction.toFun x = u.toFun x

def CKN.W1pFunction.toH1Function {d : ℕ} {U : Set (Vec d)} (u : W1pFunction U 2) : H1Function U

Regard a W1pFunction at p = 2 as the corresponding H1Function.

Equations

• u.toH1Function = { toFun := u.toFun, grad := u.grad, memL2 := ⋯, gradMemL2 := ⋯, hasWeakGradient := ⋯ }

@[simp]

theorem CKN.W1pFunction.toH1Function_toFun {d : ℕ} {U : Set (Vec d)} (u : W1pFunction U 2) : u.toH1Function.toFun = u.toFun

@[simp]

theorem CKN.W1pFunction.toH1Function_grad {d : ℕ} {U : Set (Vec d)} (u : W1pFunction U 2) : u.toH1Function.grad = u.grad

@[simp]

theorem CKN.W1pFunction.toH1Function_apply {d : ℕ} {U : Set (Vec d)} (u : W1pFunction U 2) (x : Vec d) : u.toH1Function.toFun x = u.toFun x

@[simp]

theorem CKN.H1Function.toH1Function_toW1pFunction {d : ℕ} {U : Set (Vec d)} (u : H1Function U) : u.toW1pFunction.toH1Function = u

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

Restrict an H1Function to an open subset.

Equations

• u.restrict hVOpen hVU = (u.toW1pFunction.restrict hVOpen hVU).toH1Function

@[simp]

theorem CKN.H1Function.restrict_toFun {d : ℕ} {U V : Set (Vec d)} (u : H1Function U) (hVOpen : IsOpen V) (hVU : V ⊆ U) : (u.restrict hVOpen hVU).toFun = u.toFun

@[simp]

theorem CKN.H1Function.restrict_grad {d : ℕ} {U V : Set (Vec d)} (u : H1Function U) (hVOpen : IsOpen V) (hVU : V ⊆ U) : (u.restrict hVOpen hVU).grad = u.grad

@[simp]

theorem CKN.H1Function.restrict_apply {d : ℕ} {U V : Set (Vec d)} (u : H1Function U) (hVOpen : IsOpen V) (hVU : V ⊆ U) (x : Vec d) : (u.restrict hVOpen hVU).toFun x = u.toFun x

@[simp]

theorem CKN.W1pFunction.toW1pFunction_toH1Function {d : ℕ} {U : Set (Vec d)} (u : W1pFunction U 2) : u.toH1Function.toW1pFunction = u