IncrementGaugeTwoIndex #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The two-index increment oscillation gauge, its measurability, and its bridge #
Algsuperdiff.Section3.Provider.BadEvents.incrementOscGauge measures the stream
increment whose base index is the cube scale, which is what e.Bosc.def (ABK26)
needs. The good event e.good.local.events (ABK26) gauges an increment k_L - k_n whose base n need not equal the cube scale. This module supplies that
two-index version, together with the measurability that the corresponding event
needs and the two-index unit-cube bridge into the frozen Section 2.4 sensitivity
gate (ABK26).
Everything is factored through a single-shell-field gauge cubeOscGauge Q h,
namely the manuscript's 3^{2j} ||grad h||_{W^{1,infinity}(z + square_j)} for
an arbitrary shell field h at the cube Q with j = Q.scale; the proved
one-index objects are literally the case h = k_L - k_{Q.scale}
(incrementOscGauge₂_self, incrementUnitCube₂_self, both rfl).
Main definitions #
cubeOscGauge:3^{2j} ||grad h||_{W^{1,infinity}(z + square_j)}.cubeUnitCube: the rescaled unit-cubeW^{2,infinity}package ofh.incrementOscGauge₂,incrementUnitCube₂: the two-index specializations.
Main results #
continuous_shellFieldSum,measurable_shellFieldSum,measurable_shellIncrement: the additive layer ofAlgsuperdiff.Section3.Provider.Stream.ShellSumis continuous, hence measurable, in the shell sequence.measurable_cubeOscGauge,measurable_incrementOscGauge₂: the measurability needed to realizee.good.local.eventsas a measurable event.incrementOscGauge₂_le_sum_shellOscGauge: theW^{1,infinity}triangle inequality at the two-index gauge.gradientW1Infinity_cubeUnitCube_le,gradientW1Infinity_incrementUnitCube₂_le: the two-index bridge.
References #
- ABK26 (volume-normalized Sobolev norms).
- ABK26,
e.Bosc.def,e.Bosc.decomp. - ABK26,
e.good.local.events.
Local instances #
Mathlib's default instance search reaches neither of these inside its heartbeat budget, so the file installs them locally. The first is the second-countability of the frozen compact-open carrier, which is what turns continuity in the shell sequence into measurability; the second is the second-derivative fibre's continuous addition, needed for finite sums.
Continuity and measurability of the additive layer #
Finite shell-field sums are continuous in the shell sequence.
Finite shell-field sums are measurable in the shell sequence.
The literal stream increment is measurable in the shell sequence.
The literal stream increment is measurable on the cutoff sample carrier.
The single-shell-field cube gauge #
The manuscript's 3^{2j} ||grad h||_{W^{1,infinity}(z + square_j)} for an
arbitrary shell field h, at the cube Q with j = Q.scale and base point z = cubeBasePoint Q. At p = infinity the volume-normalized Sobolev norm of
ABK26 is max { ||grad² h||_{L∞}, 3^{-j} ||grad h||_{L∞} }.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The single-shell-field gauge is subadditive along finite shell-field sums,
which is the W^{1,infinity} triangle inequality of e.Bosc.decomp.
The two-index increment gauge #
The manuscript's 3^{2j} ||grad (k_L - k_n)||_{W^{1,infinity}(z+square_j)}
with an increment base n that need not be the cube scale j = Q.scale. This
is the gauge of e.good.local.events (ABK26).
Equations
- One or more equations did not get rendered due to their size.
Instances For
Measurability of the two-index gauge, used by the local implementation of
e.good.local.events as a measurable event.
The W^{1,infinity} triangle inequality at the two-index gauge.
The two-index unit-cube bridge #
The shell field h on z + square_j, rescaled to the unit cube by
y |-> z + 3^j y, as a Section 2.4 unit-cube object.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The exact normalization: the unit-cube derivative gauges of the rescaled
field are the 3^{2j}- and 3^{j}-scaled cube gauges of the field.
The bridge at an arbitrary shell field.
The two-index rescaled literal increment.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The two-index rescaled increment has the manuscript's values
(k_L - k_n)(z + 3^j y).
The two-index bridge: the Section 2.4 sensitivity gate quantity of the
rescaled literal increment k_L - k_n is bounded by the two-index gauge
3^{2j} ||grad (k_L - k_n)||_{W^{1,infinity}(z + square_j)}.