GammaTenInteriorGaugedEnvelope

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

The interior Besov envelope of the gauged bfF_z, at one localization cube

ABK26, Step 2 of l.approximate.recurrence.formula, e.lower.bound.oscillations, e.Fz.def, e.shom.h.bounds.

What this module does

Closure.GammaTenStripEnvelopeTwoLeg.exists_besovEnvelope_two_legs_interiorMesoCubeGrid produces one envelope dominating |c_1| times the Besov tower of a first raw field and |c_2| times that of a second. The body of Closure.ClosureInteriorSplit.ClosureInteriorBesovEnvelopeInput asks instead for an envelope dominating the towers of the two gauged legs of bfF_z. By

cubeBesovPositiveVectorPartialSeminormTwo_gauged_localizationFz_potential and ..._flux --- each gauged tower is the corresponding scalar multiple of the raw tower, and

• Closure.GammaTenGaugeScalarCap.abs_gaugeScalar_potential_le / ..._flux_le --- both scalars are capped by the absolute 4 . 3^9,

the two statements are the same statement, and this module performs the substitution at one fixed localization cube. Nothing analytic happens here: the per-cell typing data and the two per-depth grid roots are binders.

What is proved

• exists_besovEnvelope_gaugedLocalizationFz_interiorMesoCubeGrid --- the body of ClosureInteriorBesovEnvelopeInput at one (M, n, h, K, e, e') and one mesh scale nmesh, from the scale bookkeeping, the boundary gate, the numerical threshold hthr, the gauge-ratio cap hgauge, the six cellwise typing binders and the two per-depth inputs at the common constant 2 d.

Binders

Those of the two-leg envelope, re-read at the closure's own two raw fields (the Dirichlet corrector gradient and the Neumann flux field of the closure's families), together with hgauge and the descendant-wise L^2 memberships the two gauge identities need. No smallness gate beyond hthr, no model estimate and no stationarity occurs.

Scope

Internal Provider infrastructure for the Step-2 fluctuation estimate. There is no sorry, no admit, no custom axiom and no set_option maxHeartbeats.

References

• ABK26, l.approximate.recurrence.formula Step 2, e.lower.bound.oscillations, e.Fz.def, e.shom.h.bounds.

The interior grid sits inside the localization cube

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.openCubeSet_subset_originCube_of_mem_interiorMesoCubeGrid {d : ℕ} {K nmesh outer : ℤ} (hn : nmesh ≤ K) {R : HCPolySupport.TriadicCube d} (hR : R ∈ interiorMesoCubeGrid d K nmesh outer) : HCPolySupport.openCubeSet R ⊆ HCPolySupport.openCubeSet (HCPolySupport.originCube d K)

Every cell of the interior meso grid at a scale below the localization scale lies in the localization cube: it is a descendant of it.

The gauged two-leg envelope at one localization cube

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.exists_besovEnvelope_gaugedLocalizationFz_interiorMesoCubeGrid {d : ℕ} [NeZero d] (M : ABKModel d) (n : ℤ) (h K : ℕ) (e e' : HCPolySupport.Vec d) {nmesh : ℤ} {p g : ℕ} (hKp : ↑K = nmesh + ↑p) (houter : n + 1 = nmesh + ↑g) (hgp : g ≤ p) (hno : nmesh ≤ n) (hsmall : ↑d * (3 ^ g / 3 ^ p) ≤ 1 / 2) (hgamma0 : 0 < M.gamma) (hthr : 200 * (4 * (2 * ↑d) * (4 * 3 ^ 9)) ^ 4 * M.gamma ^ 4 ≤ 1) (hgauge : gaugeRatio (Annealed.sigmaBar M n) (Annealed.sigmaBar M (n + ↑h - 1)) ≤ 4 * 3 ^ 9) (hmemD : ∀ (omega : Cutoff.CutoffSample d) (S : HCPolySupport.TriadicCube d), HCPolySupport.openCubeSet S ⊆ HCPolySupport.openCubeSet (HCPolySupport.originCube d ↑K) → MeasureTheory.MemLp (closureDirichletAlong M n h K e ↑omega).grad 2 (HCPolySupport.normalizedCubeMeasure S)) (hmemN : ∀ (omega : Cutoff.CutoffSample d) (S : HCPolySupport.TriadicCube d), HCPolySupport.openCubeSet S ⊆ HCPolySupport.openCubeSet (HCPolySupport.originCube d ↑K) → MeasureTheory.MemLp (neumannFluxField (Annealed.sigmaBar M n) (↑omega) n (n + ↑h) e' (closureNeumannAlong M n h K e' ↑omega)) 2 (HCPolySupport.normalizedCubeMeasure S)) (hmeasD : ∀ (i : ℕ), ∀ R' ∈ interiorMesoCubeGrid d (↑K) (nmesh - ↑i) (n - 1), Measurable fun (omega : Cutoff.CutoffSample d) => meshOscillationCell (nmesh - ↑i) (closureDirichletAlong M n h K e ↑omega).grad R') (hintD : ∀ (i : ℕ), ∀ R' ∈ interiorMesoCubeGrid d (↑K) (nmesh - ↑i) (n - 1), MeasureTheory.Integrable (fun (omega : Cutoff.CutoffSample d) => meshOscillationCell (nmesh - ↑i) (closureDirichletAlong M n h K e ↑omega).grad R' ^ 4) ↑(Cutoff.cutoffSampleLaw M)) (hmeasN : ∀ (i : ℕ), ∀ R' ∈ interiorMesoCubeGrid d (↑K) (nmesh - ↑i) (n - 1), Measurable fun (omega : Cutoff.CutoffSample d) => meshOscillationCell (nmesh - ↑i) (neumannFluxField (Annealed.sigmaBar M n) (↑omega) n (n + ↑h) e' (closureNeumannAlong M n h K e' ↑omega)) R') (hintN : ∀ (i : ℕ), ∀ R' ∈ interiorMesoCubeGrid d (↑K) (nmesh - ↑i) (n - 1), MeasureTheory.Integrable (fun (omega : Cutoff.CutoffSample d) => meshOscillationCell (nmesh - ↑i) (neumannFluxField (Annealed.sigmaBar M n) (↑omega) n (n + ↑h) e' (closureNeumannAlong M n h K e' ↑omega)) R' ^ 4) ↑(Cutoff.cutoffSampleLaw M)) (hdepthD : ∀ (i : ℕ), (gridFourthMomentRoot (↑(Cutoff.cutoffSampleLaw M)) (interiorMesoCubeGrid d (↑K) (nmesh - ↑i) (n - 1)) fun (R' : HCPolySupport.TriadicCube d) (omega : Cutoff.CutoffSample d) => meshOscillationCell (nmesh - ↑i) (closureDirichletAlong M n h K e ↑omega).grad R') ≤ 2 * ↑d * (M.gamma ^ 16 * ((1 + ↑i) * 3 ^ (-↑i)))) (hdepthN : ∀ (i : ℕ), (gridFourthMomentRoot (↑(Cutoff.cutoffSampleLaw M)) (interiorMesoCubeGrid d (↑K) (nmesh - ↑i) (n - 1)) fun (R' : HCPolySupport.TriadicCube d) (omega : Cutoff.CutoffSample d) => meshOscillationCell (nmesh - ↑i) (neumannFluxField (Annealed.sigmaBar M n) (↑omega) n (n + ↑h) e' (closureNeumannAlong M n h K e' ↑omega)) R') ≤ 2 * ↑d * (M.gamma ^ 16 * ((1 + ↑i) * 3 ^ (-↑i)))) : ∃ (Bg : HCPolySupport.TriadicCube d → Cutoff.CutoffSample d → ℝ), (∀ (R : HCPolySupport.TriadicCube d) (omega : Cutoff.CutoffSample d), 0 ≤ Bg R omega) ∧ (∀ R ∈ interiorMesoCubeGrid d (↑K) nmesh n, MeasureTheory.MemLp (Bg R) 4 ↑(Cutoff.cutoffSampleLaw M)) ∧ gridFourthMomentRoot (↑(Cutoff.cutoffSampleLaw M)) (interiorMesoCubeGrid d (↑K) nmesh n) Bg ≤ M.gamma ^ 15 ∧ ∀ R ∈ interiorMesoCubeGrid d (↑K) nmesh n, ∀ᵐ (omega : Cutoff.CutoffSample d) ∂↑(Cutoff.cutoffSampleLaw M), (∀ (N : ℕ), (HCPolySupport.cubeBesovPositiveVectorPartialSeminormTwo R gammaTenBesovExponent N fun (x : HCPolySupport.Vec d) => (CoarseEllipticity.blockGaugeUp (↑(Annealed.sigmaBar M (n + ↑h - 1))) ((localizationFz (Annealed.sigmaBar M n) (↑omega) n (n + ↑h) e' R (closureDirichletAlong M n h K e ↑omega) (closureNeumannAlong M n h K e' ↑omega)).eval x)).1) ≤ Bg R omega) ∧ ∀ (N : ℕ), (HCPolySupport.cubeBesovPositiveVectorPartialSeminormTwo R gammaTenBesovExponent N fun (x : HCPolySupport.Vec d) => (CoarseEllipticity.blockGaugeUp (↑(Annealed.sigmaBar M (n + ↑h - 1))) ((localizationFz (Annealed.sigmaBar M n) (↑omega) n (n + ↑h) e' R (closureDirichletAlong M n h K e ↑omega) (closureNeumannAlong M n h K e' ↑omega)).eval x)).2) ≤ Bg R omega

The body of ClosureInteriorBesovEnvelopeInput at one localization cube.

The two raw fields are the closure's own Dirichlet corrector gradient and Neumann flux field; the two gauged legs of bfF_z are their fixed scalar multiples, and the two scalars are capped by 4 . 3^9 under hgauge. So the two-leg envelope of Closure.GammaTenStripEnvelopeTwoLeg at A = 2 d, C_g = 4 . 3^9 is exactly what is wanted.

on the scale bookkeeping hKp, houter, hgp, hno, the boundary gate hsmall, hgamma0, the numerical threshold hthr, the gauge-ratio cap hgauge, the descendant-wise L^2 memberships hmemD, hmemN, the six cellwise typing binders and the two per-depth inputs.