UnitCubeSkewW2Infinity

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

structure Algsuperdiff.Frozen.Section24.UnitCubeSkewW2Infinity (d : ℕ) : Type

A skew field with essentially bounded weak derivatives through order two on the unit cube.

• toLInfSkewMatrixFieldOn : LInfSkewMatrixFieldOn (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0))

  The underlying essentially bounded skew field.

• firstDeriv : HCPolySupport.Vec d → HCPolySupport.Vec d →L[ℝ] HCPolySupport.Mat d

  The stored first weak derivative.

• secondDeriv : HCPolySupport.Vec d → HCPolySupport.Vec d →L[ℝ] HCPolySupport.Vec d →L[ℝ] HCPolySupport.Mat d

  The stored second weak derivative.

• firstDeriv_memLp (k i j : Fin d) : MeasureTheory.MemLp (fun (x : HCPolySupport.Vec d) => (self.firstDeriv x) (HCPolySupport.basisVec k) i j) ⊤ (HCPolySupport.volumeMeasureOn (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0)).carrier)
• secondDeriv_memLp (l k i j : Fin d) : MeasureTheory.MemLp (fun (x : HCPolySupport.Vec d) => ((self.secondDeriv x) (HCPolySupport.basisVec l)) (HCPolySupport.basisVec k) i j) ⊤ (HCPolySupport.volumeMeasureOn (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0)).carrier)
• hasWeakPartialDeriv_value (k i j : Fin d) : HCPolySupport.HasWeakPartialDerivOn (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0)).carrier k (fun (x : HCPolySupport.Vec d) => ↑↑self.toLInfSkewMatrixFieldOn x i j) fun (x : HCPolySupport.Vec d) => (self.firstDeriv x) (HCPolySupport.basisVec k) i j
• hasWeakPartialDeriv_firstDeriv (l k i j : Fin d) : HCPolySupport.HasWeakPartialDerivOn (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0)).carrier l (fun (x : HCPolySupport.Vec d) => (self.firstDeriv x) (HCPolySupport.basisVec k) i j) fun (x : HCPolySupport.Vec d) => ((self.secondDeriv x) (HCPolySupport.basisVec l)) (HCPolySupport.basisVec k) i j