LocalizationOscillationDisplay

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

e.lower.bound.oscillations at the fresh-shell correctors

Source displays in ABK26:

• e.lower.bound.oscillations (label; \begin{multline}, \end{multline}; the printed chain occupies),
• e.nablaw.oscillations (label; display),
• e.recurrence.params (label), which fixes n and K,
• e.def.w (label), which defines the two finite-volume correctors.

ABK26 asserts, for w either of the two correctors of e.def.w,

  ( avsum_{z in 3^n Zd cap cu_K} 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(cu_{m-h})} ]^{1/4}
  <= C 3^{-(m-h-n)}
     + C shom_{m-h}^{-1} 3^{-(m-h-n)} 3^{gamma(m-h)} gamma^{-1}
     + C 3^{-(K-m+h)/4}
  <= gamma^{15} .

This module assembles the first inequality at the manuscript's own carriers: the actual finite-volume Dirichlet and Neumann correctors on cu_K, the actual fresh-shell forcing, the actual triadic meso grid of scale n = m - h - N, and the actual shell-derivative gauge of e.nabla.km.kn.infty.

The three consumed ingredients

• the per-site estimate e.nablaw.oscillations at the genuine carriers, Corrector.exists_freshShellDirichlet_gradient_oscillation_interior_mesh_localGauge and its Neumann mirror (module OscillationAssemblyShell);
• the fourth moment of the forcing gauge, integral_shellDerivNormSum_rpow_four_le and mul_shellDerivNormSum_momentRoot_four_le_gap (module LocalizationOscillationTail);
• the grid functional and its two-term majorant step, gridFourthMomentRoot_le_add_of_le (module LocalizationOscillationGridMoment), on the interior grid interiorMesoCubeGrid of LocalizationGrid.

What is proved

• meshOscillationCell, meshEnergyCell -- the two per-cube quantities of the display, based at the cube's own site triadicCubeShift R.
• openCubeAtScale_subset_of_mem_interiorMesoCubeGrid -- membership in the interior grid at outer scale n + N - 1 is exactly the containment z + cu_{n+N} subset cu_K that e.nablaw.oscillations needs.
• integrable_shellDerivNormSum_rpow_four, gridFourthMoment_shellDerivNormSum_le -- the forcing gauge is fourth-power integrable and its grid fourth moment obeys the uniform shell bound.
• exists_freshShellDirichlet_gradient_oscillation_lower_bound_display and exists_freshShellNeumann_gradient_oscillation_lower_bound_display -- the display itself, at the two correctors.

Declared divergences from the printed statement

• The grid is the interior grid. The manuscript averages over the unrestricted mesh 3^n Zd cap cu_K while the preceding per-site estimate holds only where z + cu_{m-h} subset cu_K. Averaging only over the interior mesh is the route taken here: the grid below is interiorMesoCubeGrid d K n (n + N - 1). Consequently the printed third term C 3^{-(K-m+h)/4} does not appear: there is no boundary contribution to bound.
• The printed boundary exponent is unreachable anyway. The quarter exponent 3^{-(K-m+h)/4} follows only from a uniform-in-window annealed fourth moment that is not available, and the global L^8 envelope gives at best 3^{-(K-m+h)/8}. Nothing below asserts either exponent.
• The gap restriction d + 3 <= N. The per-site estimate is the birth-scale telescope, not the false adjacent-cube 1/3-contraction; its coarse leg needs a gap of at least d + 3 scales. The restriction is inherited verbatim and appears as an explicit hypothesis.
• The forcing amplitude is sharper than printed. The printed second term carries gamma^{-1}; the bound below carries the number of telescope scales N = m - h - n on the oscillation leg and no factor at all on the standalone leg, with the absolute constant shellDerivGammaFourthConst of the class Gamma_2. In the regime of e.recurrence.params one has N <= 2 gamma^{-1} (recurrenceGap_le_two_mul_inv, module LocalizationParams, under its coverage gate), so the bound below implies the printed one up to the absolute factor 2; nothing is weakened to match the printed form.
• The forcing random variable is the dominating gauge, not the L^infty norm. Both on the left of the display and inside the per-site estimate, the manuscript's ‖grad(k_m - k_{m-h})‖_{Linf(z + cu_{m-h})} is replaced by the summed first-derivative shell gauge shellDerivNormSum, which dominates it by the triangle inequality over the shells with no loss (see the carrier note of LocalizationOscillationTail). The statements below therefore imply the printed ones and are stronger. The standalone left-hand term is moreover stated at an arbitrary base point z0, of which the manuscript's untranslated cu_{m-h} is one instance.
• The triangle step costs 8^{1/4}. The manuscript's implicit Minkowski inequality in L^4(counting x P) has constant 1; the elementary route used here has the absolute constant 8^{1/4}, written out in oscillationDisplayConst and absorbed by the manuscript's dimension-only C.
• The visible sqrt d and the explicit sigmaInv. The carrier Vec d is sup-normed while the shell gauge is Euclidean, so the forcing amplitude reads sigmaInv * sqrt d * |e|_2; the manuscript's C is dimension-only and absorbs the sqrt d. The manuscript's shom_{m-h}^{-1} is the free nonnegative parameter sigmaInv here; no value is assumed for it.
• None of the three is assumed or asserted below.

What is not proved here

The meso-window energy average hcoarse is NOT discharged here. The manuscript writes "by e.nablaw.in.L.eight", which controls the single global normalized L^8 norm of grad w on cu_K. Passing from that to avsum_{z} E[ ‖grad w‖^4_{L2bar(z + cu_{m-h})} ] requires a bounded-overlap count: the windows z + cu_{m-h} indexed by the scale-n grid overlap, each point of cu_K lying in 3^{d(m-h-n)} of them, so the tiling identity cubeAverage_originCube_eq_mesoGridAverage of LocalizationGrid -- which is a partition statement -- does not apply. The correct multiplicity is 3^{dN} and makes the constant 1, but no covering lemma at ratio 3^N is available in this repository; LocalizationGrid's transfer is at ratio 3 only. The binder hcoarse therefore carries the whole passage, visibly, at every instantiation site.

The two per-cube quantities of the display

noncomputable def Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.meshOscillationCell {d : ℕ} (n : ℤ) (u : HCPolySupport.Vec d → HCPolySupport.Vec d) (R : HCPolySupport.TriadicCube d) : ℝ

The left-hand side of e.nablaw.oscillations at the cube R, based at the cube's own site: ‖grad w - (grad w)_{z + cu_n}‖_{L2bar(z + cu_n)}.

Equations

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

noncomputable def Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.meshEnergyCell {d : ℕ} (ell : ℤ) (u : HCPolySupport.Vec d → HCPolySupport.Vec d) (R : HCPolySupport.TriadicCube d) : ℝ

The coarse energy on the outer window of e.nablaw.oscillations: ‖grad w‖_{L2bar(z + cu_{m-h})}.

Equations

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

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.meshOscillationCell_nonneg {d : ℕ} (n : ℤ) (u : HCPolySupport.Vec d → HCPolySupport.Vec d) (R : HCPolySupport.TriadicCube d) : 0 ≤ meshOscillationCell n u R

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.meshEnergyCell_nonneg {d : ℕ} (ell : ℤ) (u : HCPolySupport.Vec d → HCPolySupport.Vec d) (R : HCPolySupport.TriadicCube d) : 0 ≤ meshEnergyCell ell u R

The interior grid supplies the containment of e.nablaw.oscillations

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.openCubeAtScale_subset_of_mem_interiorMesoCubeGrid {d : ℕ} {K n : ℤ} {N : ℕ} {R : HCPolySupport.TriadicCube d} (hR : R ∈ interiorMesoCubeGrid d K n (n + ↑N - 1)) : HCPolySupport.Book.Ch03.openCubeAtScale (HCPolySupport.triadicCubeShift R) (n + ↑N) ⊆ HCPolySupport.openCubeSet (HCPolySupport.originCube d K)

Membership in the interior grid at outer scale n + N - 1 is the containment z + cu_{n+N} ⊆ cu_K printed.

The forcing gauge: integrability and the grid moment

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.integrable_shellDerivNormSum_rpow_four {d : ℕ} (M : ABKModel d) {lowScale highScale : ℤ} (hlt : lowScale < highScale) (z : HCPolySupport.Vec d) : MeasureTheory.Integrable (fun (omega : Cutoff.ShellSeq d) => shellDerivNormSum lowScale highScale z omega ^ 4) ↑M.P

The forcing gauge of e.nablaw.oscillations is fourth-power integrable. Same route as integral_shellDerivNormSum_rpow_four_le: the weak-Orlicz tail e.nabla.km.kn.infty at the translated cube, through CoarseGraining's layer-cake bound.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.gridFourthMoment_shellDerivNormSum_le {d : ℕ} (M : ABKModel d) (I : Finset (HCPolySupport.TriadicCube d)) {lowScale highScale : ℤ} (hlt : lowScale < highScale) : (gridFourthMoment (↑M.P) I fun (R : HCPolySupport.TriadicCube d) (omega : ℤ → Frozen.Assumptions.ShellField d) => shellDerivNormSum lowScale highScale (HCPolySupport.triadicCubeShift R) omega) ≤ (shellDerivGammaFourthConst * 3 ^ ((M.gamma - 1) * ↑lowScale)) ^ 4

The grid fourth moment of the forcing gauge. The per-site bound of integral_shellDerivNormSum_rpow_four_le is uniform in the base point, so it survives the grid average unchanged.

The constant of the display

noncomputable def Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.oscillationDisplayConst (C : ℝ) : ℝ

The absolute constant of the display: the 8^{1/4} of the elementary triangle step, the dimension-only constant C of e.nablaw.oscillations, and the Gamma_2 fourth-moment constant of the forcing gauge, combined so that a single constant dominates all three terms.

Equations

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

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.oscillationDisplayConst_nonneg {C : ℝ} (hC : 0 ≤ C) : 0 ≤ oscillationDisplayConst C

The core assembly

The display at the two correctors

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.exists_freshShellDirichlet_gradient_oscillation_lower_bound_display {d : ℕ} (hd : 0 < d) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (M : ABKModel d) (K n : ℤ) (N : ℕ), d + 3 ≤ N → ∀ (highScale : ℤ), n + ↑N < highScale → ∀ (sigmaInv : ℝ), 0 ≤ sigmaInv → ∀ (e z₀ : HCPolySupport.Vec d) (wD : Cutoff.ShellSeq d → HCPolySupport.H10Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d K))), (∀ (omega : Cutoff.ShellSeq d), HCPolySupport.IsZeroTraceDirichletRhsWeakSolution (fun (x : HCPolySupport.Vec d) => 1) (HCPolySupport.openCubeSet (HCPolySupport.originCube d K)) (wD omega) fun (x : HCPolySupport.Vec d) => -Corrector.streamForcing sigmaInv omega (n + ↑N) highScale e x) → ∀ (W : ℝ), 0 ≤ W → (gridFourthMoment (↑M.P) (interiorMesoCubeGrid d K n (n + ↑N - 1)) fun (R : HCPolySupport.TriadicCube d) (omega : ℤ → Frozen.Assumptions.ShellField d) => meshEnergyCell (n + ↑N) (wD omega).grad R) ≤ W ^ 4 → (∀ R ∈ interiorMesoCubeGrid d K n (n + ↑N - 1), MeasureTheory.Integrable (fun (omega : Cutoff.ShellSeq d) => meshEnergyCell (n + ↑N) (wD omega).grad R ^ 4) ↑M.P) → (gridFourthMomentRoot (↑M.P) (interiorMesoCubeGrid d K n (n + ↑N - 1)) fun (R : HCPolySupport.TriadicCube d) (omega : ℤ → Frozen.Assumptions.ShellField d) => meshOscillationCell n (wD omega).grad R) + sigmaInv * (3 ^ ↑n * (∫ (omega : Cutoff.ShellSeq d), shellDerivNormSum (n + ↑N) highScale z₀ omega ^ 4 ∂↑M.P) ^ 4⁻¹) ≤ C * (3 ^ (-↑N) * W) + C * (↑N * (sigmaInv * √↑d * HCPolySupport.Book.Ch02.vecNorm e)) * (3 ^ (-↑N) * 3 ^ (M.gamma * (↑n + ↑N))) + C * sigmaInv * (3 ^ (-↑N) * 3 ^ (M.gamma * (↑n + ↑N)))

e.lower.bound.oscillations for the Dirichlet corrector of e.def.w, on the interior meso grid.

The second printed term is proved in the sharper form carrying N = m - h - n instead of gamma^{-1}.

Conditional A. The caller supplies hd : 0 < d, the telescope gap `hN: d

• 3 ≤ N, the nonempty shell range hlt: n + N < highScale, hsigma: 0 ≤ sigmaInvforshom_{m-h}^{-1}, the weak-solution property hwDofe.def.wat every sample, and the two propositionshcoarse, hcoarseIntabout the meso-window corrector energies. hcoarseis the manuscript's "by `e.nablaw.in.L.eight`" step and is not discharged here; see the module's open obstruction.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.exists_freshShellNeumann_gradient_oscillation_lower_bound_display {d : ℕ} (hd : 0 < d) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (M : ABKModel d) (K n : ℤ) (N : ℕ), d + 3 ≤ N → ∀ (highScale : ℤ), n + ↑N < highScale → ∀ (sigmaInv : ℝ), 0 ≤ sigmaInv → ∀ (e' z₀ : HCPolySupport.Vec d) (wN : Cutoff.ShellSeq d → HCPolySupport.H1MeanZeroFunction (HCPolySupport.openCubeSet (HCPolySupport.originCube d K))), (∀ (omega : Cutoff.ShellSeq d), HCPolySupport.IsMeanZeroNeumannRhsWeakSolution (fun (x : HCPolySupport.Vec d) => 1) (HCPolySupport.openCubeSet (HCPolySupport.originCube d K)) (wN omega) fun (x : HCPolySupport.Vec d) => -Corrector.streamForcing sigmaInv omega (n + ↑N) highScale e' x) → ∀ (W : ℝ), 0 ≤ W → (gridFourthMoment (↑M.P) (interiorMesoCubeGrid d K n (n + ↑N - 1)) fun (R : HCPolySupport.TriadicCube d) (omega : ℤ → Frozen.Assumptions.ShellField d) => meshEnergyCell (n + ↑N) (wN omega).toH1Function.grad R) ≤ W ^ 4 → (∀ R ∈ interiorMesoCubeGrid d K n (n + ↑N - 1), MeasureTheory.Integrable (fun (omega : Cutoff.ShellSeq d) => meshEnergyCell (n + ↑N) (wN omega).toH1Function.grad R ^ 4) ↑M.P) → (gridFourthMomentRoot (↑M.P) (interiorMesoCubeGrid d K n (n + ↑N - 1)) fun (R : HCPolySupport.TriadicCube d) (omega : ℤ → Frozen.Assumptions.ShellField d) => meshOscillationCell n (wN omega).toH1Function.grad R) + sigmaInv * (3 ^ ↑n * (∫ (omega : Cutoff.ShellSeq d), shellDerivNormSum (n + ↑N) highScale z₀ omega ^ 4 ∂↑M.P) ^ 4⁻¹) ≤ C * (3 ^ (-↑N) * W) + C * (↑N * (sigmaInv * √↑d * HCPolySupport.Book.Ch02.vecNorm e')) * (3 ^ (-↑N) * 3 ^ (M.gamma * (↑n + ↑N))) + C * sigmaInv * (3 ^ (-↑N) * 3 ^ (M.gamma * (↑n + ↑N)))

e.lower.bound.oscillations for the Neumann corrector of e.def.w, on the interior meso grid. The Neumann mirror of the previous statement; the manuscript's "the same results are valid for w_{N,e'}^{(K)}".

Conditional A. The binders are those of the Dirichlet leg, with hwN the mean-zero Neumann weak-solution property in place of the zero-trace one.