Coarse-graining support:

Support.Sobolev.Foundations.CubeNeumannW22CZ.WeakInteriorDQ.ReflectionParentSmoothApprox

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

Smooth approximation after parent-cube reflection

This file packages the clean part of the reflected-parent approximation step: smooth convex-domain approximants on the original cube converge after all-face reflection in the parent cube. It intentionally does not assert that the reflected smooth representatives are already parent-cube H¹ functions; that is the remaining trace/gluing bridge.

theorem HCPolySupport.tendsto_toScalarL2_openCubeSet_succ_originCube_reflectedScalar_convexApproxSmoothH1 {d : ℕ} {m : ℤ} (u : H1Function (openCubeSet (originCube d m))) {x0 : Vec d} {r : ℝ} (hball : Metric.closedBall x0 r ⊆ openCubeSet (originCube d m)) (hr : 0 < r) : Filter.Tendsto (fun (n : ℕ) => toScalarL2 ⋯) Filter.atTop (nhds (toScalarL2 ⋯))

Smooth convex approximants on the origin cube converge, after all-face scalar reflection, to the reflected scalar target in parent-cube L².

theorem HCPolySupport.tendsto_toScalarL2_openCubeSet_succ_originCube_reflectedGradient_convexApproxSmoothH1_coord {d : ℕ} {m : ℤ} (u : H1Function (openCubeSet (originCube d m))) {x0 : Vec d} {r : ℝ} (hball : Metric.closedBall x0 r ⊆ openCubeSet (originCube d m)) (hr : 0 < r) (j : Fin d) : Filter.Tendsto (fun (n : ℕ) => toScalarL2 ⋯) Filter.atTop (nhds (toScalarL2 ⋯))

Smooth convex approximant gradients on the origin cube converge coordinatewise, after all-face vector-field reflection, to the reflected gradient target in parent-cube L².