ExitMeanValueIdentificationCutoff

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

A smooth cutoff between two consecutive exhaustion cubes

The Caccioppoli estimate is applied on a pair of consecutive cubes of the exhaustion (-3^v, 3^v)^d ⊆ (-3^(v+1), 3^(v+1))^d, and needs a smooth compactly supported function equal to one on the inner cube and supported in the outer one, with a uniform bound on its gradient.

The quantitative cutoff of the upstream package is attached to the concentric subcubes of a triadic cube, so the only work here is the transport: the exhaustion cube of index v is the concentric subcube of relative radius 2 of the triadic cube of scale v centered at the origin, and the exhaustion cube of index v + 1 is the concentric subcube of relative radius 6 of that same triadic cube. The cutoff between relative radii 2 and 4 therefore does what is needed.

The triadic cube underlying an exhaustion cube

def DivergenceFormProcess.Form.exhaustionTriadicCube (d v : ℕ) : HCPolySupport.TriadicCube d

The triadic cube of scale v centered at the origin. Its concentric subcubes of relative radii 2 and 6 are the exhaustion cubes of indices v and v + 1.

Equations

• DivergenceFormProcess.Form.exhaustionTriadicCube d v = { scale := ↑v, index := fun (x : Fin d) => 0 }

The cutoff

theorem DivergenceFormProcess.Form.exists_wholeSpaceCubeCutoff (d v : ℕ) : ∃ (eta : HCPolySupport.Vec d → ℝ), ContDiff ℝ (↑⊤) eta ∧ HasCompactSupport eta ∧ tsupport eta ⊆ wholeSpaceCube d (v + 1) ∧ (∀ x ∈ wholeSpaceCube d v, eta x = 1) ∧ ∃ (K : ℝ), 0 ≤ K ∧ ∀ (x : HCPolySupport.Vec d), (HCPolySupport.vecNormSq fun (i : Fin d) => (fderiv ℝ eta x) (HCPolySupport.basisVec i)) ≤ K

A smooth cutoff between two consecutive exhaustion cubes. It equals one on the inner cube, is supported in the outer cube, and has a uniformly bounded coordinate gradient.