WaveSizesZeroth

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

Provider: the zeroth-order leg and the full W^{2,∞} carrier of e.wave.sizes

Companion of Provider/MultiscaleEstimate/WaveSizes.lean, which carries the derivative half of ABK26's wave-size display e.wave.sizes. This module adds the missing zeroth-order L∞ leg, forms the extended carrier, records the zeroth-order fidelity statement, and states the headline endpoint wave_sizes_bound at that extended carrier.

This is a provider endpoint only. It is not a source node, not a frozen declaration, and it does not close p.multiscale.estimate.

Why the zeroth order is required

The printed display carries ‖k_m - k_{l-h}‖_{W^{2,∞}(z+cu_l)}. At p = ∞ the printed object is a maximum, not a sum. Reading at p = ∞ on a cube of side 3^l (where |U|^{-1/d} = 3^{-l}) and iterating to second order gives

3^{2l} ‖f‖_{W^{2,∞}(z+cu_l)} = max{‖f‖_{L∞(z+cu_l)}, 3^l ‖∇f‖_{L∞(z+cu_l)}, 3^{2l} ‖∇²f‖_{L∞(z+cu_l)}},

the p → ∞ limit of the printed ℓ^p combination. This module works with the three-order sum

‖f‖_{L∞(z+cu_l)} + 3^l ‖∇f‖_{L∞(z+cu_l)} + 3^{2l} ‖∇²f‖_{L∞(z+cu_l)},

which dominates that maximum, all three legs being nonnegative (and is at most three times it, so the two are equivalent). Every bound proved here against the sum is therefore a bound on the printed maximum: the domination runs in the safe direction and nothing is over-claimed. An earlier version of this docstring wrote the two with an =; that equation was false as written and is withdrawn. "The three-order object" below always means the sum.

The zeroth-order term is load-bearing. The frozen sensitivity remainder of Frozen/Section24/ResponseJSensitivity.lean carries vecNormSq p * h.w1Infinity ^ 2 with w1Infinity = max{‖∇h‖_{L∞(□₀)}, ‖h‖_{L∞(□₀)}} (Frozen/Section24/UnitCubeSkewW2Infinity/W1Infinity.lean), i.e. it contains ‖h‖_{L∞}, at a strictly positive coefficient; it is consumed verbatim at Provider/BadEvents/GoodLocalEvents.lean. The printed e.J.sensitivity.apppp merges that remainder with the gradientW1Infinity remainder into the single 3^{4l}‖·‖²_{W^{2,∞}} object. Any wave carrier that drops the L∞ term therefore does not feed the consumer. See the full discussion in the sibling module's docstring.

The extended carrier

waveGaugeW2 m h R is the sum of the two legs at the triadic cube R of scale l = R.scale, read at the base point z = cubeCenter R:

waveGaugeW2 m h R = cubeSupBound R (l-h) m + waveGauge l m h (cubeCenter R).

• the derivative leg is the sibling module's waveGauge.

The Γ₂ input for the zeroth-order leg is Stream.isBigOWith_gammaSigma_cubeSupBound (Provider/Stream/WaveTranslation.lean), the Γ₂ form whose only binder is hnm : n < m -- it carries no m ≤ Q.scale binder, which is what makes it usable at n = l-h, Q.scale = l ≤ m. The squared companions in that module do carry m ≤ Q.scale and are unusable in the wave lane; they are not touched here. cubeSupBound R m m = 0 covers the single degenerate case h = 0, l = m.

cubeCenter R = triadicCubeShift R holds by definitional unfolding, so the two legs really live on the same set: the cube R is exactly cubeCenter R + cu_l (openCubeSet_eq_translateSet_originCube_of_triadicCube).

The endpoint arithmetic, and why it is exactly s^{-2}

At n = l-h, Q.scale = l = m-j the amplitude of isBigOWith_gammaSigma_cubeSupBound is

(3 max{1, log |subcubeShifts d (l-h) l|})^{1/2} · C_∞(d) · min{√(γ^{-1}), √(m-l+h)} · 3^{γm},

with |subcubeShifts d (l-h) l| = (2·3^{h+1}+1)^d, so the covering penalty is O(√(h+1)). After the 3^{-γl} normalization of waveSizeW2 the factor 3^{γm} leaves 3^{γj}, and after squaring and paying the grid maximum (waveGridConst d (1+j)) the per-scale base is

∝ (1+j) (j+h) 3^{2γj},

which is quadratic in the depth j. The exponent split three_rpow_split (legitimate because s ≥ 8γ) turns 3^{-sj} 3^{2γj} into 3^{-(3/4)sj}, and

s Σ_j (1+j)(j+h) 3^{-(3/4)sj} ≤ C h s^{-2},

the printed s^{-2} exactly. This is the reason the printed amplitude is s^{-2} and not the s^{-1} the derivative half alone would give: the zeroth-order leg, not the derivative leg, is what saturates the printed exponent. The summation lemma is tsum_weighted_sq_le below, proved from half_le_one_sub_three_rpow_neg and the elementary (1+j) x^j ≤ (1-x)^{-1} at the two auxiliary ratios 3^{-s/8} and 3^{-s/2}.

Main definitions

• waveCoverConst, waveSupAmp, waveAmpW2, waveLayerAmpW2, waveKW2, waveSizesConstW2: the constants, all explicit.
• waveGaugeW2: the extended (three-order) wave carrier.
• waveSizeW2, waveSizeMaxW2, waveSizesTotalW2: the per-cube quantity, its grid maximum, and the complete left-hand side of e.wave.sizes, all at the extended carrier.
• waveCutoff: the integer cutoff ⌈C |log ε|⌉.

Main results

• summable_weighted_sq, tsum_weighted_sq_le: the weighted scale sum at a quadratic base, at s^{-3} (hence s^{-2} after the outer s). Reusable development arithmetic.
• streamIncrementLinftyNorm_le_waveGaugeW2: the zeroth-order half of the fidelity statement. The extended carrier dominates ‖k_m-k_{l-h}‖_{L∞(z+cu_l)} in the genuine L∞-norm carrier Stream.streamIncrementLinftyNorm.
• isBigOWith_gammaSigma_waveSup: the Γ₂ estimate for the zeroth-order leg.
• isBigOWith_gammaSigma_waveGaugeW2, isBigOWith_gammaSigma_waveSizeW2: the per-cube Γ₂ estimate at the extended carrier.
• isBigOWith_gammaSigma_waveSizeMaxW2_sq: the per-scale Γ₁ estimate.
• isBigOWith_gammaSigma_waveSizesTotalW2: e.wave.sizes at the extended carrier and the printed s^{-2}.
• wave_sizes_bound: the headline, the printed form O_{Γ₁}(C s^{-2} ε^{-C}) at the extended carrier and at the integer cutoff h = ⌈C₀|log ε|⌉.

The fidelity convention, stated

This module is stated against the honest scale-l convention for the volume-normalized norm on a cube of side 3^l. At p = ∞ that norm is the maximum

3^{2l}‖f‖_{W^{2,∞}(Q)} = max{‖f‖_{L∞(Q)}, 3^l‖∇f‖_{L∞(Q)}, 3^{2l}‖∇²f‖_{L∞(Q)}},

which is the reading (‖·‖_{W^{1,p}} with the |U|^{-p/d} weight on the zeroth-order term, taken at p = ∞ and iterated to second order) used throughout the Section 3 stream chain. The carrier is built against the three-order sum

‖f‖_{L∞(Q)} + 3^l‖∇f‖_{L∞(Q)} + 3^{2l}‖∇²f‖_{L∞(Q)},

which dominates that maximum (all three legs are nonnegative), so every bound proved here against the sum implies the corresponding bound on the printed W^{2,∞} object and claims nothing beyond it. Writing the sum with an = -- as an earlier version of this section did -- was wrong, and is withdrawn: the relation is max ≤ sum ≤ 3 max, and only the first inequality is used. What is available, and used, is that the zeroth-order leg is stated in the genuine L∞-norm carrier Stream.streamIncrementLinftyNorm, which Provider/Stream/IncrementLinftyNorm.lean identifies with eLpNorm ∞ (volume.restrict (openCubeSet (originCube d l))) -- the same shape as the frozen norms, one rescaling away.

The grid/lattice identification, asserted not proved

Unchanged from the sibling module: the printed index set z ∈ 3^l Z^d ∩ cu_m is realized as descendantsAtScale (originCube d m) l with z:= cubeCenter R. This is the convention inherited from Localization.legScaleAverage (Provider/Localization/Breakdown.lean), asserted and not proved; the required set-equality pair is recorded verbatim in the sibling module's docstring. No declaration here depends on it being a bijection.

References

• ABK26, e.wave.sizes.
• ABK26, e.J.sensitivity.apppp (the consumer shape).
• ABK26, e.km.kn.Linfty (the zeroth-order input).
• ABK26, l.maximums.Gamma.s.
• ABK26, (the volume-normalized Sobolev norm convention).

Elementary real arithmetic: the quadratic base

All of this section is abstract-real: no model, no measure, no cube.

theorem Algsuperdiff.Section3.Provider.MultiscaleEstimate.summable_weighted_sq {s gamma K : ℝ} (hs : 0 < s) (hs1 : s ≤ 1) (hsg : 8 * gamma ≤ s) (hK : 0 ≤ K) : Summable fun (j : ℕ) => 3 ^ (-s * ↑j) * (3 ^ (2 * gamma * ↑j) * ((1 + ↑j) ^ 2 * K))

The quadratic-base weighted scale family is summable.

theorem Algsuperdiff.Section3.Provider.MultiscaleEstimate.tsum_weighted_sq_le {s gamma K : ℝ} (hs : 0 < s) (hs1 : s ≤ 1) (hsg : 8 * gamma ≤ s) (hK : 0 ≤ K) : ∑' (j : ℕ), 3 ^ (-s * ↑j) * (3 ^ (2 * gamma * ↑j) * ((1 + ↑j) ^ 2 * K)) ≤ 1024 * K / s ^ 3

The quadratic-base weighted scale sum, at s^{-3}.

The covering penalty of the zeroth-order leg

noncomputable def Algsuperdiff.Section3.Provider.MultiscaleEstimate.waveCoverConst (d : ℕ) : ℝ

The dimensional constant of the covering penalty of e.km.kn.Linfty at the wave lane's cutoff depth.

Duplication, disclosed. This constant and the lemma cover_log_le below re-derive a proved result of the same family, by the same route, from inside this module's own import closure: Provider/Stream/LargeCubeLinfty.lean bounds the same 3 max{1, log |subcubeShifts d n l|} in three_mul_max_one_log_card_subcubeShifts_le, at the constant largeCubeLogConst = 3(1 + 3 log 3) there, by the same three steps. The constants are different (3(1 + 2d log 3) here, with d inside; d sits outside there as a separate factor), and the reason for re-deriving rather than consuming is the h = 0 case -- see cover_log_le.

Equations

• Algsuperdiff.Section3.Provider.MultiscaleEstimate.waveCoverConst d = 3 * (1 + 2 * ↑d * Real.log 3)

theorem Algsuperdiff.Section3.Provider.MultiscaleEstimate.waveCoverConst_pos (d : ℕ) : 0 < waveCoverConst d

theorem Algsuperdiff.Section3.Provider.MultiscaleEstimate.waveCoverConst_nonneg (d : ℕ) : 0 ≤ waveCoverConst d

The zeroth-order leg

noncomputable def Algsuperdiff.Section3.Provider.MultiscaleEstimate.waveSupAmp {d : ℕ} (M : ABKModel d) (h j : ℕ) : ℝ

The Γ₂ amplitude of the zeroth-order leg at depth j = m - l and cutoff h, after the 3^{-γl} normalization: the covering penalty √(C(d)(1+h)), the e.km.kn.Linfty constant, the layer count √(j+h), and the residual 3^{γ j} left over from 3^{γ m} = 3^{γ j} 3^{γ l}.

Equations

• One or more equations did not get rendered due to their size.

theorem Algsuperdiff.Section3.Provider.MultiscaleEstimate.waveSupAmp_nonneg {d : ℕ} (M : ABKModel d) (h j : ℕ) : 0 ≤ waveSupAmp M h j

theorem Algsuperdiff.Section3.Provider.MultiscaleEstimate.isBigOWith_gammaSigma_waveSup {d : ℕ} (M : ABKModel d) (m : ℤ) (h j : ℕ) {R : HCPolySupport.TriadicCube d} (hR : R.scale = m - ↑j) : HCPolySupport.IndependentSums.IsBigOWith (↑M.P) (HCPolySupport.IndependentSums.gammaSigma 2) (fun (omega : Cutoff.ShellSeq d) => Stream.cubeSupBound R (R.scale - ↑h) m omega) (waveSupAmp M h j * 3 ^ (M.gamma * ↑R.scale))

The Γ₂ estimate of the zeroth-order leg. On the triadic cube R of scale l = m - j, the uniform supremum gauge of k_m - k_{l-h} obeys

cubeSupBound R (l-h) m ≤ O_{Γ₂}(waveSupAmp M h j · 3^{γ l}),

the amplitude being the e.km.kn.Linfty amplitude of Stream.isBigOWith_gammaSigma_cubeSupBound with the covering penalty made explicit. Unlike the derivative leg, this amplitude does grow with the scale gap j = m - l, through √(j+h) and 3^{γ j}; that growth is exactly what makes the l-sum land at the printed s^{-2}.

The extended carrier

noncomputable def Algsuperdiff.Section3.Provider.MultiscaleEstimate.waveGaugeW2 {d : ℕ} (m : ℤ) (h : ℕ) (R : HCPolySupport.TriadicCube d) (omega : Cutoff.ShellSeq d) : ℝ

The extended wave carrier. The full three-order object of the printed display at the cube R of scale l = R.scale, read at the base point z = cubeCenter R:

waveGaugeW2 m h R = ‖k_m-k_{l-h}‖_{L∞(R)}-gauge + waveGauge l m h z,

the first summand the proved uniform supremum gauge Stream.cubeSupBound and the second the derivative half of the sibling module. It dominates 3^{2l}‖k_m-k_{l-h}‖_{W^{2,∞}(z+cu_l)}; the zeroth-order half of that domination is streamIncrementLinftyNorm_le_waveGaugeW2.

Equations

• One or more equations did not get rendered due to their size.

theorem Algsuperdiff.Section3.Provider.MultiscaleEstimate.waveGaugeW2_nonneg {d : ℕ} (m : ℤ) (h : ℕ) (R : HCPolySupport.TriadicCube d) (omega : Cutoff.ShellSeq d) : 0 ≤ waveGaugeW2 m h R omega

theorem Algsuperdiff.Section3.Provider.MultiscaleEstimate.measurable_waveGaugeW2 {d : ℕ} (m : ℤ) (h : ℕ) (R : HCPolySupport.TriadicCube d) : Measurable fun (omega : Cutoff.ShellSeq d) => waveGaugeW2 m h R omega

theorem Algsuperdiff.Section3.Provider.MultiscaleEstimate.streamIncrementLinftyNorm_le_waveGaugeW2 {d : ℕ} (m : ℤ) (h : ℕ) (R : HCPolySupport.TriadicCube d) (omega : Cutoff.ShellSeq d) : Stream.streamIncrementLinftyNorm R.scale (R.scale - ↑h) m (Frozen.Assumptions.ShellField.translateSequence (HCPolySupport.cubeCenter R) omega) ≤ waveGaugeW2 m h R omega

The zeroth-order half of the fidelity statement. The literal L∞ norm of the realized increment k_m - k_{l-h} on the cube R, in the genuine L∞-norm carrier Stream.streamIncrementLinftyNorm read at the translated sample (equivalently: on cubeCenter R + cu_l, which is R), is dominated by the extended carrier.

noncomputable def Algsuperdiff.Section3.Provider.MultiscaleEstimate.waveAmpW2 {d : ℕ} (M : ABKModel d) (h j : ℕ) : ℝ

The per-cube Γ₂ amplitude of the extended carrier: the countable-triangle constant applied to the two legs.

Equations

• One or more equations did not get rendered due to their size.

theorem Algsuperdiff.Section3.Provider.MultiscaleEstimate.waveAmpW2_pos {d : ℕ} (M : ABKModel d) (h j : ℕ) : 0 < waveAmpW2 M h j

theorem Algsuperdiff.Section3.Provider.MultiscaleEstimate.waveAmpW2_nonneg {d : ℕ} (M : ABKModel d) (h j : ℕ) : 0 ≤ waveAmpW2 M h j

theorem Algsuperdiff.Section3.Provider.MultiscaleEstimate.isBigOWith_gammaSigma_waveGaugeW2 {d : ℕ} (M : ABKModel d) (m : ℤ) (h j : ℕ) {R : HCPolySupport.TriadicCube d} (hR : R.scale = m - ↑j) : HCPolySupport.IndependentSums.IsBigOWith (↑M.P) (HCPolySupport.IndependentSums.gammaSigma 2) (fun (omega : Cutoff.ShellSeq d) => waveGaugeW2 m h R omega) (waveAmpW2 M h j * 3 ^ (M.gamma * ↑R.scale))

The per-cube Γ₂ estimate at the extended carrier. On every triadic cube R of scale l = m - j,

3^{2l}‖k_m-k_{l-h}‖_{W^{2,∞}(z+cu_l)} ≤ O_{Γ₂}(waveAmpW2 M h j · 3^{γ l}).

The per-cube quantity, the grid maximum, and the scale sum

noncomputable def Algsuperdiff.Section3.Provider.MultiscaleEstimate.waveSizeW2 {d : ℕ} (M : ABKModel d) (m : ℤ) (h : ℕ) (R : HCPolySupport.TriadicCube d) (omega : Cutoff.ShellSeq d) : ℝ

The printed per-cube quantity of e.wave.sizes at the extended carrier, 3^{(2-γ)l}‖k_m-k_{l-h}‖_{W^{2,∞}(z+cu_l)}: the scale-l normalized carrier already carries 3^{2l}, so what is left is 3^{-γl}.

Equations

• Algsuperdiff.Section3.Provider.MultiscaleEstimate.waveSizeW2 M m h R omega = 3 ^ (-M.gamma * ↑R.scale) * Algsuperdiff.Section3.Provider.MultiscaleEstimate.waveGaugeW2 m h R omega

theorem Algsuperdiff.Section3.Provider.MultiscaleEstimate.waveSizeW2_nonneg {d : ℕ} (M : ABKModel d) (m : ℤ) (h : ℕ) (R : HCPolySupport.TriadicCube d) (omega : Cutoff.ShellSeq d) : 0 ≤ waveSizeW2 M m h R omega

theorem Algsuperdiff.Section3.Provider.MultiscaleEstimate.measurable_waveSizeW2 {d : ℕ} (M : ABKModel d) (m : ℤ) (h : ℕ) (R : HCPolySupport.TriadicCube d) : Measurable fun (omega : Cutoff.ShellSeq d) => waveSizeW2 M m h R omega

theorem Algsuperdiff.Section3.Provider.MultiscaleEstimate.isBigOWith_gammaSigma_waveSizeW2 {d : ℕ} (M : ABKModel d) (m : ℤ) (h j : ℕ) {R : HCPolySupport.TriadicCube d} (hR : R.scale = m - ↑j) : HCPolySupport.IndependentSums.IsBigOWith (↑M.P) (HCPolySupport.IndependentSums.gammaSigma 2) (fun (omega : Cutoff.ShellSeq d) => waveSizeW2 M m h R omega) (waveAmpW2 M h j)

The per-cube Γ₂ estimate at the printed normalization.

noncomputable def Algsuperdiff.Section3.Provider.MultiscaleEstimate.waveSizeMaxW2 {d : ℕ} (M : ABKModel d) (m : ℤ) (h j : ℕ) (omega : Cutoff.ShellSeq d) : ℝ

The grid maximum of the printed per-cube quantity at depth j = m - l, at the extended carrier.

Equations

• One or more equations did not get rendered due to their size.

theorem Algsuperdiff.Section3.Provider.MultiscaleEstimate.waveSizeW2_le_waveSizeMaxW2 {d : ℕ} (M : ABKModel d) (m : ℤ) (h j : ℕ) {R : HCPolySupport.TriadicCube d} (hR : R ∈ HCPolySupport.descendantsAtScale (HCPolySupport.originCube d m) (m - ↑j)) (omega : Cutoff.ShellSeq d) : waveSizeW2 M m h R omega ≤ waveSizeMaxW2 M m h j omega

theorem Algsuperdiff.Section3.Provider.MultiscaleEstimate.waveSizeMaxW2_nonneg {d : ℕ} (M : ABKModel d) (m : ℤ) (h j : ℕ) (omega : Cutoff.ShellSeq d) : 0 ≤ waveSizeMaxW2 M m h j omega

noncomputable def Algsuperdiff.Section3.Provider.MultiscaleEstimate.waveLayerAmpW2 {d : ℕ} (M : ABKModel d) (h j : ℕ) : ℝ

The per-scale Γ₁ amplitude at the extended carrier: the per-cube amplitude squared, times the grid-maximum penalty.

Equations

• One or more equations did not get rendered due to their size.

theorem Algsuperdiff.Section3.Provider.MultiscaleEstimate.isBigOWith_gammaSigma_waveSizeMaxW2_sq {d : ℕ} (M : ABKModel d) (m : ℤ) (h j : ℕ) : HCPolySupport.IndependentSums.IsBigOWith (↑M.P) (HCPolySupport.IndependentSums.gammaSigma 1) (fun (omega : Cutoff.ShellSeq d) => waveSizeMaxW2 M m h j omega ^ 2) (waveLayerAmpW2 M h j)

The per-scale Γ₁ estimate at the extended carrier.

noncomputable def Algsuperdiff.Section3.Provider.MultiscaleEstimate.waveSizesTotalW2 {d : ℕ} (M : ABKModel d) (m : ℤ) (h : ℕ) (s : ℝ) (omega : Cutoff.ShellSeq d) : ℝ

The left-hand side of e.wave.sizes at the extended carrier, reindexed by the depth j = m - l.

Equations

• One or more equations did not get rendered due to their size.

theorem Algsuperdiff.Section3.Provider.MultiscaleEstimate.legScaleAverage_waveSizeW2_sq_le {d : ℕ} (M : ABKModel d) (m : ℤ) (h j : ℕ) {s : ℝ} (hs : 0 < s) (omega : Cutoff.ShellSeq d) : (Localization.legScaleAverage (HCPolySupport.originCube d m) (m - ↑j) s fun (R : HCPolySupport.TriadicCube d) => waveSizeW2 M m h R omega ^ 2) ≤ waveSizeMaxW2 M m h j omega ^ 2

The per-scale power mean is at most the squared grid maximum. As in the sibling module, d ≠ 0 is derived from M, not assumed.

theorem Algsuperdiff.Section3.Provider.MultiscaleEstimate.measurable_waveScaleAverageW2 {d : ℕ} (M : ABKModel d) (m : ℤ) (h j : ℕ) {s : ℝ} (hs : 0 < s) : Measurable fun (omega : Cutoff.ShellSeq d) => Localization.legScaleAverage (HCPolySupport.originCube d m) (m - ↑j) s fun (R : HCPolySupport.TriadicCube d) => waveSizeW2 M m h R omega ^ 2

Measurability hook, per-scale level, extended carrier.

noncomputable def Algsuperdiff.Section3.Provider.MultiscaleEstimate.waveKW2 (d h : ℕ) : ℝ

The cutoff-dependent per-scale majorant of the extended carrier: the constant K for which the per-scale Γ₁ amplitude is at most (1+j)^2 3^{2γj} K.

Equations

• One or more equations did not get rendered due to their size.

theorem Algsuperdiff.Section3.Provider.MultiscaleEstimate.waveKW2_pos (d h : ℕ) : 0 < waveKW2 d h

theorem Algsuperdiff.Section3.Provider.MultiscaleEstimate.waveKW2_nonneg (d h : ℕ) : 0 ≤ waveKW2 d h

theorem Algsuperdiff.Section3.Provider.MultiscaleEstimate.waveLayerAmpW2_le {d : ℕ} (M : ABKModel d) (h j : ℕ) : waveLayerAmpW2 M h j ≤ 3 ^ (2 * M.gamma * ↑j) * ((1 + ↑j) ^ 2 * waveKW2 d h)

The per-scale amplitude is dominated by the quadratic base.

noncomputable def Algsuperdiff.Section3.Provider.MultiscaleEstimate.waveSizesConstW2 : ℝ

The dimensional constant of the extended wave-size endpoint.

Equations

• Algsuperdiff.Section3.Provider.MultiscaleEstimate.waveSizesConstW2 = 1024 * HCPolySupport.IndependentSums.gammaTriangleConst 1

theorem Algsuperdiff.Section3.Provider.MultiscaleEstimate.waveSizesConstW2_pos : 0 < waveSizesConstW2

theorem Algsuperdiff.Section3.Provider.MultiscaleEstimate.isBigOWith_gammaSigma_waveSizesTotalW2 {d : ℕ} (M : ABKModel d) (m : ℤ) (h : ℕ) {s : ℝ} (hs : 0 < s) (hs1 : s ≤ 1) (hsg : 8 * M.gamma ≤ s) : HCPolySupport.IndependentSums.IsBigOWith (↑M.P) (HCPolySupport.IndependentSums.gammaSigma 1) (fun (omega : Cutoff.ShellSeq d) => waveSizesTotalW2 M m h s omega) (waveSizesConstW2 * waveKW2 d h / s ^ 2)

e.wave.sizes at the extended carrier and the printed s^{-2}. For every integer cutoff h and every s ∈ [8γ, 1],

s Σ_{l ≤ m} 3^{-s(m-l)} (⨍_z (3^{(2-γ)l}‖k_m-k_{l-h}‖_{W^{2,∞}(z+cu_l)})^{2d/s})^{s/d} ≤ O_{Γ₁}(C(d,h) s^{-2}),

with the full W^{2,∞} object on the left. The exponent is exactly the printed one: the zeroth-order leg's quadratic base is what saturates it.

The printed cutoff h = ⌈C|log ε|⌉

noncomputable def Algsuperdiff.Section3.Provider.MultiscaleEstimate.waveCutoff (C0 eps : ℝ) : ℕ

The integer cutoff. The manuscript sets h := C|log ε|, which is not an integer, while every occurrence of k_{l-h} needs an integer scale. This is the ceiling; the overshoot is a fixed factor, absorbed into the dimensional constant below.

Equations

• Algsuperdiff.Section3.Provider.MultiscaleEstimate.waveCutoff C0 eps = ⌈C0 * |Real.log eps|⌉₊

theorem Algsuperdiff.Section3.Provider.MultiscaleEstimate.wave_sizes_bound (d : ℕ) {C0 : ℝ} (hC0 : 0 < C0) : ∃ (C : ℝ), 0 < C ∧ ∀ (M : ABKModel d) (m : ℤ) (eps s : ℝ), 0 < eps → eps ≤ 1 → 0 < s → s ≤ 1 → 8 * M.gamma ≤ s → HCPolySupport.IndependentSums.IsBigOWith (↑M.P) (HCPolySupport.IndependentSums.gammaSigma 1) (fun (omega : Cutoff.ShellSeq d) => waveSizesTotalW2 M m (waveCutoff C0 eps) s omega) (C * eps ^ (-C) / s ^ 2)

e.wave.sizes in the printed form, at the extended W^{2,∞} carrier. For every cutoff coefficient C₀ > 0 there is a constant C, depending only on the dimension and C₀, with

s Σ_{l ≤ m} 3^{-s(m-l)} (⨍_{z ∈ 3^l Z^d ∩ cu_m} (3^{(2-γ)l}‖k_m-k_{l-h}‖_{W^{2,∞}(z+cu_l)})^{2d/s})^{s/d} ≤ O_{Γ₁}(C s^{-2} ε^{-C})

at the integer cutoff h = ⌈C₀|log ε|⌉, for every ε ∈ (0,1] and every s ∈ [8γ, 1]. The left-hand side carries the full three-order object, not merely its derivative half.