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

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

Weak gradient of the fold extension

The extension x ↦ v (Fold lo hi x) of a globally C¹, compactly supported v has weak j-th partial derivative (∂ⱼv)(Fold x) · foldSignⱼ(x) on all of Vec (n+1). Along a j-line only the j-th fold varies (two kinks), so the d-dimensional statement reduces to the single-face reflection with two-kink integration by parts.

theorem HCPolySupport.hasWeakPartialDerivOn_univ_foldComp {n : ℕ} {v : Vec (n + 1) → ℝ} (hv : ContDiff ℝ 1 v) (hvc : HasCompactSupport v) (lo hi : Vec (n + 1)) (hlohi : ∀ (k : Fin (n + 1)), lo k ≤ hi k) (j : Fin (n + 1)) : HasWeakPartialDerivOn Set.univ j (fun (x : Vec (n + 1)) => v (Fold lo hi x)) fun (x : Vec (n + 1)) => (fderiv ℝ v (Fold lo hi x)) (basisVec j) * foldSign (lo j) (hi j) (x j)

Weak-gradient transport for the fold extension. For v : Vec (n+1) → ℝ globally C¹ with compact support and a box [lo, hi], the extension x ↦ v (Fold lo hi x) has weak j-th partial derivative (∂ⱼv)(Fold x) · foldSignⱼ(x) on all of Vec (n+1), for every j.