Coarse-graining support: Support.Sobolev.Foundations.CubeBesovPoincare.W12NormalizedPartition

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

Normalized W^{1,2} data on triadic cubes

This small bridge keeps the source-facing open-cube Sobolev carrier while identifying its normalized volume with the cube normalization used by the disjoint Besov hierarchy.

def HCPolySupport.W1pFunction.restrictToOpenSubcube {d : ℕ} {Q R : TriadicCube d} {j : ℕ} {p : ENNReal} (u : W1pFunction (openCubeSet Q) p) (hR : R ∈ descendantsAtDepth Q j) : W1pFunction (openCubeSet R) p

Restrict a Sobolev witness on an open triadic cube to one of its open descendants. Both its function and stored weak-gradient representatives are unchanged.

Equations

• u.restrictToOpenSubcube hR = u.restrict ⋯ ⋯

@[simp]

theorem HCPolySupport.W1pFunction.restrictToOpenSubcube_toFun {d : ℕ} {Q R : TriadicCube d} {j : ℕ} {p : ENNReal} (u : W1pFunction (openCubeSet Q) p) (hR : R ∈ descendantsAtDepth Q j) : (u.restrictToOpenSubcube hR).toFun = u.toFun

@[simp]

theorem HCPolySupport.W1pFunction.restrictToOpenSubcube_grad {d : ℕ} {Q R : TriadicCube d} {j : ℕ} {p : ENNReal} (u : W1pFunction (openCubeSet Q) p) (hR : R ∈ descendantsAtDepth Q j) : (u.restrictToOpenSubcube hR).grad = u.grad

theorem HCPolySupport.openCubeSet_boundedMeasurableDomain_normalizedVolume_eq_normalizedCubeMeasure {d : ℕ} (Q : TriadicCube d) : (⋯.toBoundedMeasurableDomain ⋯).normalizedVolume = normalizedCubeMeasure Q

The normalized measure of the source-facing open cube is exactly the normalized cube measure. This is a measure equality, not a pointwise carrier identification.

theorem HCPolySupport.openCubeSet_normalizedW1pSeminorm_two_eq_cubeLpNorm_euclideanGrad {d : ℕ} (Q : TriadicCube d) (u : W1pFunction (openCubeSet Q) 2) : BoundedMeasurableDomain.NormalizedW1pKernel.seminorm (⋯.toBoundedMeasurableDomain ⋯) 2 openCubeSet_normalizedW1pSeminorm_two_eq_cubeLpNorm_euclideanGrad._proof_1 openCubeSet_normalizedW1pSeminorm_two_eq_cubeLpNorm_euclideanGrad._proof_2 u = cubeLpNorm Q 2 fun (x : Vec d) => euclideanNorm (u.grad x)

The exact source-facing normalized W^{1,2} seminorm on an open cube is the normalized cube L² norm of the explicit Euclidean gradient magnitude.

theorem HCPolySupport.descendantsAverage_cubeLpNorm_euclideanGrad_two_sq_eq {d : ℕ} (Q : TriadicCube d) (u : W1pFunction (openCubeSet Q) 2) (j : ℕ) : (descendantsAverage Q j fun (R : TriadicCube d) => (cubeLpNorm R 2 fun (x : Vec d) => euclideanNorm (u.grad x)) ^ 2) = (cubeLpNorm Q 2 fun (x : Vec d) => euclideanNorm (u.grad x)) ^ 2

Normalized L² energy partitions exactly over descendants. This is the measure-theoretic ingredient needed to aggregate the restricted open-cube Sobolev seminorms.

noncomputable def HCPolySupport.descendantOpenCubeSetNormalizedW1pSeminormTwo {d : ℕ} (Q : TriadicCube d) (u : W1pFunction (openCubeSet Q) 2) (j : ℕ) (R : TriadicCube d) : ℝ

The source-facing normalized Sobolev seminorm of a descendant. The zero value off the finite descendant family makes this a total function of a cube, as required by descendantsAverage; it is never used on that off-family branch.

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.descendantOpenCubeSetNormalizedW1pSeminormTwo_eq_of_mem {d : ℕ} (Q : TriadicCube d) (u : W1pFunction (openCubeSet Q) 2) (j : ℕ) {R : TriadicCube d} (hR : R ∈ descendantsAtDepth Q j) : descendantOpenCubeSetNormalizedW1pSeminormTwo Q u j R = BoundedMeasurableDomain.NormalizedW1pKernel.seminorm (⋯.toBoundedMeasurableDomain ⋯) 2 openCubeSet_normalizedW1pSeminorm_two_eq_cubeLpNorm_euclideanGrad._proof_1 openCubeSet_normalizedW1pSeminorm_two_eq_cubeLpNorm_euclideanGrad._proof_2 (u.restrictToOpenSubcube hR)

On an actual descendant, the totalized seminorm is the literal source-facing seminorm of the restricted Sobolev witness.

theorem HCPolySupport.descendantsAverage_openCubeSet_normalizedW1pSeminorm_two_sq_eq {d : ℕ} (Q : TriadicCube d) (u : W1pFunction (openCubeSet Q) 2) (j : ℕ) : (descendantsAverage Q j fun (R : TriadicCube d) => descendantOpenCubeSetNormalizedW1pSeminormTwo Q u j R ^ 2) = BoundedMeasurableDomain.NormalizedW1pKernel.seminorm (⋯.toBoundedMeasurableDomain ⋯) 2 openCubeSet_normalizedW1pSeminorm_two_eq_cubeLpNorm_euclideanGrad._proof_1 openCubeSet_normalizedW1pSeminorm_two_eq_cubeLpNorm_euclideanGrad._proof_2 u ^ 2

The exact source-facing normalized Sobolev energy partitions over the open descendants of a triadic cube.