UnitCube #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Lipschitz representatives at the frozen unit-cube W^{2,∞} carrier #
The carrier of Algsuperdiff.Frozen.Section24.UnitCubeSkewW2Infinity is the
open unit triadic cube cubeDomain (originCube d 0), which is a bounded open
convex domain, so the bridge of
Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Lipschitz.Assembly applies
directly. This module discharges its hypotheses from the frozen fields and
records the two consumer corollaries:
exists_lipschitz_ae_eq_unitCubeSkewW2Infinity_value: every entry of the matrix field has a globallyd * h.w1Infinity-Lipschitz representative;exists_lipschitz_ae_eq_unitCubeSkewW2Infinity_firstDeriv: every entry of the first-derivative field has a globallyd * h.gradientW1Infinity-Lipschitz representative.
Both are stated pointwise (an oscillation bound valid for every pair of points
and an a.e. identification with the frozen entry function), which is the form
the D_h-bound assembly and the Besov estimates consume.
The L^∞ finiteness that gives w1Infinity and gradientW1Infinity their
meaning is derived here from the entrywise L^∞ memberships stored in the
frozen structure, via MatrixNorms; it is never assumed.
L^∞ bookkeeping #
An a.e. uniform bound on an a.e. strongly measurable function makes the essential supremum finite.
A finite essential supremum is an a.e. pointwise bound.
Measurability of the frozen derivative norms #
The frozen first-derivative norm is Lipschitz for the operator norm.
The frozen second-derivative norm is Lipschitz for the operator norm.
A field of continuous linear maps on Vec d is in L^p as soon as its values
on the coordinate directions are.
Entrywise L^p membership of a derivative field gives L^p membership of
the field itself.
A derivative field with entrywise L^∞ entries has an a.e. strongly
measurable frozen derivative norm.
Second-derivative analogue of
aestronglyMeasurable_matrixDerivativeNorm_of_memLp.
Entrywise a.e. bounds through the frozen derivative norms #
Every coordinate entry of a derivative field is bounded a.e. by the
essential supremum of the frozen first-derivative norm, whose finiteness follows
from the entrywise L^∞ memberships.
Second-derivative analogue of
ae_abs_apply_le_toReal_eLpNorm_matrixDerivativeNorm.
The frozen unit-cube norms #
Entrywise a.e. derivative bounds at the frozen carrier #
The consumer corollaries #
Lipschitz representative of a frozen unit-cube matrix-field entry.
Lipschitz representative of a frozen unit-cube first-derivative entry.
Half-open cube form #
The frozen carrier lives on the open unit cube, while the Besov and cube
average machinery integrates over the half-open realization cubeSet. The two
restricted measures coincide, so the a.e. identifications transfer verbatim.
Half-open-cell form of
exists_lipschitz_ae_eq_unitCubeSkewW2Infinity_value.
Half-open-cell form of
exists_lipschitz_ae_eq_unitCubeSkewW2Infinity_firstDeriv.