Documentation

LeanPool.Superdiffusion.Algsuperdiff.Section3.Cutoff.RangeNormalization

RangeNormalization #

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

Canonical normalization of the cutoff range #

The cutoff at scale m has literal range sqrt(d) * 3^m. We use the fixed open-thickening budget epsilon = 1/4 and normalize by the least triadic depth whose spatial factor leaves strict room for the two thickenings.

source
noncomputable def Algsuperdiff.Section3.Cutoff.cutoffBridgeEpsilon :
ℝ

Fixed open-thickening radius used in the local-integral to restriction bridge. Its exact value leaves the slack 1 - 2 epsilon = 1/2.

Equations
Instances For
    source
    theorem Algsuperdiff.Section3.Cutoff.cutoffBridgeEpsilon_pos :
    0 < cutoffBridgeEpsilon
    source
    @[simp]
    theorem Algsuperdiff.Section3.Cutoff.one_sub_two_mul_cutoffBridgeEpsilon :
    1 - 2 * cutoffBridgeEpsilon = 1 / 2
    source
    theorem Algsuperdiff.Section3.Cutoff.exists_cutoffNormalizationDepth (d : ℕ) (m : ℤ) :
    ∃ (k : ℕ), 2 * cutoffNaturalRange d m < 3 ^ k
    source
    noncomputable def Algsuperdiff.Section3.Cutoff.cutoffNormalizationDepth (d : ℕ) (m : ℤ) :
    ℕ

    Least triadic depth that leaves strict epsilon = 1/4 bridge slack for the literal cutoff range. This is a deterministic natural number, never a noncanonical choice witness.

    Equations
    Instances For
      source
      theorem Algsuperdiff.Section3.Cutoff.cutoffNormalizationDepth_spec (d : ℕ) (m : ℤ) :
      2 * cutoffNaturalRange d m < 3 ^ cutoffNormalizationDepth d m
      source
      theorem Algsuperdiff.Section3.Cutoff.cutoffNormalizationDepth_strict_slack (d : ℕ) (m : ℤ) :
      cutoffNaturalRange d m < 3 ^ cutoffNormalizationDepth d m * (1 - 2 * cutoffBridgeEpsilon)

      Exact strict slack discharged by the canonical depth.

      source
      theorem Algsuperdiff.Section3.Cutoff.cutoffNormalization_unitRangeDependentLaw {d : ℕ} (M : ABKModel d) (m : ℤ) :
      HCPolySupport.Book.Ch04.RestrictionUnitRangeDependentLaw (HCPolySupport.Book.Ch04.restrictionScaleNormalizedLaw (cutoffNormalizationDepth d m) (coefficientCutoffLaw M m))

      The canonical triadically normalized actual cutoff law has CoarseGraining's exact unit-range dependence predicate.