ValueLipschitz #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The cube-local L² value budget and the gradient-Lipschitz value representative #
Source: ABK26, the Term A bookkeeping of the unconditional J estimate.
The unconditional aggregation of
Algsuperdiff.Frozen.Section24.responseJ_sensitivity_unconditional prices the
Term A error of every mesoscopic cube against ‖h‖²_{L²(□₀)}, not against the
root W^{1,∞} norm. Two ingredients are needed, and both live here.
The value budget.
valueBudget h Ris the normalizedL²-square of|h|on the triadic cubeR. Its depth-ndescendant average over the unit cube is exactly‖h‖²_{L²(□₀)}(descendantsAverage_valueBudget), by the cube-average tower identity of CoarseGraining, and it dominates the normalizedL¹average of|h|onRby Cauchy-Schwarz (cubeAverage_matrixNormField_le_sqrt_valueBudget).The gradient-Lipschitz representative of the value field. The frozen carrier stores a weak first derivative of the value field which is bounded by
‖∇h‖_{W^{1,∞}}(not only by‖h‖_{W^{1,∞}}), so theW^{1,∞}-to-Lipschitz bridge ofProvider.DhBound.Lipschitzproduces a globally Lipschitz representative of the value field with constantd ‖∇h‖_{W^{1,∞}}. This is what turns the Term A Besov seminorm into a scale-damped quantity on a deep cube.
The pointwise norm field matrixNormField, its measurability chain and the
characterization valueL2_sq_eq_integral are not here: they live in
Algsuperdiff.Section24.UnitCubeSkewW2Infinity.ValueL2, an ordinary A module
beside the frozen definition, so that UnitCubeSkewW2Infinity.valueL2 is
delta-unfolded exactly once in the whole development and every consumer routes
through the characterization.
Every declaration in this module is an internal helper for the Section 2.4 sensitivity providers.
The gradient-Lipschitz representative of the value field #
Lipschitz representative of a frozen value entry, with the gradient
constant. Identical to
Provider.DhBound.Lipschitz.exists_lipschitz_ae_eq_unitCubeSkewW2Infinity_value
except that the a.e. bound on the weak derivative is taken from
‖∇h‖_{W^{1,∞}} rather than from ‖h‖_{W^{1,∞}}.
The entrywise globally Lipschitz representative of the frozen matrix field, with the gradient Lipschitz constant.
Equations
Instances For
The Lipschitz representative of the Term A field, with the gradient constant.
Equations
Instances For
L^∞ bounds for the frozen matrix norm field #
matrixNormField, its measurability chain and its L² membership on the
carrier live in Algsuperdiff.Section24.UnitCubeSkewW2Infinity.ValueL2, beside
the frozen definition they characterize; only the provider-level L^∞ and
cube-transport bookkeeping is added here.
The cube-local L² value budget #
The cube-local L² value budget. The normalized mean square of |h|
on the triadic cube R.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Cauchy-Schwarz for the value budget.
The unit cube: the budget aggregates to the frozen L² value norm #
The value budget aggregates to the frozen L² value norm.