CubeControlAggregate

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

Finite aggregation of unit-cube controls

The half-open origin cube is partitioned by finitely many unit descendants. Their finite maximum, rather than their sum, gives the measurable control used by the Gaussian maximum estimate.

noncomputable def Algsuperdiff.Section3.Cutoff.originCubeUnitControlMax {d : ℕ} (q : ℤ) (hq : 0 ≤ q) (j : Frozen.Assumptions.ShellField d) : ℝ

The finite maximum of translated unit-cube controls over the exact unit-descendant lattice of a nonnegative-scale origin cube. The explicit nonemptiness witness is part of the definition, so this is the genuine finite maximum rather than an empty-set convention.

Equations

• One or more equations did not get rendered due to their size.

theorem Algsuperdiff.Section3.Cutoff.originCubeUnitControlMax_nonneg {d : ℕ} (q : ℤ) (hq : 0 ≤ q) (j : Frozen.Assumptions.ShellField d) : 0 ≤ originCubeUnitControlMax q hq j

theorem Algsuperdiff.Section3.Cutoff.matrixOperatorNorm_le_originCubeUnitControlMax {d : ℕ} (q : ℤ) (hq : 0 ≤ q) (j : Frozen.Assumptions.ShellField d) {x : HCPolySupport.Vec d} (hx : x ∈ HCPolySupport.cubeSet (HCPolySupport.originCube d q)) : HCPolySupport.Book.Ch02.matrixOperatorNorm ((↑j).1 x) ≤ originCubeUnitControlMax q hq j

The finite unit-descendant maximum controls the matrix operator norm at every point of the canonical half-open origin cube.

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

The number of variables in originCubeUnitControlMax is the expected number of unit descendants.