Majorant

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

Deterministic lower-tail majorants

The probabilistic lower-tail argument uses a polynomially weighted geometric majorant. This module is deterministic: it contains neither a law nor an almost-everywhere assertion.

noncomputable def Algsuperdiff.Section3.Cutoff.cubeMajorant (gamma : ℝ) (m ell : ℤ) (r : ℕ) : ℝ

The scale profile used to dominate the local control of the shell indexed by m - r on the cube at scale ell.

Equations

• Algsuperdiff.Section3.Cutoff.cubeMajorant gamma m ell r = √(1 + max (↑ell - (↑m - ↑r)) 0) * Real.rpow 3 (gamma * (↑m - ↑r))

theorem Algsuperdiff.Section3.Cutoff.cubeMajorant_nonneg (gamma : ℝ) (m ell : ℤ) (r : ℕ) : 0 ≤ cubeMajorant gamma m ell r

theorem Algsuperdiff.Section3.Cutoff.summable_cubeMajorant {gamma : ℝ} (hgamma : 0 < gamma) (m ell : ℤ) : Summable (cubeMajorant gamma m ell)

Positive scaling exponents make the lower-half majorant summable.

theorem Algsuperdiff.Section3.Cutoff.cubeSet_originCube_subset_iUnion_unitDescendants (d : ℕ) (q : ℤ) (hq : 0 ≤ q) : HCPolySupport.cubeSet (HCPolySupport.originCube d q) ⊆ ⋃ R ∈ ↑(HCPolySupport.descendantsAtScale (HCPolySupport.originCube d q) 0), HCPolySupport.cubeSet R

The finite lattice of unit triadic descendants covers a nonnegative-scale origin cube. The half-open realization gives an exact cover, including the internal partition boundaries.

theorem Algsuperdiff.Section3.Cutoff.card_unitDescendants_originCube (d : ℕ) (q : ℤ) (hq : 0 ≤ q) : (HCPolySupport.descendantsAtScale (HCPolySupport.originCube d q) 0).card = (3 ^ d) ^ q.toNat

The unit-descendant lattice has the expected finite cardinality.