J2LInfSeal

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

Exact L-infinity interpretation of the J2 shell norms

This file identifies each pointwise open-cube supremum in the J2 observable with the corresponding L∞ seminorm for volume restricted to the literal manuscript cube cu₀ = (-1/2, 1/2)^d.

The reverse inequality from essential supremum to pointwise supremum uses continuity: a strict pointwise violation persists on a nonempty open neighborhood, and such a neighborhood has positive volume. The argument is uniform in d, including d = 0.

theorem Algsuperdiff.Frozen.Assumptions.ShellField.unitCubeValueNorm_eq_eLpNorm_top {d : ℕ} (j : ShellField d) : j.unitCubeValueNorm = (MeasureTheory.eLpNorm (fun (x : HCPolySupport.Vec d) => HCPolySupport.Book.Ch02.matrixOperatorNorm ((↑j).1 x)) ⊤ (MeasureTheory.volume.restrict (HCPolySupport.openCubeSet (HCPolySupport.originCube d 0)))).toReal

The pointwise value supremum in J2 is exactly its restricted-volume L∞ seminorm on the literal open unit cube.