Coarse-graining support: Support.Sobolev.W1p.CubeVector

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

Vector-valued W^{1,p} functions on cubes

This file packages a vector field coordinatewise as genuine scalar W1pFunction witnesses on an open cube. Its Jacobian is the matrix of the stored weak gradients. All L^p statements use normalized cube measure, but the carrier itself contains no cube-scale-dependent quantity.

structure HCPolySupport.CubeVectorW1pFunction {d : ℕ} (Q : TriadicCube d) (p : FiniteLpExponent) : Type

A vector-valued W^{1,p} function on an open cube, represented by one genuine scalar W1pFunction for each coordinate.

• coord : Fin d → W1pFunction (openCubeSet Q) p.exponent

  Scalar W¹,p witnesses for the vector-field coordinates, whose weak gradients form the Jacobian.

theorem HCPolySupport.CubeVectorW1pFunction.ext_iff {d : ℕ} {Q : TriadicCube d} {p : FiniteLpExponent} {x y : CubeVectorW1pFunction Q p} : x = y ↔ x.coord = y.coord

theorem HCPolySupport.CubeVectorW1pFunction.ext {d : ℕ} {Q : TriadicCube d} {p : FiniteLpExponent} {x y : CubeVectorW1pFunction Q p} (coord : x.coord = y.coord) : x = y

def HCPolySupport.CubeVectorW1pFunction.toField {d : ℕ} {Q : TriadicCube d} {p : FiniteLpExponent} (F : CubeVectorW1pFunction Q p) : Vec d → Vec d

The pointwise vector field represented by the coordinate witnesses.

Equations

• F.toField x i = (F.coord i).toFun x

@[instance_reducible]

instance HCPolySupport.CubeVectorW1pFunction.instCoeFunForallVec {d : ℕ} {Q : TriadicCube d} {p : FiniteLpExponent} : CoeFun (CubeVectorW1pFunction Q p) fun (x : CubeVectorW1pFunction Q p) => Vec d → Vec d

Equations

• HCPolySupport.CubeVectorW1pFunction.instCoeFunForallVec = { coe := HCPolySupport.CubeVectorW1pFunction.toField }

def HCPolySupport.CubeVectorW1pFunction.jacobian {d : ℕ} {Q : TriadicCube d} {p : FiniteLpExponent} (F : CubeVectorW1pFunction Q p) : Vec d → Mat d

The pointwise Jacobian formed from the stored weak-gradient representatives.

Equations

• F.jacobian x i j = (F.coord i).grad x j

@[simp]

theorem HCPolySupport.CubeVectorW1pFunction.toField_apply {d : ℕ} {Q : TriadicCube d} {p : FiniteLpExponent} (F : CubeVectorW1pFunction Q p) (x : Vec d) (i : Fin d) : F.toField x i = (F.coord i).toFun x

@[simp]

theorem HCPolySupport.CubeVectorW1pFunction.coe_apply {d : ℕ} {Q : TriadicCube d} {p : FiniteLpExponent} (F : CubeVectorW1pFunction Q p) (x : Vec d) (i : Fin d) : F.toField x i = (F.coord i).toFun x

@[simp]

theorem HCPolySupport.CubeVectorW1pFunction.jacobian_apply {d : ℕ} {Q : TriadicCube d} {p : FiniteLpExponent} (F : CubeVectorW1pFunction Q p) (x : Vec d) (i j : Fin d) : F.jacobian x i j = (F.coord i).grad x j

@[simp]

theorem HCPolySupport.CubeVectorW1pFunction.jacobian_row {d : ℕ} {Q : TriadicCube d} {p : FiniteLpExponent} (F : CubeVectorW1pFunction Q p) (x : Vec d) (i : Fin d) : F.jacobian x i = (F.coord i).grad x

theorem HCPolySupport.CubeVectorW1pFunction.euclideanMemLp {d : ℕ} {Q : TriadicCube d} {p : FiniteLpExponent} (F : CubeVectorW1pFunction Q p) : MeasureTheory.MemLp (fun (x : Vec d) => HilbertVec.ofVec (F.toField x)) p.exponent (normalizedCubeMeasure Q)

The Hilbert realization of the represented vector field belongs to normalized L^p on the cube.

theorem HCPolySupport.CubeVectorW1pFunction.jacobianRowMemLp {d : ℕ} {Q : TriadicCube d} {p : FiniteLpExponent} (F : CubeVectorW1pFunction Q p) (i : Fin d) : MeasureTheory.MemLp (fun (x : Vec d) => HilbertVec.ofVec (F.jacobian x i)) p.exponent (normalizedCubeMeasure Q)

The Hilbert realization of one Jacobian row belongs to normalized L^p on the cube.

theorem HCPolySupport.CubeVectorW1pFunction.jacobianRowEuclideanMemLp {d : ℕ} {Q : TriadicCube d} {p : FiniteLpExponent} (F : CubeVectorW1pFunction Q p) (i : Fin d) : MeasureTheory.MemLp (fun (x : Vec d) => euclideanNorm (F.jacobian x i)) p.exponent (normalizedCubeMeasure Q)

The Euclidean magnitude of one Jacobian row belongs to normalized L^p. This is the norm-valued form of jacobianRowMemLp.

theorem HCPolySupport.CubeVectorW1pFunction.jacobianHilbertMemLp {d : ℕ} {Q : TriadicCube d} {p : FiniteLpExponent} (F : CubeVectorW1pFunction Q p) : MeasureTheory.MemLp (fun (x : Vec d) => HilbertMat.ofMat (F.jacobian x)) p.exponent (normalizedCubeMeasure Q)

The Hilbert-matrix realization of the Jacobian belongs to normalized L^p on the cube.

theorem HCPolySupport.CubeVectorW1pFunction.eLpNorm_jacobianHilbert_le_sum_grad {d : ℕ} {Q : TriadicCube d} {p : FiniteLpExponent} (F : CubeVectorW1pFunction Q p) : MeasureTheory.eLpNorm (fun (x : Vec d) => HilbertMat.ofMat (F.jacobian x)) p.exponent (normalizedCubeMeasure Q) ≤ ∑ i : Fin d, MeasureTheory.eLpNorm (fun (x : Vec d) => HilbertVec.ofVec ((F.coord i).grad x)) p.exponent (normalizedCubeMeasure Q)

The normalized L^p norm of the Jacobian is bounded by the finite sum of the normalized L^p norms of its coordinate gradients.

noncomputable def HCPolySupport.CubeVectorW1pFunction.toCubeEuclideanLpField {d : ℕ} {Q : TriadicCube d} {p : FiniteLpExponent} (F : CubeVectorW1pFunction Q p) : CubeEuclideanLpField Q p

Forget the weak-derivative witnesses and retain the represented normalized Euclidean L^p vector field.

Equations

• F.toCubeEuclideanLpField = { toField := F.toField, euclideanMemLp := ⋯ }

@[simp]

theorem HCPolySupport.CubeVectorW1pFunction.toCubeEuclideanLpField_toField {d : ℕ} {Q : TriadicCube d} {p : FiniteLpExponent} (F : CubeVectorW1pFunction Q p) : F.toCubeEuclideanLpField.toField = F.toField

theorem HCPolySupport.CubeVectorW1pFunction.weakHessianRowGradMemLpOn {d : ℕ} {Q : TriadicCube d} {p : FiniteLpExponent} {u : H1Function (openCubeSet Q)} (H : HasWeakHessianOn (openCubeSet Q) u) (hrows : ∀ (i : Fin d), MeasureTheory.MemLp (fun (x : Vec d) => HilbertVec.ofVec fun (j : Fin d) => H.hess i j x) p.exponent (normalizedCubeMeasure Q)) (i : Fin d) : GradMemLpOn (openCubeSet Q) p.exponent (H.gradCoordH1Function i).grad

noncomputable def HCPolySupport.CubeVectorW1pFunction.ofWeakHessian {d : ℕ} {Q : TriadicCube d} {p : FiniteLpExponent} [NeZero d] {u : H1Function (openCubeSet Q)} (H : HasWeakHessianOn (openCubeSet Q) u) (hrows : ∀ (i : Fin d), MeasureTheory.MemLp (fun (x : Vec d) => HilbertVec.ofVec fun (j : Fin d) => H.hess i j x) p.exponent (normalizedCubeMeasure Q)) : CubeVectorW1pFunction Q p

Build a cube-vector W^{1,p} function from a weak Hessian whose rows have normalized L^p membership. The represented vector field is exactly the stored weak gradient, and the represented Jacobian is exactly the stored weak Hessian. No separate L^p hypothesis on the gradient values is needed.

Equations

• HCPolySupport.CubeVectorW1pFunction.ofWeakHessian H hrows = { coord := fun (i : Fin d) => HCPolySupport.H1Function.toW1pOfGradMemLp ⋯ (H.gradCoordH1Function i) p ⋯ }

@[simp]

theorem HCPolySupport.CubeVectorW1pFunction.ofWeakHessian_coord_toFun {d : ℕ} {Q : TriadicCube d} {p : FiniteLpExponent} [NeZero d] {u : H1Function (openCubeSet Q)} (H : HasWeakHessianOn (openCubeSet Q) u) (hrows : ∀ (i : Fin d), MeasureTheory.MemLp (fun (x : Vec d) => HilbertVec.ofVec fun (j : Fin d) => H.hess i j x) p.exponent (normalizedCubeMeasure Q)) (i : Fin d) : ((ofWeakHessian H hrows).coord i).toFun = fun (x : Vec d) => u.grad x i

@[simp]

theorem HCPolySupport.CubeVectorW1pFunction.ofWeakHessian_coord_grad {d : ℕ} {Q : TriadicCube d} {p : FiniteLpExponent} [NeZero d] {u : H1Function (openCubeSet Q)} (H : HasWeakHessianOn (openCubeSet Q) u) (hrows : ∀ (i : Fin d), MeasureTheory.MemLp (fun (x : Vec d) => HilbertVec.ofVec fun (j : Fin d) => H.hess i j x) p.exponent (normalizedCubeMeasure Q)) (i : Fin d) : ((ofWeakHessian H hrows).coord i).grad = fun (x : Vec d) (j : Fin d) => H.hess i j x

@[simp]

theorem HCPolySupport.CubeVectorW1pFunction.ofWeakHessian_toField {d : ℕ} {Q : TriadicCube d} {p : FiniteLpExponent} [NeZero d] {u : H1Function (openCubeSet Q)} (H : HasWeakHessianOn (openCubeSet Q) u) (hrows : ∀ (i : Fin d), MeasureTheory.MemLp (fun (x : Vec d) => HilbertVec.ofVec fun (j : Fin d) => H.hess i j x) p.exponent (normalizedCubeMeasure Q)) : (ofWeakHessian H hrows).toField = u.grad

@[simp]

theorem HCPolySupport.CubeVectorW1pFunction.ofWeakHessian_jacobian {d : ℕ} {Q : TriadicCube d} {p : FiniteLpExponent} [NeZero d] {u : H1Function (openCubeSet Q)} (H : HasWeakHessianOn (openCubeSet Q) u) (hrows : ∀ (i : Fin d), MeasureTheory.MemLp (fun (x : Vec d) => HilbertVec.ofVec fun (j : Fin d) => H.hess i j x) p.exponent (normalizedCubeMeasure Q)) : (ofWeakHessian H hrows).jacobian = fun (x : Vec d) (i j : Fin d) => H.hess i j x

theorem HCPolySupport.CubeVectorW1pFunction.ofWeakHessian_jacobianHilbertMemLp {d : ℕ} {Q : TriadicCube d} {p : FiniteLpExponent} [NeZero d] {u : H1Function (openCubeSet Q)} (H : HasWeakHessianOn (openCubeSet Q) u) (hrows : ∀ (i : Fin d), MeasureTheory.MemLp (fun (x : Vec d) => HilbertVec.ofVec fun (j : Fin d) => H.hess i j x) p.exponent (normalizedCubeMeasure Q)) : MeasureTheory.MemLp (fun (x : Vec d) => HilbertMat.ofMat ((ofWeakHessian H hrows).jacobian x)) p.exponent (normalizedCubeMeasure Q)

For the weak-Hessian constructor, the generic Jacobian membership theorem reduces to the existing finite-p weak-Hessian aggregation theorem without changing representatives.

theorem HCPolySupport.CubeVectorW1pFunction.ofWeakHessian_eLpNorm_jacobianHilbert_le_sum_rows {d : ℕ} {Q : TriadicCube d} {p : FiniteLpExponent} [NeZero d] {u : H1Function (openCubeSet Q)} (H : HasWeakHessianOn (openCubeSet Q) u) (hrows : ∀ (i : Fin d), MeasureTheory.MemLp (fun (x : Vec d) => HilbertVec.ofVec fun (j : Fin d) => H.hess i j x) p.exponent (normalizedCubeMeasure Q)) : MeasureTheory.eLpNorm (fun (x : Vec d) => HilbertMat.ofMat ((ofWeakHessian H hrows).jacobian x)) p.exponent (normalizedCubeMeasure Q) ≤ ∑ i : Fin d, MeasureTheory.eLpNorm (fun (x : Vec d) => HilbertVec.ofVec fun (j : Fin d) => H.hess i j x) p.exponent (normalizedCubeMeasure Q)

For the weak-Hessian constructor, the generic Jacobian row-sum bound is exactly the existing finite-p weak-Hessian estimate.