CubeControlTransport

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

Elementary transports for the local cube control

This module records the direct unit-cube consequences of J2 used by the later finite-cover argument. It deliberately does not assert an off-cube tail.

theorem Algsuperdiff.Section3.Cutoff.unitCubeValueNorm_le_j2Observable {d : ℕ} (j : Frozen.Assumptions.ShellField d) : j.unitCubeValueNorm ≤ Frozen.Assumptions.ShellField.j2Observable d j

theorem Algsuperdiff.Section3.Cutoff.localCubeControl_zero_eq_unitCubeValueNorm {d : ℕ} (j : Frozen.Assumptions.ShellField d) : localCubeControl 0 j = j.unitCubeValueNorm

theorem Algsuperdiff.Section3.Cutoff.integrable_unitCubeValueNorm_zero {d : ℕ} (M : ABKModel d) : MeasureTheory.Integrable (fun (omega : ShellSeq d) => (omega 0).unitCubeValueNorm) ↑M.P

J2 supplies an integrable unit-cube value control for the zero shell.