WaveThirdTerm #

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

`e.wave.influence.bound`, the printed three-term right-hand side #

This module re-bases the lower leg of the node p.bfA.multiscalebound, the wave-oscillations step (ABK26, proof of Proposition p.bfA.multiscalebound, Step 2) onto the manuscript's own cube-averaged L⁴(cu_{n-k}) amplitude, and thereby splits the merged leg Provider.Multiscale.waveLowerTerm into the display's printed first and third terms. The printed display reads

  c gamma^{1/2} 3^{-gamma(n-k-h_k)} ||k_L - k_{n-k-h_k}||_{L^4bar(cu_{n-k})}
     <= gamma^{1/2} hsep^{1/2} + O_{Gamma_2}(gamma^{1/2}(L-l)^{1/2} 3^{gamma(L-l)})
        + O_{Gamma_{2(1+sigma)^{-1}}}(sigma^{-1} 3^{-(d/8)k_0}) ,

with l = n - k - h_k + hsep = n - k - ceil(b(1-b)^{-1}k) - k_0 deterministic; the parameters are named ell = l and lout = n - k here, so lout - ell = ceil(b(1-b)^{-1}k) + k_0 is exactly the manuscript's gain exponent, and in particular lout - ell >= k_0.

The partial reversal, and why it is needed #

Provider/Multiscale/WaveOscillations.lean provides the display in the merged two-leg form, at the uniform (L^infinity) per-layer gauge of e.km.kn.Linfty, and its section "Divergences from the printed right-hand side, recorded honestly" (its paragraph) records the reason the merged first and third terms cannot be split there: no uniform gauge can carry the 3^{-(d/8)k_0} gain. That gain is a cube-averaging phenomenon, and a bound on the supremum of a stationary nondegenerate field over a growing cube cannot decay in the cube size (the proved e.km.kn.Linfty amplitude in fact G like (lout-ell+i)^{1/2}). Splitting the third term therefore requires reinstating the manuscript's L⁴ Minkowski step for the lower leg — a partial reversal of form choice, for the lower leg only.

This module performs that reversal and nothing more:

streamIncrementLpNorm_add_le is the reinstated L⁴(cu_lout) triangle inequality, proved from Mathlib's ENNReal.lintegral_Lp_add_le at the volume-normalized cube average. It is used exactly once, to split k_L - k_{ell-hsep} at the scale ell, which is the manuscript's own first display.
The upper leg is not touched here. It keeps the local uniform formulation, where the passage to the large-cube amplitude costs constant 1 (Stream.streamIncrementLinftyNorm_le_largeCubeSupBound; |.| is the matrix operator norm, so a supremum of a pointwise-dominated quantity is dominated with constant 1). The form choice is therefore reversed for the lower leg and retained for the upper one.
The lower leg is priced by the proved unconditional e.km.kn.Lp (Provider.Stream.streamIncrementLpNorm_head_tail_gain) at p = 4, applied — as the manuscript does — to the whole lower increment k_ell - k_{ell-h} at each depth h, not per layer. Its deterministic head is C(d) min{gamma^{-1/2}, h^{1/2}} 3^{gamma ell} (waveL4Head_eq), which after the prefactor is the display's first term; its Gamma_2 part carries the gain 3^{-(d/(2p))(lout-ell)} = 3^{-(d/8)(lout-ell)} (waveL4TailScale_eq), which is the display's third term.

The assembly, and why the proved truncated-sum core suffices #

The manuscript assembles over 1_{{hsep = h}}; this repository assembles over 1_{{i < hsep}}, and the proved WaveOscillationsCore.isBigOWith_gammaSigma_truncatedSum is exactly that assembly. No head+tail variant of it is needed, because of one elementary observation: writing X_h for the nonnegative Gamma_2 part at depth h,

  X_{hsep}  <=  sum_{i < hsep} X_{i+1}                (waveL4Tail_le_range_sum)

— for hsep = H >= 1 the term i = H-1 of the right-hand sum is X_H, and for hsep = 0 both sides vanish because the empty increment has zero mass. The deterministic head needs no summation at all: it is evaluated at the single random depth hsep, which is what produces the printed hsep^{1/2} (summing per-layer heads would have produced the weaker hsep). The shift by one keeps every summand at a strictly positive depth, where e.km.kn.Lp's own binder n < m holds; that is why the proved core's 0 < a i is available.

Divergences from the printed right-hand side, recorded honestly #

The printed first term is the bare gamma^{1/2} hsep^{1/2}; the local one is C(d) gamma^{1/2} hsep^{1/2} with the explicit dimensional constant waveL4HeadConst d, which is what the manuscript's own proof produces (C 3^{gamma ell} hsep^{1/2}). With the left-hand constant c taken to be 1 (the manuscript does not pin c), the constant has to appear somewhere; it appears here. Class [C].
The printed third term is sigma^{-1} 3^{-(d/8)k_0}; the local scale waveTailGainScale is C(d, sigma_2) * (sum_i indicator scale) * 3^{-(d/8)(lout-ell)}, where the indicator series is the manuscript's own C b^{-1} sigma^{-1} factor at t = 1/sigma_2 and the gain is the manuscript's own exponent. Class [C].
The Orlicz exponent of the lower leg is kept free, exactly as in the proved WaveOscillations.lean: e.indc.O.sigma is applied at a general sigma_2 > 0, and at the manuscript's t = sigma/2, i.e. sigma_2 = 2/sigma, the delivered index 2 sigma_2/(2 + sigma_2) is the printed 2(1+sigma)^{-1} on the nose.

Main definitions #

waveL4Head, waveL4Tail, waveL4TailScale, waveL4HeadConst: the p = 4 head/tail carriers of e.km.kn.Lp at the lower increment.
waveHeadTerm, waveTailTerm: the printed first and third terms.
waveTailScale, waveTailGainScale: the third term's sharp series and its gain-factored dominator.

Main results #

streamIncrementLpNorm_add_le: the reinstated L⁴ Minkowski step.
measurable_streamIncrementLpMass: the cube mass is a random variable.
waveL4Head_eq, waveL4TailScale_eq: the closed forms of the head and of the gain.
waveHeadTerm_le: the printed C(d) gamma^{1/2} hsep^{1/2}.
waveTailScale_le_waveTailGainScale: the printed 3^{-(d/8)k_0} decay.
isBigOWith_gammaSigma_waveTailTerm_of_gates: the third term's Orlicz bound, in the premise-minimal form that reads the bad-event gates directly.

References #

ABK26, proof of p.bfA.multiscalebound, Step 2, (first display, indicator display, e.km.kn.Lp application, assembly).
ABK26, e.km.kn.Lp; e.kl.bounds.large; e.kmn.bounds; e.km.kn.Linfty; e.indc.O.sigma; e.multGammasig; l.Gamma.sigma.triangle; e.hsep.tails.
Provider/Multiscale/WaveOscillations.lean (the merged two-leg display and its section "Divergences from the printed right-hand side, recorded honestly" (its paragraph)), Provider/Multiscale/WaveOscillationsCore.lean (the truncated-sum assembly), Provider/Stream/IncrementLpLarge.lean (the unconditional corrected e.km.kn.Lp).

Deterministic preliminaries on the layer split #

Minkowski's inequality for the cube `L^p` norm #

The step reinstated by the partial reversal of form choice: the manuscript's own L⁴(cu_{n-k}) triangle inequality.

WaveThirdTerm #

e.wave.influence.bound, the printed three-term right-hand side #

The partial reversal, and why it is needed #

The assembly, and why the proved truncated-sum core suffices #

Divergences from the printed right-hand side, recorded honestly #

Main definitions #

Main results #

References #

Deterministic preliminaries on the layer split #

Minkowski's inequality for the cube L^p norm #

The L^p ≤ L^∞ passage on the observation cube #

Measurability of the cube mass in the sample #

The empty increment #

The p = 4 carriers of the re-based lower leg #

Summability of the re-based tail series #

The three legs of the printed display #

The generalized three-term provider #

`e.wave.influence.bound`, the printed three-term right-hand side #

Minkowski's inequality for the cube `L^p` norm #

The `L^p ≤ L^∞` passage on the observation cube #

The `p = 4` carriers of the re-based lower leg #