ConclusionKtot #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The layer constant Ktot: pricing the Step-1 increment gauge over a Whitney layer #
Provider/Multiscale/ConclusionCompetitor.lean leaves ONE analytic datum of
the good leg of p.bfA.multiscalebound's conclusion open, and names it exactly: the
binder hgood of toReal_tsum_simplexPartition_cutoff_two_leg_le_payload asks
for a layer-uniform bound
g_good 𝔰 ≤ Ktot . 3^{γ (k + h_k)}
and that module's docstring records why it cannot supply it: every factor of
the Step-1 majorant M = stepOneLayerMajorant depends on □ only through
□.scale, which is constant on a layer the increment gauge ‖k_L − k_{□.scale}‖²_{W^{1,∞}(□)}, represented by (incrementUnitCube₂ □ □.scale L ω).w1Infinity ^ 2.
This module prices that gauge. It has three parts.
1. The missing deterministic bridge #
Before this module NOTHING in the repository bounded w1Infinity ABOVE: the
proved UnitCubeSkewW2Infinity A (toReal_eLpNorm_..._le_w1Infinity,
ae_abs_..._le_w1Infinity, w1Infinity_nonneg) only lets w1Infinity
DOMINATE things, and the proved cube-level bridge
gradientW1Infinity_incrementUnitCube₂_le controls gradientW1Infinity — the
max of the S derivative gauges — which is a different quantity.
w1Infinity(incrementUnitCube₂ □ n L ω)
≤ max { 3^{2j} ‖∇(k_L − k_n)‖_{W^{1,∞}(□)} , ‖k_L − k_n‖_{L^∞(□)} } .
w1Infinity_incrementUnitCube₂_le is exactly this, with the first entry the
proved incrementOscGauge₂ and the second the T per-cube uniform gauge
Stream.cubeSupBound of Provider/Stream/WaveTranslation.lean — the object
e.km.kn.Linfty prices at every triadic cube. The value half is where the new
transport machinery enters: cubeSupBound □ n L dominates the increment
pointwise on □ (matrixOperatorNorm_finiteShellIncrement_le_cubeSupBound),
and the rescaling y ↦ 3^{j} y + z_□ carries the open unit cube into the open
cube □ (mem_openCubeSet_of_mem_unitOpenCube).
2. The two halves, priced #
- The oscillation half is S on good cubes. On the complement of
B_osc(□)the provedincrementOscGauge_le_oscThreshold(whose geometric series(1/5)Σ_{n≥1}3^{-n/5} ≤ 1is settled inBadEvents/Definitions.lean) gives3^{2j}‖∇(k_L−k_j)‖_{W^{1,∞}(□)} ≤ δ_osc c⋆^{1/2} γ^{-1/2} 3^{γ j}, andrpow_mul_oscThreshold_sqrecords the design identity behind the whole step:
So the oscillation half contributes a constant to3^{−2γ j} . oscThreshold(j)² = δ_osc² c⋆ / γ , for EVERY scale j.Ktotwith noj- and no layer-dependence at all.oscThreshold_monomakes the layer-to-root comparisonoscThreshold(□.scale) ≤ oscThreshold(m)for a layer cube. - The value half is the wave gauge, and it is priced distributionally.
isBigOWith_gammaSigma_two_layerSup_cubeSupBound_cutoffLawprices the MAXIMUM over one Whitney layer atΓ₂:□.scaleis constant on the layer (scale_eq_of_mem_whitneyLayer), so the transported per-cube amplitude ofStream.isBigOWith_gammaSigma_cubeSupBound_cutoffLawis the SAME for every cube of the layer, and the proved finite-max estimateOrlicz.isBigOWith_gammaSigma_finset_sup'_of_nonemptypays exactly one(3 max{1, log #𝒲(□_m,k)})^{1/2}for the whole layer. Each cube's estimate is the O estimate at the translated sample; no same-sample identification is made anywhere.
3. The pricing itself #
stepOneLayerMajorant_le_ktotConst_mul is the deterministic layer arithmetic:
with □.scale = m − k − h_k,
3^{−2γ □.scale} = 3^{−2γ m} . 3^{2γ(k+h_k)} ,
3^{ γ(i − □.scale)} = 3^{γ(i−m)} . 3^{γ(k+h_k)} ≤ 3^{γ(i−m)} . 3^{2γ(k+h_k)} ,
so the whole majorant is at most ktotConst . 3^{2γ(k+h_k)} as soon as the
gauge and the descendant weight are bounded uniformly over the layers.
Ktot := ktotConst M m i Cw (max (oscThreshold M m) Swave) p q ,
γ := 2 M.gamma ,
at the framed loads (σ_i^{-1/2} p, σ_i^{1/2} q) at which Step 1 is stated.
What is not proved in this file #
Swaveis not produced in this file. The remaining datum of the two a.e. theorems is a single realSwavedominatingcubeSupBound □ □.scale L ωover ALL layers simultaneously.ConclusionKtotEnvelope.leanlater supplies the countable wave-envelope route; the declarations here retainSwaveas an antecedent.- The re-basing is not performed for the Step-2
b_Lbranch, which is a different display. Cwis carried, not computed in this file. The descendant weightmultiscaleDescendantWeight □ (simplexScale m h k) (1/4) = 3^{(1 + h_{k+1} − h_k)/2}is layer-dependent through the profile only; bounding it uniformly is an arithmetic property ofh(for the Whitney sequence, of⌈b(1−b)^{-1}k⌉), and it is left as the caller's datumCwrather than derived. The gap lemma in the needed direction is proved andConclusionDatasupplies the concrete choiceCw = 3; that downstream producer does not change this theorem's conditional interface.h_k ≤ h_{k+1} + 1.- No
3^{-3k/4}per-layer weight is produced or approached: blocks it independently, and the exponent produced here is the payload's own3^{γ(k+h_k)}growth, not a weight.
Main definitions #
Main results #
Algsuperdiff.Section3.Provider.Multiscale.w1Infinity_incrementUnitCube₂_leAlgsuperdiff.Section3.Provider.Multiscale.rpow_mul_oscThreshold_sqAlgsuperdiff.Section3.Provider.Multiscale.w1Infinity_incrementUnitCube₂_le_max_oscThreshold
isBigOWith_gammaSigma_two_layerSup_cubeSupBound_cutoffLaw
Algsuperdiff.Section3.Provider.Multiscale.stepOneLayerMajorant_le_ktotConst_mulAlgsuperdiff.Section3.Provider.Multiscale.ktotConst_nonneg
References #
- ABK26,
p.bfA.multiscalebound, Step 1 (majorant) and Step 3;e.Bosc.def/e.BoscL.def/e.Bosc.decomp;e.good.local.events;e.km.kn.Linfty;l.maximums.Gamma.s; the normalized Sobolev norms. Provider/Multiscale/ConclusionCompetitor.lean(the consumer),Provider/Stream/WaveTranslation.lean(the transported gauge),Provider/Orlicz/Maximum.lean(the finite maximum),Provider/BadEvents/IncrementOscillation.lean(the oscillation half).
The rescaling map on the unit cube #
The dilation y ↦ 3^j y carries the open unit cube into the open origin
cube of scale j.
The rescaling of cubeUnitCube proves in the cube. The map y ↦ 3^{j} y + z_Q of IncrementGaugeTwoIndex.cubeUnitCube carries the open unit cube into
the open cube Q, so a pointwise bound on Q is a pointwise bound for the
rescaled unit-cube object.
The bridge #
The missing upper bound on the Step-1 increment gauge. The frozen Section
2.4 quantity w1Infinity of the rescaled literal increment k_L - k_n on Q
is at most the maximum of the two halves of the manuscript's normalized
W^{1,∞} norm (reading):
w1Infinity(incrementUnitCube₂ Q n L ω)
≤ max { 3^{2j}‖∇(k_L−k_n)‖_{W^{1,∞}(Q)} , ‖k_L−k_n‖_{L^∞(Q)} } ,
the first entry the proved incrementOscGauge₂, the second the T per-cube
uniform gauge Stream.cubeSupBound of e.km.kn.Linfty. No hypothesis at all:
the comparison is a pointwise statement about one shell field.
The oscillation half on good cubes #
The e.Bosc.def threshold is exactly scale-invariant in the Step-1
combination. For every scale j,
3^{-2γj} . oscThreshold(j)² = δ_osc² c⋆ / γ. This is why the oscillation half
of the increment gauge contributes a constant to Ktot with no layer
dependence whatsoever.
The e.Bosc.def threshold is nondecreasing in the scale; a layer cube has
□.scale ≤ m, so its threshold is below the root threshold.
The increment gauge on a good cube. Off B_osc(Q) the oscillation half of
the bridge is the deterministic e.Bosc.def threshold (proved
incrementOscGauge_le_oscThreshold, whose geometric series is settled in
BadEvents/Definitions.lean), so only the wave half remains random.
The layer maximum #
The wave half, priced over a whole Whitney layer. □.scale is constant on
𝒲(□_m,k), so the transported per-cube amplitude of e.km.kn.Linfty is the
same for every cube of the layer and the proved finite maximum estimate
l.maximums.Gamma.s pays exactly one log-cardinality factor for the entire
layer. Every per-cube estimate is the O estimate at the translated sample; no
same-sample identification and no independence across cubes is used.
The layer constant #
Both Cw (a bound for the descendant weight along the layers) and Sup are
the caller's data.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The layer arithmetic. On 𝒲(□_m,k) one has □.scale = m − k − h_k,
hence 3^{-2γ□.scale} = 3^{-2γm}3^{2γ(k+h_k)} and
3^{γ(i−□.scale)} = 3^{γ(i−m)}3^{γ(k+h_k)} ≤ 3^{γ(i−m)}3^{2γ(k+h_k)}, so the
Step-1 majorant is at most ktotConst . 3^{2γ(k+h_k)} once the increment gauge
and the descendant weight are bounded.
The good-leg pricing, a.e. #
The layer constant is nonnegative, which is what the bad-cube branch of the good leg needs.