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

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

Single-face even reflection: weak-gradient transport

Assembles the per-line calculus (FaceReflectionLines), the kink integration by parts (OneDimIBP), and coordinate-peeling Fubini (PeelFubini) into the weak gradient of the even reflection faceReflect v a i.

theorem HCPolySupport.exists_norm_bound_of_continuous_hasCompactSupport {d : ℕ} {w : Vec d → ℝ} (hw : Continuous w) (hwc : HasCompactSupport w) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (x : Vec d), ‖w x‖ ≤ C

A continuous compactly supported function is bounded.

theorem HCPolySupport.coordFaceReflection_eq_self_of_face {d : ℕ} {a : ℝ} {i : Fin d} {x : Vec d} (hx : x i = a) : coordFaceReflection a i x = x

On the face {x_i = a} the reflection is the identity.

theorem HCPolySupport.continuous_faceReflect {d : ℕ} {v : Vec d → ℝ} (hv : Continuous v) (a : ℝ) (i : Fin d) : Continuous (faceReflect v a i)

The even reflection of a continuous function is continuous (the two branches agree on the face).

theorem HCPolySupport.hasCompactSupport_faceReflect {d : ℕ} {v : Vec d → ℝ} (hvc : HasCompactSupport v) (a : ℝ) (i : Fin d) : HasCompactSupport (faceReflect v a i)

The even reflection has compact support when v does.