LocalizationOscillationEndpoint

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

e.lower.bound.oscillations at the recurrence parameters: the gamma^{15} endpoint

ABK26, l.approximate.recurrence.formula, e.lower.bound.oscillations, read at the parameters of e.recurrence.params with the multiplier a = 32:

• the buffer n = recurrenceMesoScale 32 gamma m h = m - h - 32 ceil|log_3 gamma|;
• the outer window scale n + N = m - h, N = recurrenceGap 32 gamma;
• the gauge shom_{m-h}^{-1} and the shell pair (m - h, m) of e.def.w;
• the big cube cu_K at the gate 10^10 gamma^{-1} <= K - m.

Three modules meet here.

• LocalizationOscillationDisplay.lean proves the first inequality of the printed chain, at a free buffer, conditionally on a coarse-energy envelope W and on the sample integrability of the per-cell coarse energies.
• LocalizationEnvelopeWire.lean discharges the coarse-energy envelope from e.nablaw.in.L.eight -- this is the manuscript's own "by e.nablaw.in.L.eight" step -- at the constant 3^d freshShellFourthEnergyConst Chead (gamma^100).
• LocalizationOscillationBudget.lean collapses the resulting three terms to gamma^{15}.
• LocalizationFluctuationCellIntegrable.lean discharges the display's last sample-space hypothesis, the integrability in the sample of the per-cell coarse energies to the fourth power.

What is proved

exists_gamma0_freshShellDirichlet_meshOscillation_le_gamma_pow_fifteen and its Neumann mirror: at every gamma below one explicit threshold,

  ( avsum_{z} E[ ‖grad w - (grad w)_{z+cu_n}‖^4_{L2bar(z+cu_n)} ] )^{1/4}
    + shom_{m-h}^{-1} 3^n E[ ‖grad(k_m - k_{m-h})‖^4_{Linf} ]^{1/4}
  <= gamma^{15} .

References

• ABK26, e.lower.bound.oscillations, e.nablaw.oscillations, e.nablaw.in.L.eight, e.recurrence.params, e.def.w.

The buffer identities

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.recurrenceMesoScale_add_recurrenceGap (a : ℕ) (gamma : ℝ) (m : ℤ) (h : ℕ) : recurrenceMesoScale a gamma m ↑h + ↑(recurrenceGap a gamma) = m - ↑h

The buffer and the gap add up to the inner scale of the fresh shell. Unconditional.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.recurrenceMesoScale_add_recurrenceGap_real (a : ℕ) (gamma : ℝ) (m : ℤ) (h : ℕ) : ↑(recurrenceMesoScale a gamma m ↑h) + ↑(recurrenceGap a gamma) = ↑(m - ↑h)

The same identity after the real cast. Unconditional.