UnitCubeValue #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
L^∞ bookkeeping for the frozen unit-cube perturbation #
The frozen W^{1,∞} norm
h.w1Infinity = max ‖∇h‖_{L^∞(□₀)} ‖h‖_{L^∞(□₀)}
dominates the entries of h itself, exactly as gradientW1Infinity dominates
the entries of ∇h. Provider.DhBound.Lipschitz.UnitCube records the
derivative half; this module records the value half and transports the frozen
L^∞ memberships from the open-cube carrier to the normalized cube measure that
the Besov machinery integrates against.
Transporting L^∞ data to the normalized cube measure #
The frozen open-cube carrier is the open cube of the origin triadic cube.
Any a.e. property on the frozen open-cube carrier holds a.e. for the normalized cube measure.
The value half of the frozen W^{1,∞} norm #
Every entry of the frozen matrix field is bounded a.e. by w1Infinity.