Documentation

LeanPool.Superdiffusion.Algsuperdiff.Section3.Cutoff.CubeControlCover

CubeControlCover #

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

Local controls on translated unit cubes #

The finite-cover tail argument uses these exact translated unit-cube controls.

source
noncomputable def Algsuperdiff.Section3.Cutoff.translatedUnitCubeControl {d : ℕ} (z : HCPolySupport.Vec d) (j : Frozen.Assumptions.ShellField d) :
ℝ

The exact value control on the open unit cube translated by z.

Equations
Instances For
    source
    theorem Algsuperdiff.Section3.Cutoff.translatedUnitCubeControl_nonneg {d : ℕ} (z : HCPolySupport.Vec d) (j : Frozen.Assumptions.ShellField d) :
    0 ≤ translatedUnitCubeControl z j
    source
    theorem Algsuperdiff.Section3.Cutoff.measurable_translatedUnitCubeControl {d : ℕ} (z : HCPolySupport.Vec d) :
    Measurable (translatedUnitCubeControl z)
    source
    theorem Algsuperdiff.Section3.Cutoff.matrixOperatorNorm_le_translatedUnitCubeControl {d : ℕ} (z : HCPolySupport.Vec d) (j : Frozen.Assumptions.ShellField d) {x : HCPolySupport.Vec d} (hx : x ∈ HCPolySupport.translateSet z (HCPolySupport.openCubeSet (HCPolySupport.originCube d 0))) :
    HCPolySupport.Book.Ch02.matrixOperatorNorm ((↑j).1 x) ≤ translatedUnitCubeControl z j

    The translated unit control bounds the matrix operator norm on its literal open translated cube.