Coarse-graining support: Support.Sobolev.Foundations.CubeReflection.CubePairings #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
theorem
HCPolySupport.setIntegral_cubeUpperFaceNeighbor_reflectedField_pairing
{d : ℕ}
{G : Vec d → Vec d}
{φ : Vec d → ℝ}
(hφ : ContDiff ℝ (↑⊤) φ)
(Q : TriadicCube d)
(i : Fin d)
:
∫ (x : Vec d) in openCubeSet (cubeUpperFaceNeighbor Q i), vecDot ((coordReflectionLinear i) (G (cubeUpperFaceReflection Q i x))) (euclideanGradient φ x) = ∫ (y : Vec d) in openCubeSet Q, vecDot (G y) (euclideanGradient (fun (z : Vec d) => φ (cubeUpperFaceReflection Q i z)) y)
theorem
HCPolySupport.integrable_cubeUpperFaceNeighbor_reflectedField_pairing
{d : ℕ}
{G : Vec d → Vec d}
{φ : Vec d → ℝ}
(hφ : ContDiff ℝ (↑⊤) φ)
(Q : TriadicCube d)
(i : Fin d)
(hreflected :
MeasureTheory.Integrable
(fun (y : Vec d) => vecDot (G y) (euclideanGradient (fun (z : Vec d) => φ (cubeUpperFaceReflection Q i z)) y))
(MeasureTheory.volume.restrict (openCubeSet Q)))
:
MeasureTheory.Integrable
(fun (x : Vec d) => vecDot ((coordReflectionLinear i) (G (cubeUpperFaceReflection Q i x))) (euclideanGradient φ x))
(MeasureTheory.volume.restrict (openCubeSet (cubeUpperFaceNeighbor Q i)))
Integrability of the reflected weak-gradient pairing on the upper face
neighbor, transported from the corresponding reflected test pairing on Q.
theorem
HCPolySupport.setIntegral_cubeLowerFaceNeighbor_reflectedField_pairing
{d : ℕ}
{G : Vec d → Vec d}
{φ : Vec d → ℝ}
(hφ : ContDiff ℝ (↑⊤) φ)
(Q : TriadicCube d)
(i : Fin d)
:
∫ (x : Vec d) in openCubeSet (cubeLowerFaceNeighbor Q i), vecDot ((coordReflectionLinear i) (G (cubeLowerFaceReflection Q i x))) (euclideanGradient φ x) = ∫ (y : Vec d) in openCubeSet Q, vecDot (G y) (euclideanGradient (fun (z : Vec d) => φ (cubeLowerFaceReflection Q i z)) y)
theorem
HCPolySupport.integrable_cubeLowerFaceNeighbor_reflectedField_pairing
{d : ℕ}
{G : Vec d → Vec d}
{φ : Vec d → ℝ}
(hφ : ContDiff ℝ (↑⊤) φ)
(Q : TriadicCube d)
(i : Fin d)
(hreflected :
MeasureTheory.Integrable
(fun (y : Vec d) => vecDot (G y) (euclideanGradient (fun (z : Vec d) => φ (cubeLowerFaceReflection Q i z)) y))
(MeasureTheory.volume.restrict (openCubeSet Q)))
:
MeasureTheory.Integrable
(fun (x : Vec d) => vecDot ((coordReflectionLinear i) (G (cubeLowerFaceReflection Q i x))) (euclideanGradient φ x))
(MeasureTheory.volume.restrict (openCubeSet (cubeLowerFaceNeighbor Q i)))
Integrability of the reflected weak-gradient pairing on the lower face
neighbor, transported from the corresponding reflected test pairing on Q.
theorem
HCPolySupport.setIntegral_foldedCubeUpperFaceTest_reflectedField_pairing
{d : ℕ}
{G : Vec d → Vec d}
{φ : Vec d → ℝ}
(hφ : ContDiff ℝ (↑⊤) φ)
(Q : TriadicCube d)
(i : Fin d)
(hmain :
MeasureTheory.Integrable (fun (y : Vec d) => vecDot (G y) (euclideanGradient φ y))
(MeasureTheory.volume.restrict (openCubeSet Q)))
(hreflected :
MeasureTheory.Integrable
(fun (y : Vec d) => vecDot (G y) (euclideanGradient (fun (z : Vec d) => φ (cubeUpperFaceReflection Q i z)) y))
(MeasureTheory.volume.restrict (openCubeSet Q)))
:
∫ (y : Vec d) in openCubeSet Q, vecDot (G y) (euclideanGradient (foldedCubeUpperFaceTest Q i φ) y) = (∫ (y : Vec d) in openCubeSet Q, vecDot (G y) (euclideanGradient φ y)) + ∫ (x : Vec d) in openCubeSet (cubeUpperFaceNeighbor Q i), vecDot ((coordReflectionLinear i) (G (cubeUpperFaceReflection Q i x))) (euclideanGradient φ x)
theorem
HCPolySupport.setIntegral_foldedCubeLowerFaceTest_reflectedField_pairing
{d : ℕ}
{G : Vec d → Vec d}
{φ : Vec d → ℝ}
(hφ : ContDiff ℝ (↑⊤) φ)
(Q : TriadicCube d)
(i : Fin d)
(hmain :
MeasureTheory.Integrable (fun (y : Vec d) => vecDot (G y) (euclideanGradient φ y))
(MeasureTheory.volume.restrict (openCubeSet Q)))
(hreflected :
MeasureTheory.Integrable
(fun (y : Vec d) => vecDot (G y) (euclideanGradient (fun (z : Vec d) => φ (cubeLowerFaceReflection Q i z)) y))
(MeasureTheory.volume.restrict (openCubeSet Q)))
:
∫ (y : Vec d) in openCubeSet Q, vecDot (G y) (euclideanGradient (foldedCubeLowerFaceTest Q i φ) y) = (∫ (y : Vec d) in openCubeSet Q, vecDot (G y) (euclideanGradient φ y)) + ∫ (x : Vec d) in openCubeSet (cubeLowerFaceNeighbor Q i), vecDot ((coordReflectionLinear i) (G (cubeLowerFaceReflection Q i x))) (euclideanGradient φ x)
theorem
HCPolySupport.setIntegral_cubeUpperFaceNeighbor_reflectedGradient_pairing
{d : ℕ}
{u φ : Vec d → ℝ}
(hu : ContDiff ℝ (↑⊤) u)
(hφ : ContDiff ℝ (↑⊤) φ)
(Q : TriadicCube d)
(i : Fin d)
:
∫ (x : Vec d) in openCubeSet (cubeUpperFaceNeighbor Q i), vecDot (euclideanGradient (fun (y : Vec d) => u (cubeUpperFaceReflection Q i y)) x) (euclideanGradient φ x) = ∫ (y : Vec d) in openCubeSet Q, vecDot (euclideanGradient u y) (euclideanGradient (fun (z : Vec d) => φ (cubeUpperFaceReflection Q i z)) y)
theorem
HCPolySupport.setIntegral_cubeLowerFaceNeighbor_reflectedGradient_pairing
{d : ℕ}
{u φ : Vec d → ℝ}
(hu : ContDiff ℝ (↑⊤) u)
(hφ : ContDiff ℝ (↑⊤) φ)
(Q : TriadicCube d)
(i : Fin d)
:
∫ (x : Vec d) in openCubeSet (cubeLowerFaceNeighbor Q i), vecDot (euclideanGradient (fun (y : Vec d) => u (cubeLowerFaceReflection Q i y)) x) (euclideanGradient φ x) = ∫ (y : Vec d) in openCubeSet Q, vecDot (euclideanGradient u y) (euclideanGradient (fun (z : Vec d) => φ (cubeLowerFaceReflection Q i z)) y)
theorem
HCPolySupport.euclideanCoordSecondDeriv_comp_cubeUpperFaceReflection
{d : ℕ}
{u : Vec d → ℝ}
(hu : ContDiff ℝ (↑⊤) u)
(Q : TriadicCube d)
(i k l : Fin d)
(x : Vec d)
:
euclideanCoordSecondDeriv k l (fun (y : Vec d) => u (cubeUpperFaceReflection Q i y)) x = ((if k = i then -1 else 1) * if l = i then -1 else 1) * euclideanCoordSecondDeriv k l u (cubeUpperFaceReflection Q i x)
theorem
HCPolySupport.euclideanCoordSecondDeriv_comp_cubeLowerFaceReflection
{d : ℕ}
{u : Vec d → ℝ}
(hu : ContDiff ℝ (↑⊤) u)
(Q : TriadicCube d)
(i k l : Fin d)
(x : Vec d)
:
euclideanCoordSecondDeriv k l (fun (y : Vec d) => u (cubeLowerFaceReflection Q i y)) x = ((if k = i then -1 else 1) * if l = i then -1 else 1) * euclideanCoordSecondDeriv k l u (cubeLowerFaceReflection Q i x)
theorem
HCPolySupport.euclideanCoordLaplacian_comp_cubeUpperFaceReflection
{d : ℕ}
{u : Vec d → ℝ}
(hu : ContDiff ℝ (↑⊤) u)
(Q : TriadicCube d)
(i : Fin d)
(x : Vec d)
:
euclideanCoordLaplacian (fun (y : Vec d) => u (cubeUpperFaceReflection Q i y)) x = euclideanCoordLaplacian u (cubeUpperFaceReflection Q i x)
theorem
HCPolySupport.euclideanCoordLaplacian_comp_cubeLowerFaceReflection
{d : ℕ}
{u : Vec d → ℝ}
(hu : ContDiff ℝ (↑⊤) u)
(Q : TriadicCube d)
(i : Fin d)
(x : Vec d)
:
euclideanCoordLaplacian (fun (y : Vec d) => u (cubeLowerFaceReflection Q i y)) x = euclideanCoordLaplacian u (cubeLowerFaceReflection Q i x)
theorem
HCPolySupport.sum_sq_euclideanCoordSecondDeriv_comp_cubeUpperFaceReflection
{d : ℕ}
{u : Vec d → ℝ}
(hu : ContDiff ℝ (↑⊤) u)
(Q : TriadicCube d)
(i : Fin d)
(x : Vec d)
:
∑ k : Fin d, ∑ l : Fin d, euclideanCoordSecondDeriv k l (fun (y : Vec d) => u (cubeUpperFaceReflection Q i y)) x ^ 2 = ∑ k : Fin d, ∑ l : Fin d, euclideanCoordSecondDeriv k l u (cubeUpperFaceReflection Q i x) ^ 2
theorem
HCPolySupport.sum_sq_euclideanCoordSecondDeriv_comp_cubeLowerFaceReflection
{d : ℕ}
{u : Vec d → ℝ}
(hu : ContDiff ℝ (↑⊤) u)
(Q : TriadicCube d)
(i : Fin d)
(x : Vec d)
:
∑ k : Fin d, ∑ l : Fin d, euclideanCoordSecondDeriv k l (fun (y : Vec d) => u (cubeLowerFaceReflection Q i y)) x ^ 2 = ∑ k : Fin d, ∑ l : Fin d, euclideanCoordSecondDeriv k l u (cubeLowerFaceReflection Q i x) ^ 2