Coarse-graining support: Support.Sobolev.Foundations.CubeReflection.Derivatives

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

theorem HCPolySupport.coordReflectionLinear_basisVec {d : ℕ} (i k : Fin d) : (coordReflectionLinear i) (basisVec k) = (if k = i then -1 else 1) • basisVec k

theorem HCPolySupport.fderiv_coordFaceReflection {d : ℕ} (a : ℝ) (i : Fin d) (x : Vec d) : fderiv ℝ (coordFaceReflection a i) x = coordReflectionLinear i

theorem HCPolySupport.differentiableAt_coordFaceReflection {d : ℕ} (a : ℝ) (i : Fin d) (x : Vec d) : DifferentiableAt ℝ (coordFaceReflection a i) x

theorem HCPolySupport.euclideanCoordDeriv_comp_coordFaceReflection {d : ℕ} {u : Vec d → ℝ} (hu : ContDiff ℝ (↑⊤) u) (a : ℝ) (i k : Fin d) (x : Vec d) : euclideanCoordDeriv k (fun (y : Vec d) => u (coordFaceReflection a i y)) x = (if k = i then -1 else 1) * euclideanCoordDeriv k u (coordFaceReflection a i x)

First coordinate-derivative chain rule for scalar functions composed with a coordinate face reflection. The normal derivative changes sign; tangential derivatives do not.

theorem HCPolySupport.euclideanGradient_comp_coordFaceReflection {d : ℕ} {u : Vec d → ℝ} (hu : ContDiff ℝ (↑⊤) u) (a : ℝ) (i : Fin d) (x : Vec d) : euclideanGradient (fun (y : Vec d) => u (coordFaceReflection a i y)) x = (coordReflectionLinear i) (euclideanGradient u (coordFaceReflection a i x))

def HCPolySupport.foldedCoordFaceTest {d : ℕ} (a : ℝ) (i : Fin d) (φ : Vec d → ℝ) : Vec d → ℝ

Fold a scalar test through a coordinate face: on the original side this is φ + φ ∘ r, where r is the face reflection.

Equations

• HCPolySupport.foldedCoordFaceTest a i φ x = φ x + φ (HCPolySupport.coordFaceReflection a i x)

noncomputable def HCPolySupport.foldedCubeUpperFaceTest {d : ℕ} (Q : TriadicCube d) (i : Fin d) (φ : Vec d → ℝ) : Vec d → ℝ

The sum of a test function and its reflection through the upper ith face of the cube.

Equations

• HCPolySupport.foldedCubeUpperFaceTest Q i φ = HCPolySupport.foldedCoordFaceTest (HCPolySupport.cubeUpperFaceCoord Q i) i φ

noncomputable def HCPolySupport.foldedCubeLowerFaceTest {d : ℕ} (Q : TriadicCube d) (i : Fin d) (φ : Vec d → ℝ) : Vec d → ℝ

The sum of a test function and its reflection through the lower ith face of the cube.

Equations

• HCPolySupport.foldedCubeLowerFaceTest Q i φ = HCPolySupport.foldedCoordFaceTest (HCPolySupport.cubeLowerFaceCoord Q i) i φ

theorem HCPolySupport.contDiff_foldedCoordFaceTest {d : ℕ} {φ : Vec d → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (a : ℝ) (i : Fin d) : ContDiff ℝ (↑⊤) (foldedCoordFaceTest a i φ)

theorem HCPolySupport.contDiff_foldedCubeUpperFaceTest {d : ℕ} {φ : Vec d → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (Q : TriadicCube d) (i : Fin d) : ContDiff ℝ (↑⊤) (foldedCubeUpperFaceTest Q i φ)

theorem HCPolySupport.contDiff_foldedCubeLowerFaceTest {d : ℕ} {φ : Vec d → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (Q : TriadicCube d) (i : Fin d) : ContDiff ℝ (↑⊤) (foldedCubeLowerFaceTest Q i φ)

theorem HCPolySupport.hasCompactSupport_comp_coordFaceReflection {d : ℕ} {φ : Vec d → ℝ} (hφ : HasCompactSupport φ) (a : ℝ) (i : Fin d) : HasCompactSupport fun (x : Vec d) => φ (coordFaceReflection a i x)

theorem HCPolySupport.hasCompactSupport_comp_cubeUpperFaceReflection {d : ℕ} {φ : Vec d → ℝ} (hφ : HasCompactSupport φ) (Q : TriadicCube d) (i : Fin d) : HasCompactSupport fun (x : Vec d) => φ (cubeUpperFaceReflection Q i x)

theorem HCPolySupport.hasCompactSupport_comp_cubeLowerFaceReflection {d : ℕ} {φ : Vec d → ℝ} (hφ : HasCompactSupport φ) (Q : TriadicCube d) (i : Fin d) : HasCompactSupport fun (x : Vec d) => φ (cubeLowerFaceReflection Q i x)

theorem HCPolySupport.hasCompactSupport_foldedCoordFaceTest {d : ℕ} {φ : Vec d → ℝ} (hφ : HasCompactSupport φ) (a : ℝ) (i : Fin d) : HasCompactSupport (foldedCoordFaceTest a i φ)

theorem HCPolySupport.hasCompactSupport_foldedCubeUpperFaceTest {d : ℕ} {φ : Vec d → ℝ} (hφ : HasCompactSupport φ) (Q : TriadicCube d) (i : Fin d) : HasCompactSupport (foldedCubeUpperFaceTest Q i φ)

theorem HCPolySupport.hasCompactSupport_foldedCubeLowerFaceTest {d : ℕ} {φ : Vec d → ℝ} (hφ : HasCompactSupport φ) (Q : TriadicCube d) (i : Fin d) : HasCompactSupport (foldedCubeLowerFaceTest Q i φ)

theorem HCPolySupport.euclideanGradient_foldedCoordFaceTest {d : ℕ} {φ : Vec d → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (a : ℝ) (i : Fin d) (x : Vec d) : euclideanGradient (foldedCoordFaceTest a i φ) x = euclideanGradient φ x + (coordReflectionLinear i) (euclideanGradient φ (coordFaceReflection a i x))

theorem HCPolySupport.euclideanGradient_foldedCubeUpperFaceTest {d : ℕ} {φ : Vec d → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (Q : TriadicCube d) (i : Fin d) (x : Vec d) : euclideanGradient (foldedCubeUpperFaceTest Q i φ) x = euclideanGradient φ x + (coordReflectionLinear i) (euclideanGradient φ (cubeUpperFaceReflection Q i x))

theorem HCPolySupport.euclideanGradient_foldedCubeLowerFaceTest {d : ℕ} {φ : Vec d → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (Q : TriadicCube d) (i : Fin d) (x : Vec d) : euclideanGradient (foldedCubeLowerFaceTest Q i φ) x = euclideanGradient φ x + (coordReflectionLinear i) (euclideanGradient φ (cubeLowerFaceReflection Q i x))

theorem HCPolySupport.vecDot_euclideanGradient_foldedCoordFaceTest {d : ℕ} {u φ : Vec d → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (a : ℝ) (i : Fin d) (x : Vec d) : vecDot (euclideanGradient u x) (euclideanGradient (foldedCoordFaceTest a i φ) x) = vecDot (euclideanGradient u x) (euclideanGradient φ x) + vecDot (euclideanGradient u x) ((coordReflectionLinear i) (euclideanGradient φ (coordFaceReflection a i x)))

theorem HCPolySupport.vecDot_euclideanGradient_foldedCubeUpperFaceTest {d : ℕ} {u φ : Vec d → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (Q : TriadicCube d) (i : Fin d) (x : Vec d) : vecDot (euclideanGradient u x) (euclideanGradient (foldedCubeUpperFaceTest Q i φ) x) = vecDot (euclideanGradient u x) (euclideanGradient φ x) + vecDot (euclideanGradient u x) ((coordReflectionLinear i) (euclideanGradient φ (cubeUpperFaceReflection Q i x)))

theorem HCPolySupport.vecDot_euclideanGradient_foldedCubeLowerFaceTest {d : ℕ} {u φ : Vec d → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (Q : TriadicCube d) (i : Fin d) (x : Vec d) : vecDot (euclideanGradient u x) (euclideanGradient (foldedCubeLowerFaceTest Q i φ) x) = vecDot (euclideanGradient u x) (euclideanGradient φ x) + vecDot (euclideanGradient u x) ((coordReflectionLinear i) (euclideanGradient φ (cubeLowerFaceReflection Q i x)))

noncomputable def HCPolySupport.foldedCubeUpperFaceH1Test {d : ℕ} (Q : TriadicCube d) (i : Fin d) {φ : Vec d → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) : H1Function (openCubeSet Q)

The folded upper-face smooth test, packaged as an H¹(openCubeSet Q) witness for variational Neumann equations.

Equations

• HCPolySupport.foldedCubeUpperFaceH1Test Q i hφ = HCPolySupport.H1Function.ofContDiffOnIsOpenBoundedConvexDomain ⋯ ⋯

noncomputable def HCPolySupport.foldedCubeLowerFaceH1Test {d : ℕ} (Q : TriadicCube d) (i : Fin d) {φ : Vec d → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) : H1Function (openCubeSet Q)

The folded lower-face smooth test, packaged as an H¹(openCubeSet Q) witness for variational Neumann equations.

Equations

• HCPolySupport.foldedCubeLowerFaceH1Test Q i hφ = HCPolySupport.H1Function.ofContDiffOnIsOpenBoundedConvexDomain ⋯ ⋯

@[simp]

theorem HCPolySupport.foldedCubeUpperFaceH1Test_toFun {d : ℕ} (Q : TriadicCube d) (i : Fin d) {φ : Vec d → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) : (foldedCubeUpperFaceH1Test Q i hφ).toFun = foldedCubeUpperFaceTest Q i φ

@[simp]

theorem HCPolySupport.foldedCubeLowerFaceH1Test_toFun {d : ℕ} (Q : TriadicCube d) (i : Fin d) {φ : Vec d → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) : (foldedCubeLowerFaceH1Test Q i hφ).toFun = foldedCubeLowerFaceTest Q i φ

@[simp]

theorem HCPolySupport.foldedCubeUpperFaceH1Test_grad {d : ℕ} (Q : TriadicCube d) (i : Fin d) {φ : Vec d → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (x : Vec d) : (foldedCubeUpperFaceH1Test Q i hφ).grad x = euclideanGradient (foldedCubeUpperFaceTest Q i φ) x

@[simp]

theorem HCPolySupport.foldedCubeLowerFaceH1Test_grad {d : ℕ} (Q : TriadicCube d) (i : Fin d) {φ : Vec d → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (x : Vec d) : (foldedCubeLowerFaceH1Test Q i hφ).grad x = euclideanGradient (foldedCubeLowerFaceTest Q i φ) x

theorem HCPolySupport.vecDot_euclideanGradient_comp_coordFaceReflection_pairing {d : ℕ} {u φ : Vec d → ℝ} (hu : ContDiff ℝ (↑⊤) u) (hφ : ContDiff ℝ (↑⊤) φ) (a : ℝ) (i : Fin d) (x : Vec d) : vecDot (euclideanGradient (fun (y : Vec d) => u (coordFaceReflection a i y)) (coordFaceReflection a i x)) (euclideanGradient φ (coordFaceReflection a i x)) = vecDot (euclideanGradient u x) (euclideanGradient (fun (y : Vec d) => φ (coordFaceReflection a i y)) x)

theorem HCPolySupport.euclideanCoordSecondDeriv_comp_coordFaceReflection {d : ℕ} {u : Vec d → ℝ} (hu : ContDiff ℝ (↑⊤) u) (a : ℝ) (i k l : Fin d) (x : Vec d) : euclideanCoordSecondDeriv k l (fun (y : Vec d) => u (coordFaceReflection a i y)) x = ((if k = i then -1 else 1) * if l = i then -1 else 1) * euclideanCoordSecondDeriv k l u (coordFaceReflection a i x)

Second coordinate-derivative chain rule for scalar functions composed with a coordinate face reflection. Each differentiation in the reflected normal direction contributes one sign.

theorem HCPolySupport.euclideanCoordSecondDeriv_diag_comp_coordFaceReflection {d : ℕ} {u : Vec d → ℝ} (hu : ContDiff ℝ (↑⊤) u) (a : ℝ) (i k : Fin d) (x : Vec d) : euclideanCoordSecondDeriv k k (fun (y : Vec d) => u (coordFaceReflection a i y)) x = euclideanCoordSecondDeriv k k u (coordFaceReflection a i x)

theorem HCPolySupport.euclideanCoordLaplacian_comp_coordFaceReflection {d : ℕ} {u : Vec d → ℝ} (hu : ContDiff ℝ (↑⊤) u) (a : ℝ) (i : Fin d) (x : Vec d) : euclideanCoordLaplacian (fun (y : Vec d) => u (coordFaceReflection a i y)) x = euclideanCoordLaplacian u (coordFaceReflection a i x)

theorem HCPolySupport.sum_sq_euclideanCoordSecondDeriv_comp_coordFaceReflection {d : ℕ} {u : Vec d → ℝ} (hu : ContDiff ℝ (↑⊤) u) (a : ℝ) (i : Fin d) (x : Vec d) : ∑ k : Fin d, ∑ l : Fin d, euclideanCoordSecondDeriv k l (fun (y : Vec d) => u (coordFaceReflection a i y)) x ^ 2 = ∑ k : Fin d, ∑ l : Fin d, euclideanCoordSecondDeriv k l u (coordFaceReflection a i x) ^ 2

theorem HCPolySupport.euclideanCoordDeriv_comp_cubeUpperFaceReflection {d : ℕ} {u : Vec d → ℝ} (hu : ContDiff ℝ (↑⊤) u) (Q : TriadicCube d) (i k : Fin d) (x : Vec d) : euclideanCoordDeriv k (fun (y : Vec d) => u (cubeUpperFaceReflection Q i y)) x = (if k = i then -1 else 1) * euclideanCoordDeriv k u (cubeUpperFaceReflection Q i x)

theorem HCPolySupport.euclideanCoordDeriv_comp_cubeLowerFaceReflection {d : ℕ} {u : Vec d → ℝ} (hu : ContDiff ℝ (↑⊤) u) (Q : TriadicCube d) (i k : Fin d) (x : Vec d) : euclideanCoordDeriv k (fun (y : Vec d) => u (cubeLowerFaceReflection Q i y)) x = (if k = i then -1 else 1) * euclideanCoordDeriv k u (cubeLowerFaceReflection Q i x)

theorem HCPolySupport.euclideanGradient_comp_cubeUpperFaceReflection {d : ℕ} {u : Vec d → ℝ} (hu : ContDiff ℝ (↑⊤) u) (Q : TriadicCube d) (i : Fin d) (x : Vec d) : euclideanGradient (fun (y : Vec d) => u (cubeUpperFaceReflection Q i y)) x = (coordReflectionLinear i) (euclideanGradient u (cubeUpperFaceReflection Q i x))

theorem HCPolySupport.euclideanGradient_comp_cubeLowerFaceReflection {d : ℕ} {u : Vec d → ℝ} (hu : ContDiff ℝ (↑⊤) u) (Q : TriadicCube d) (i : Fin d) (x : Vec d) : euclideanGradient (fun (y : Vec d) => u (cubeLowerFaceReflection Q i y)) x = (coordReflectionLinear i) (euclideanGradient u (cubeLowerFaceReflection Q i x))

theorem HCPolySupport.vecDot_euclideanGradient_comp_cubeUpperFaceReflection_pairing {d : ℕ} {u φ : Vec d → ℝ} (hu : ContDiff ℝ (↑⊤) u) (hφ : ContDiff ℝ (↑⊤) φ) (Q : TriadicCube d) (i : Fin d) (x : Vec d) : vecDot (euclideanGradient (fun (y : Vec d) => u (cubeUpperFaceReflection Q i y)) (cubeUpperFaceReflection Q i x)) (euclideanGradient φ (cubeUpperFaceReflection Q i x)) = vecDot (euclideanGradient u x) (euclideanGradient (fun (y : Vec d) => φ (cubeUpperFaceReflection Q i y)) x)

theorem HCPolySupport.vecDot_euclideanGradient_comp_cubeLowerFaceReflection_pairing {d : ℕ} {u φ : Vec d → ℝ} (hu : ContDiff ℝ (↑⊤) u) (hφ : ContDiff ℝ (↑⊤) φ) (Q : TriadicCube d) (i : Fin d) (x : Vec d) : vecDot (euclideanGradient (fun (y : Vec d) => u (cubeLowerFaceReflection Q i y)) (cubeLowerFaceReflection Q i x)) (euclideanGradient φ (cubeLowerFaceReflection Q i x)) = vecDot (euclideanGradient u x) (euclideanGradient (fun (y : Vec d) => φ (cubeLowerFaceReflection Q i y)) x)