Single-face even reflection: definitions and per-line calculus

Global (on all of ℝ^d) even reflection of a function across the face {x_i = a}, its candidate gradient (sign-flipped in direction i on the reflected side), the geometric fact that the reflection commutes with coordinate insertion, and the one-dimensional derivatives of the direct and reflected line functions. These feed the Fubini assembly in FaceReflection.

noncomputable def Homogenization.faceReflect {d : ℕ} (v : Vec d → ℝ) (a : ℝ) (i : Fin d) : Vec d → ℝ

Even reflection of v across the face {x_i = a}: unchanged where a ≤ x i, reflected otherwise.

Equations

• Homogenization.faceReflect v a i x = if a ≤ x i then v x else v (Homogenization.coordFaceReflection a i x)

noncomputable def Homogenization.faceGrad {d : ℕ} (v : Vec d → ℝ) (a : ℝ) (i : Fin d) : Vec d → Vec d

Candidate gradient of faceReflect v a i: the reflected-side gradient carries a sign flip in direction i (and no flip in the other directions).

Equations

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

theorem Homogenization.coordFaceReflection_insertNth {n : ℕ} (a : ℝ) (i : Fin (n + 1)) (t : ℝ) (z : Vec n) : coordFaceReflection a i (i.insertNth t z) = i.insertNth (2 * a - t) z

The face reflection commutes with coordinate insertion at the reflected axis: inserting t at i then reflecting is inserting 2a − t.

theorem Homogenization.hasDerivAt_insertNth {n : ℕ} (i : Fin (n + 1)) (z : Vec n) (t₀ : ℝ) : HasDerivAt (fun (t : ℝ) => i.insertNth t z) (basisVec i) t₀

The insertion line t ↦ i.insertNth t z is affine with velocity basisVec i.

theorem Homogenization.hasDerivAt_insertNth_reflect {n : ℕ} (a : ℝ) (i : Fin (n + 1)) (z : Vec n) (t₀ : ℝ) : HasDerivAt (fun (t : ℝ) => i.insertNth (2 * a - t) z) (-basisVec i) t₀

The reflected insertion line t ↦ i.insertNth (2a − t) z has velocity -basisVec i.

theorem Homogenization.hasDerivAt_comp_insertNth {n : ℕ} {v : Vec (n + 1) → ℝ} (hv : Differentiable ℝ v) (i : Fin (n + 1)) (z : Vec n) (t₀ : ℝ) : HasDerivAt (fun (t : ℝ) => v (i.insertNth t z)) ((fderiv ℝ v (i.insertNth t₀ z)) (basisVec i)) t₀

Directional derivative of v along the insertion line in direction i.

theorem Homogenization.hasDerivAt_comp_insertNth_reflect {n : ℕ} {v : Vec (n + 1) → ℝ} (hv : Differentiable ℝ v) (a : ℝ) (i : Fin (n + 1)) (z : Vec n) (t₀ : ℝ) : HasDerivAt (fun (t : ℝ) => v (i.insertNth (2 * a - t) z)) ((fderiv ℝ v (i.insertNth (2 * a - t₀) z)) (-basisVec i)) t₀

Directional derivative of v along the reflected insertion line.

theorem Homogenization.hasDerivAt_coordFaceReflection_insertNth {n : ℕ} (a : ℝ) {i j : Fin (n + 1)} (hji : j ≠ i) (z : Vec n) (t₀ : ℝ) : HasDerivAt (fun (t : ℝ) => coordFaceReflection a i (j.insertNth t z)) (basisVec j) t₀

Velocity of the reflected insertion line in a tangential coordinate j ≠ i: inserting t at j then reflecting across {x_i = a} moves with velocity basisVec j (the reflection fixes tangential directions).

theorem Homogenization.hasDerivAt_comp_coordFaceReflection_insertNth {n : ℕ} {v : Vec (n + 1) → ℝ} (hv : Differentiable ℝ v) (a : ℝ) {i j : Fin (n + 1)} (hji : j ≠ i) (z : Vec n) (t₀ : ℝ) : HasDerivAt (fun (t : ℝ) => v (coordFaceReflection a i (j.insertNth t z))) ((fderiv ℝ v (coordFaceReflection a i (j.insertNth t₀ z))) (basisVec j)) t₀

Directional derivative of v along the reflected insertion line in a tangential coordinate j ≠ i.