Coarse-graining support: Support.Sobolev.CubeEmbedding.FaceReflectionMain

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

Single-face even reflection: weak-gradient transport (main theorem)

The even reflection faceReflect v a i of a globally C¹, compactly supported function v on Vec (n+1) has weak gradient the piecewise faceGrad v a i on all of Vec (n+1) (hence, by restriction, on any open set).

theorem HCPolySupport.hasCompactSupport_insertNth_line {n : ℕ} {φ : Vec (n + 1) → ℝ} (hφc : HasCompactSupport φ) (j : Fin (n + 1)) (z : Vec n) : HasCompactSupport fun (t : ℝ) => φ (j.insertNth t z)

The restriction of a compactly supported function to an insertion line is compactly supported.

theorem HCPolySupport.hasWeakPartialDerivOn_univ_faceReflect {n : ℕ} {v : Vec (n + 1) → ℝ} (hv : ContDiff ℝ 1 v) (hvc : HasCompactSupport v) (a : ℝ) (i j : Fin (n + 1)) : HasWeakPartialDerivOn Set.univ j (faceReflect v a i) fun (x : Vec (n + 1)) => faceGrad v a i x j

Single-face weak-gradient transport. For v : Vec (n+1) → ℝ globally C¹ with compact support, the even reflection faceReflect v a i across {x_i = a} has weak j-th partial derivative faceGrad v a i · j on all of Vec (n+1), for every j.