Derivatives

Support for the Armstrong–Vicol anomalous-diffusion formalization.

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

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

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

theorem Homogenization.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 Homogenization.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 Homogenization.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

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

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

Fold a test function across the upper face of a triadic cube.

Equations

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

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

Fold a test function across the lower face of a triadic cube.

Equations

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

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

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

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

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

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

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

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

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

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

theorem Homogenization.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 Homogenization.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 Homogenization.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 Homogenization.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 Homogenization.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 Homogenization.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 Homogenization.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

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

noncomputable def Homogenization.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

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

@[simp]

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

@[simp]

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

@[simp]

theorem Homogenization.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 Homogenization.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 Homogenization.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 Homogenization.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 Homogenization.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 Homogenization.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 Homogenization.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 Homogenization.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 Homogenization.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 Homogenization.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 Homogenization.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 Homogenization.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 Homogenization.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)