LocalControlBridge

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

From pointwise unit descendants to local cube controls

This module upgrades the finite-cover pointwise bound to the exact sSup control used by the lower-tail summability argument.

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

The exact sSup local control on a nonnegative-scale origin cube is bounded by the finite maximum of translated unit-cube controls.

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

On a nonpositive-scale centered cube, the local control is bounded by the unit-cube control.