NestedCubeCutoff

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

Smooth cutoffs between nested concentric cubes

theorem HCPolySupport.scaledClosedCubeSet_subset_scaledOpenCubeSet_of_lt {d : ℕ} (Q : TriadicCube d) {rho sigma : ℝ} (hrhoSigma : rho < sigma) : scaledClosedCubeSet Q rho ⊆ scaledOpenCubeSet Q sigma

A closed concentric cube of smaller relative radius lies in the open concentric cube of any strictly larger relative radius.

theorem HCPolySupport.QuantitativeCubeCutoff.canonicalFun_tsupport_subset_scaledOpenCubeSet {d : ℕ} (Q : TriadicCube d) {rhoInner rhoTransition rhoOuter : ℝ} (hrhoInner : 0 < rhoInner) (hinnerTransition : rhoInner < rhoTransition) (htransitionOuter : rhoTransition < rhoOuter) : tsupport (canonicalFun Q rhoInner rhoTransition) ⊆ scaledOpenCubeSet Q rhoOuter

The canonical cutoff's topological support lies in every strictly larger open concentric cube.

theorem HCPolySupport.QuantitativeCubeCutoff.vecNormSq_canonicalFun_gradient_le {d : ℕ} (Q : TriadicCube d) {rhoInner rhoTransition : ℝ} (hrhoInner : 0 < rhoInner) (hinnerTransition : rhoInner < rhoTransition) (x : Vec d) : (vecNormSq fun (i : Fin d) => (fderiv ℝ (canonicalFun Q rhoInner rhoTransition) x) (basisVec i)) ≤ ↑d * (↑d * smoothTransitionProfile.derivBound * (2 / ((rhoTransition - rhoInner) * cubeRadius Q))) ^ 2

The squared coordinate-gradient of the canonical cutoff is controlled by its explicit Fréchet-derivative bound.