Coarse-graining support: Support.Sobolev.Foundations.CubeReflection.Folding.BlockIntegrals #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
theorem
HCPolySupport.euclideanGradient_comp_cubeFaceReflectionCellFoldMap_eq_reflectedVectorField
{d : ℕ}
{u : Vec d → ℝ}
(hu : ContDiff ℝ (↑⊤) u)
(Q : TriadicCube d)
(choice : Fin d → Fin 3)
{x : Vec d}
(hx : x ∈ openCubeSet (cubeFaceReflectionCellCube Q choice))
:
euclideanGradient (fun (y : Vec d) => u (cubeFaceReflectionCellFoldMap Q choice y)) x = cubeCoordinateFoldReflectedVectorField Q (euclideanGradient u) x
On a reflection-block cell, the smooth cell-folded potential has gradient given by the all-coordinate reflected vector field.
theorem
HCPolySupport.setIntegral_cubeFaceReflectionCellCube_sum_sq_secondDeriv_comp_cellFoldMap
{d : ℕ}
{u : Vec d → ℝ}
(hu : ContDiff ℝ (↑⊤) u)
(Q : TriadicCube d)
(choice : Fin d → Fin 3)
:
∫ (x : Vec d) in openCubeSet (cubeFaceReflectionCellCube Q choice), ∑ k : Fin d,
∑ l : Fin d,
euclideanCoordSecondDeriv k l (fun (y : Vec d) => u (cubeFaceReflectionCellFoldMap Q choice y)) x ^ 2 = ∫ (y : Vec d) in openCubeSet Q, ∑ k : Fin d, ∑ l : Fin d, euclideanCoordSecondDeriv k l u y ^ 2
The Hessian-square energy of a smooth function precomposed with a reflection-cell fold is one copy of the original cube Hessian-square energy.
theorem
HCPolySupport.setIntegral_cubeFaceReflectionCellCube_laplacian_sq_comp_cellFoldMap
{d : ℕ}
{u : Vec d → ℝ}
(hu : ContDiff ℝ (↑⊤) u)
(Q : TriadicCube d)
(choice : Fin d → Fin 3)
:
∫ (x : Vec d) in openCubeSet (cubeFaceReflectionCellCube Q choice), euclideanCoordLaplacian (fun (y : Vec d) => u (cubeFaceReflectionCellFoldMap Q choice y)) x ^ 2 = ∫ (y : Vec d) in openCubeSet Q, euclideanCoordLaplacian u y ^ 2
The Laplacian-square energy of a smooth function precomposed with a reflection-cell fold is one copy of the original cube Laplacian-square energy.
theorem
HCPolySupport.setIntegral_cubeFaceReflectionCellCube_cubeCoordinateFoldReflectedScalar_sq
{d : ℕ}
{F : Vec d → ℝ}
(Q : TriadicCube d)
(choice : Fin d → Fin 3)
:
∫ (x : Vec d) in openCubeSet (cubeFaceReflectionCellCube Q choice), cubeCoordinateFoldReflectedScalar Q F x * cubeCoordinateFoldReflectedScalar Q F x = ∫ (y : Vec d) in openCubeSet Q, F y * F y
The scalar square energy on any reflection-block cell is one copy of the original cube energy.
theorem
HCPolySupport.foldedCellVector_selfPairing_eq_parent
{d : ℕ}
{G : Vec d → Vec d}
(Q : TriadicCube d)
(choice : Fin d → Fin 3)
:
∫ (x : Vec d) in openCubeSet (cubeFaceReflectionCellCube Q choice), vecDot (cubeCoordinateFoldReflectedVectorField Q G x) (cubeCoordinateFoldReflectedVectorField Q G x) = ∫ (y : Vec d) in openCubeSet Q, vecDot (G y) (G y)
The vector self-pairing energy on any reflection-block cell is one copy of the original cube energy.
theorem
HCPolySupport.setIntegral_cubeFaceReflectionBlockSet_cubeCoordinateFoldReflectedScalar_sq
{d : ℕ}
{F : Vec d → ℝ}
(Q : TriadicCube d)
(hF : MeasureTheory.Integrable (fun (y : Vec d) => F y * F y) (MeasureTheory.volume.restrict (openCubeSet Q)))
:
∫ (x : Vec d) in cubeFaceReflectionBlockSet Q, cubeCoordinateFoldReflectedScalar Q F x * cubeCoordinateFoldReflectedScalar Q F x = ↑(Fintype.card (Fin d → Fin 3)) * ∫ (y : Vec d) in openCubeSet Q, F y * F y
The scalar square energy on the full all-coordinate reflection block is the sum of one identical copy over each reflection cell.
theorem
HCPolySupport.setIntegral_cubeFaceReflectionBlockSet_cubeCoordinateFoldReflectedVectorField_self_pairing
{d : ℕ}
{G : Vec d → Vec d}
(Q : TriadicCube d)
(hG : MeasureTheory.Integrable (fun (y : Vec d) => vecDot (G y) (G y)) (MeasureTheory.volume.restrict (openCubeSet Q)))
:
∫ (x : Vec d) in cubeFaceReflectionBlockSet Q, vecDot (cubeCoordinateFoldReflectedVectorField Q G x) (cubeCoordinateFoldReflectedVectorField Q G x) = ↑(Fintype.card (Fin d → Fin 3)) * ∫ (y : Vec d) in openCubeSet Q, vecDot (G y) (G y)
The vector self-pairing energy on the full all-coordinate reflection block is the sum of one identical copy over each reflection cell.
theorem
HCPolySupport.setIntegral_openCubeSet_union_upperFaceNeighbor
{d : ℕ}
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
(Q : TriadicCube d)
(i : Fin d)
(f : Vec d → E)
(hQ : MeasureTheory.Integrable f (MeasureTheory.volume.restrict (openCubeSet Q)))
(hN : MeasureTheory.Integrable f (MeasureTheory.volume.restrict (openCubeSet (cubeUpperFaceNeighbor Q i))))
:
∫ (x : Vec d) in openCubeSet Q ∪ openCubeSet (cubeUpperFaceNeighbor Q i), f x = (∫ (x : Vec d) in openCubeSet Q, f x) + ∫ (x : Vec d) in openCubeSet (cubeUpperFaceNeighbor Q i), f x
Set-integral split over the union of an open cube and its upper face neighbor.
theorem
HCPolySupport.setIntegral_openCubeSet_union_lowerFaceNeighbor
{d : ℕ}
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
(Q : TriadicCube d)
(i : Fin d)
(f : Vec d → E)
(hQ : MeasureTheory.Integrable f (MeasureTheory.volume.restrict (openCubeSet Q)))
(hN : MeasureTheory.Integrable f (MeasureTheory.volume.restrict (openCubeSet (cubeLowerFaceNeighbor Q i))))
:
∫ (x : Vec d) in openCubeSet Q ∪ openCubeSet (cubeLowerFaceNeighbor Q i), f x = (∫ (x : Vec d) in openCubeSet Q, f x) + ∫ (x : Vec d) in openCubeSet (cubeLowerFaceNeighbor Q i), f x
Set-integral split over the union of an open cube and its lower face neighbor.
theorem
HCPolySupport.setIntegral_cubeFaceNeighborSlabSet
{d : ℕ}
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
(Q : TriadicCube d)
(i : Fin d)
(f : Vec d → E)
(hL : MeasureTheory.Integrable f (MeasureTheory.volume.restrict (openCubeSet (cubeLowerFaceNeighbor Q i))))
(hQ : MeasureTheory.Integrable f (MeasureTheory.volume.restrict (openCubeSet Q)))
(hU : MeasureTheory.Integrable f (MeasureTheory.volume.restrict (openCubeSet (cubeUpperFaceNeighbor Q i))))
:
∫ (x : Vec d) in cubeFaceNeighborSlabSet Q i, f x = ((∫ (x : Vec d) in openCubeSet (cubeLowerFaceNeighbor Q i), f x) + ∫ (x : Vec d) in openCubeSet Q, f x) + ∫ (x : Vec d) in openCubeSet (cubeUpperFaceNeighbor Q i), f x
Set-integral split over the lower/original/upper one-coordinate face-neighbor slab.