WaveSizes #

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

Provider: the derivative half of the wave-size sum `e.wave.sizes` #

Local provider for the second of the three displays that the proof of ABK26's Proposition p.multiscale.estimate reduces to, namely e.wave.sizes.

The display bounds the weighted scale sum of the grid power means of the squared wave sizes -- the size of the layers k_m - k_{l-h} that the localization step injects on each cube z + cu_l -- by a Gamma_1 tail at amplitude s^{-2} eps^{-C}.

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

What this module carries, and what it does NOT #

The printed display carries the volume-normalized Sobolev norm ‖k_m - k_{l-h}‖_{W^{2,∞}(z + cu_l)}. At p = ∞ that object is a maximum, not a sum: at p = ∞ on a cube of side 3^l (|U|^{-1/d} is 3^{-l}), iterated to second order, gives all norms on z+cu_l in L∞, 3^{2l}‖f‖_{W^{2,∞}} = max{‖f‖, 3^l‖∇f‖, 3^{2l}‖∇²f‖}. This module and its sibling work with the three-order sum ‖f‖ + 3^l‖∇f‖ + 3^{2l}‖∇²f‖, which dominates that maximum (nonnegative legs) and is at most 3 times it, so every bound proved against the sum bounds the printed maximum: nothing is over-claimed. An earlier version joined the two with =; that equation was false and is withdrawn. "The three-order object" below means the sum.

This module carries the derivative half only, i.e. the last two terms, under the name waveGauge:

`waveGauge l m h z = 3^l Σ_{k ∈ (l-h, m]} ‖∇ j_k‖_{L∞(z+cu_l)}

3^{2l} Σ_{k ∈ (l-h, m]} ‖∇² j_k‖_{L∞(z+cu_l)}`,

built from the proved layer gauges Stream.localCubeDerivNorm and Stream.localCubeSecondDerivNorm read at the base point z through the frozen translation action ShellField.translate z.

The zeroth-order L∞ leg, the extended carrier waveGaugeW2 that adds it, the zeroth-order fidelity statement, the integer cutoff, and the headline wave_sizes_bound all live in the sibling module Provider/MultiscaleEstimate/WaveSizesZeroth.lean, which imports this one. Every estimate below is therefore a derivative-half estimate and is named or documented as such.

The zeroth-order term is load-bearing; it is not an omission the source sanctions. An earlier version of this docstring claimed the contrary, on the ground that the Section 2.4 sensitivity input consumes only ‖∇h‖_{W^{1,∞}}. That claim was false and is withdrawn (and the adjudication recorded with it). The frozen remainder of Frozen/Section24/ResponseJSensitivity.lean is

C δ⁻¹ (vecNormSq p * h.w1Infinity ^ 2 * λ⁻¹ + |vecDot p q| * h.gradientW1Infinity ^ 2 * λ⁻¹ ^ 2),

and UnitCubeSkewW2Infinity.w1Infinity (Frozen/Section24/UnitCubeSkewW2Infinity/W1Infinity.lean) is max{‖∇h‖_{L∞(□₀)}, ‖h‖_{L∞(□₀)}}: it contains the zeroth-order L∞ term, at the coefficient vecNormSq p, which at the wave call site (p = shom_{l-h}^{-1/2} e) is |shom_{l-h}^{-1/2}e|² > 0. That remainder is consumed verbatim at Provider/BadEvents/GoodLocalEvents.lean (responseJ_sensitivity_of_mem_goodLocalEvent_of_lambdaTransfer). Only gradientW1Infinity = max{‖∇²h‖_{L∞}, ‖∇h‖_{L∞}} is derivative-only, and it is the sensitivity gate, not the remainder. The printed e.J.sensitivity.apppp merges both remainders into the single 3^{4l}‖·‖²_{W^{2,∞}} object, which is exactly why the wave display is stated at the full W^{2,∞} norm.

Main definitions #

layerWeight: the observation-scale reweighting max{3^{l-k}, 3^{2(l-k)}}.
waveGauge: the scale-l normalized derivative gauge of the missing layers on a translated cube (the derivative half of the printed norm).
waveAmp, waveGridConst: the constants, all explicit.

Main results #

three_rpow_split: the printed exponent split ½s(m-l) ≥ ¼s(m-l) + 2γ(m-l). Reusable development arithmetic, together with half_le_one_sub_three_rpow_neg (the geometric-gap bound) and isBigOWith_gammaSigma_of_eq_zero (the empty-range degenerate case).
isBigOWith_gammaSigma_waveGauge: the per-cube Gamma_2 estimate, uniform in the base point and free of the scale gap m - l.
measurable_waveGauge: the measurability interface of the carrier.

The grid/lattice identification, asserted not proved #

The printed display sums over the lattice points z ∈ 3^l Z^d ∩ cu_m and reads each summand on z + cu_l. This file realizes that index set as the finite family of triadic descendants descendantsAtScale (originCube d m) l, with z:= cubeCenter R for R a descendant. This is the development convention inherited from the docstring of Localization.legScaleAverage (Provider/Localization/Breakdown.lean), where the same identification is made for e.mathcal.E.breakdown; it is asserted, not proved, and no declaration in this file depends on it being a bijection.

theorem cubeCenter_injOn_descendantsAtScale (Q : TriadicCube d) (k : ℤ) :
    Set.InjOn cubeCenter ↑(descendantsAtScale Q k)

theorem cubeCenter_image_descendantsAtScale_eq_lattice (Q : TriadicCube d)
    {k : ℤ} (hk : k ≤ Q.scale) :
    (fun R => cubeCenter R) '' ↑(descendantsAtScale Q k)
      = {z : Vec d | (∀ i, ∃ p : ℤ, z i = (3 : ℝ) ^ k * (p : ℝ))
          ∧ z ∈ cubeSet Q}

Until they are proved the identification is a reading of the display, and any downstream statement that needs the printed lattice literally must supply them. What is proved here is that cubeCenter R = triadicCubeShift R holds by definitional unfolding, so the cube R and the translated cube cubeCenter R + cu_{R.scale} are the same set (openCubeSet_eq_translateSet_originCube_of_triadicCube); that identity, and not the lattice enumeration, is what the estimates below use.

Deviations from the printed proof, all disclosed #

Per-layer, not summed, stream input. The printed proof applies the summed display e.W.1.inf.bound as a black box. That display is stated at the own-scale normalization 3^k, 3^{2k}, while the wave gauge needs the observation-scale normalization 3^l, 3^{2l}; converting costs the factor 3^{2(l-k)} ≤ 3^{2h} on every layer, including the layers k > l where the true weight 3^{l-k} is a decay. Routed that way the per-scale amplitude grows like (m-l)^2 (through min{γ^{-1}, m-l+h}^2) and the l-sum proves at s^{-3}, one power worse than the printed s^{-2}; this is finding (3). This file therefore applies the per-layer proved estimate isBigOWith_gammaSigma_largeCubeDerivGauge_translate with the honest weight max{3^{l-k}, 3^{2(l-k)}}. The layers k > l then sum geometrically to a dimensional constant, the per-scale amplitude is independent of the scale gap m-l, and the l-sum is s^{-1} ≤ s^{-2}.
The comparator for the summed input is the translated summed gauge, not the frozen display. The comparator of the carrier at a base point is Σ_{k ∈ (l-h,m]} largeCubeDerivGauge l k (translate z (ω k)), whose Γ₂ estimate is Stream.isBigOWith_gammaSigma_largeCubeDerivGaugeSum_translate (Provider/Stream/TranslatedLargeCubeW1Inf.lean). The frozen Frozen.Section3.stream_derivative_sum_bound is untranslated (no base point, binder n ≤ min m l), is not imported by this module, and its own internal input is the untranslated Stream.isBigOWith_gammaSigma_largeCubeDerivGauge (Provider/Stream/LargeCubeW1Inf.lean). The honest comparator for the printed route at a base point is therefore the translated summed statement, and that is what is cited. An earlier version of this docstring named the frozen declaration instead; that naming was inaccurate and is withdrawn.
Grid power mean by the maximum lemma. The printed proof passes the per-cube Gamma_1 bound through the power mean (⨍_z (·)^{d/s})^{s/d} silently. Here the passage is paid honestly: by Localization.legScaleAverage_le_const the power mean is at most the grid maximum, and the grid maximum of Gamma_2 variables at a common amplitude costs the factor (3 max{1, log N})^{1/2} of the proved maximum lemma (ABK26 l.maximums.Gamma.s, in the strengthened N = 1-inclusive form disclosed above), i.e. a factor linear in m-l after squaring.
The l-sum is stated at s^{-1}, the printed form at s^{-2}. On the derivative half the route above is strictly sharper than the printed amplitude; the printed form follows because s ≤ 1. The full carrier does not enjoy this: the zeroth-order leg has a genuinely quadratic base and proves at exactly the printed s^{-2} (WaveSizesZeroth.lean).

References #

ABK26, e.wave.sizes.
ABK26, e.J.sensitivity.apppp (the consumer shape).
ABK26, e.W.1.inf.bound.
ABK26, l.Gamma.sigma.triangle.
ABK26, l.maximums.Gamma.s.

Elementary real arithmetic #

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

WaveSizes #

Provider: the derivative half of the wave-size sum e.wave.sizes #

What this module carries, and what it does NOT #

Main definitions #

Main results #

The grid/lattice identification, asserted not proved #

Deviations from the printed proof, all disclosed #

References #

Elementary real arithmetic #

The wave carrier #

The per-cube Gamma_2 estimate #

The grid maximum #

Provider: the derivative half of the wave-size sum `e.wave.sizes` #

The per-cube `Gamma_2` estimate #