GammaTenStripPathwise

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

NOTE: this module is an ordinary Provider helper.

A K-uniform integrable majorant for the two strip fourth energies

ABK26, e.def.w, e.Fz.def, e.nablaw.in.L.eight, read at the closure's own corrector families along the increment path.

What is proved

exists_strip_fourthEnergy_majorant produces one real number B >= 0, chosen before the localization scale K, such that for every K beyond the strip top n + h there is a sample function G >= 0, integrable for the cutoff-sample law, with E[G] <= B, dominating pathwise both shifted fourth energies

  fint_{cu_K} |e' + grad w_D|^4      and      fint_{cu_K} |e + F_z|^4 ,

where w_D is Closure.closureDirichletAlong and F_z is the flux leg neumannFluxField built from Closure.closureNeumannAlong.

The point of the statement shape is that B is chosen before K: the expectation bound is uniform in the localization scale.

The route

1. General-direction stream forcing. cubeEuclideanLpNorm_streamForcing_le of Corrector.FreshShellL8 is stated for directions of Euclidean length at most one. cubeEuclideanLpNorm_streamForcing_le_of_le below removes that normalization by the exact homogeneity streamForcing s omega n m e = streamForcing (s * c) omega n m (c⁻¹ • e), at the cost of the factor c for any c dominating both 1 and |e|.
2. Calderon--Zygmund, pathwise. Corrector.exists_cubeEuclideanL8_gradient_sq_sum_le, instantiated at Q = cu_K and at the two weak-solution facts of Closure.SplitProducerFold, bounds both gradient L^8 norms by A * t, where t is the fresh-shell L^8 norm and A is a constant free of K and of the sample.
3. L^4 <= L^8 and Minkowski. originCubeFourthEnergy_le_cubeEuclideanLpNorm_eight_pow_four and cubeEuclideanLpNorm_add_le turn that into the pathwise majorant 8 (a0^4 + (a1 t)^4) for both shifted fields, with a0, a1 free of K and of the sample.
4. The K-uniform quartic moment. Closure.Step5InputGradMoment.exists_integral_streamIncrementLpNorm_eight_pow_four_le bounds E[t^4] by a quantity free of K, which is exactly what lets B be produced before K.

No regime, no normalization

There is no inductionState, no M.gamma <= gamma0, no cstar bound, no |e| <= 1, no |e'| <= 1 and no 0 < h. The degenerate depth h = 0 is handled honestly: the fresh-shell increment sums over Finset.Ioc n n, which is empty, so the forcing vanishes identically and the majorant degenerates to a constant.

References

• ABK26, e.def.w; e.Fz.def; e.nablaw.in.L.eight; e.km.kn.Lp.
• None of the three enters a statement below: the majorant here is pathwise on the whole localization cube and carries no mesh at all.

Two elementary real inequalities

The Euclidean cube norm of a constant field

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.cubeEuclideanLpNorm_const {d : ℕ} (Q : HCPolySupport.TriadicCube d) {p : ENNReal} (hp : p ≠ 0) (c : HCPolySupport.Vec d) : (Corrector.cubeEuclideanLpNorm Q p fun (x : HCPolySupport.Vec d) => c) = HCPolySupport.Book.Ch02.vecNorm c

The Euclidean volume-normalized L^p norm of a constant vector field is the Euclidean length of that constant.

The stream forcing in a general direction

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.cubeEuclideanLpNorm_streamForcing_le_of_le {d : ℕ} {sinv : ℝ} (hsinv : 0 ≤ sinv) (l n m : ℤ) (omega : Cutoff.ShellSeq d) {e : HCPolySupport.Vec d} {c : ℝ} (hc1 : 1 ≤ c) (hce : HCPolySupport.Book.Ch02.vecNorm e ≤ c) : Corrector.cubeEuclideanLpNorm (HCPolySupport.originCube d l) 8 (Corrector.streamForcing sinv omega n m e) ≤ sinv * c * Stream.streamIncrementLpNorm 8 l n m omega

Step 1: the L^8 bound on the forcing of e.def.w in an arbitrary direction.

Corrector.cubeEuclideanLpNorm_streamForcing_le is stated for directions of Euclidean length at most one. Since streamForcing is linear in the direction, that normalization can be traded for any c dominating both 1 and |e|:

  ‖ s (k_m - k_n) e ‖_{L8bar(cu_l)}  <=  s c ‖k_m - k_n‖_{L8bar(cu_l)} .

on 0 <= s, 1 <= c and |e| <= c only; no regime, no model.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.streamForcing_self_eq_zero {d : ℕ} (sinv : ℝ) (omega : Cutoff.ShellSeq d) (n : ℤ) (e : HCPolySupport.Vec d) : Corrector.streamForcing sinv omega n n e = fun (x : HCPolySupport.Vec d) => 0

The degenerate depth. The finite stream increment sums over Ioc n n, which is empty, so the forcing of e.def.w at zero depth vanishes identically.

The spatial step, at a shifted field

The K-uniform majorant

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.exists_strip_fourthEnergy_majorant (d : ℕ) [NeZero d] (hd : 2 ≤ d) (M : ABKModel d) (n : ℤ) (h : ℕ) (e e' : HCPolySupport.Vec d) : ∃ (B : ℝ), 0 ≤ B ∧ ∀ (K : ℕ), n + ↑h ≤ ↑K → ∃ (G : Cutoff.CutoffSample d → ℝ), (∀ (omega : Cutoff.CutoffSample d), 0 ≤ G omega) ∧ MeasureTheory.Integrable G ↑(Cutoff.cutoffSampleLaw M) ∧ ∫ (omega : Cutoff.CutoffSample d), G omega ∂↑(Cutoff.cutoffSampleLaw M) ≤ B ∧ (∀ (omega : Cutoff.CutoffSample d), (originCubeFourthEnergy ↑K fun (x : HCPolySupport.Vec d) => e' + (closureDirichletAlong M n h K e ↑omega).grad x) ≤ G omega) ∧ ∀ (omega : Cutoff.CutoffSample d), (originCubeFourthEnergy ↑K fun (x : HCPolySupport.Vec d) => e + neumannFluxField (Annealed.sigmaBar M n) (↑omega) n (n + ↑h) e' (closureNeumannAlong M n h K e' ↑omega) x) ≤ G omega

A K-uniform integrable majorant for the two strip fourth energies.

There is one nonnegative B, chosen before the localization scale K, such that for every K beyond the strip top n + h there is a nonnegative integrable sample function G with E[G] <= B dominating pathwise both

  fint_{cu_K} |e' + grad w_D|^4      and      fint_{cu_K} |e + F_z|^4 ,

with w_D = Closure.closureDirichletAlong M n h K e the Dirichlet corrector of e.def.w and F_z the flux leg neumannFluxField of e.Fz.def built from the Neumann corrector Closure.closureNeumannAlong M n h K e'.

There is no regime hypothesis: no inductionState, no M.gamma <= gamma0, no bound on cstar, no normalization |e| <= 1 or |e'| <= 1, and no 0 < h. The only binders beyond the typing data are hd : 2 <= d and, per scale, n + h <= K.