Step5InputOscillation

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

hmemOsc and hosc at the closure's Dirichlet family

Two of the residual legs of Closure.Step5Basket.step5GaugeEndpoint_closureFamilies_of_momentLegs are about the oscillation cell of e.nablaw.oscillations on the closure's grid:

• hmemOsc --- the cell is L^4 in the sample;
• hosc --- e.lower.bound.oscillations itself, in the re-sited shape exists_gamma0_freshShellDirichlet_step5MeshOscillationResited_le_gamma_pow_fifteen delivers.

Both come from a single pair, the octic grid envelope ApproximateRecurrence.exists_freshShellDirichlet_meshOscillation_memLp_and_eighthMoment_le. That producer quantifies its constant E before the threshold gamma0 and before the model, and the re-sited endpoint takes E as an argument and produces its own threshold; so the two compose in the only order that works: take E from the envelope, feed it to the endpoint, and take the smaller of the two thresholds. This module carries out that composition and discharges the envelope's six spatial side conditions at the closure's own Dirichlet family, all six being consequences of the single L^8 membership of the corrector gradient.

References

• ABK26, e.lower.bound.oscillations; e.nablaw.oscillations; e.nablaw.in.L.eight.

The two missing consequences of one L^8 membership

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.integrableOn_openCubeSet_coord_of_memLp_eight {d : ℕ} (Q : HCPolySupport.TriadicCube d) {u : HCPolySupport.Vec d → HCPolySupport.Vec d} (hu : MeasureTheory.MemLp u 8 (HCPolySupport.normalizedCubeMeasure Q)) (k : Fin d) : MeasureTheory.IntegrableOn (fun (x : HCPolySupport.Vec d) => u x k) (HCPolySupport.openCubeSet Q) MeasureTheory.volume

Each coordinate of grad w is integrable on cu_K.: on hu.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.integrableOn_openCubeSet_vecNormSq_pow_four_of_memLp_eight {d : ℕ} (Q : HCPolySupport.TriadicCube d) {u : HCPolySupport.Vec d → HCPolySupport.Vec d} (hu : MeasureTheory.MemLp u 8 (HCPolySupport.normalizedCubeMeasure Q)) : MeasureTheory.IntegrableOn (fun (x : HCPolySupport.Vec d) => HCPolySupport.vecNormSq (u x) ^ 4) (HCPolySupport.openCubeSet Q) MeasureTheory.volume

|grad w|^8 is integrable on cu_K.: on hu.

Measurability of the oscillation cell itself

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.measurable_meshOscillationCell_freshShellDirichletGrad {d : ℕ} [NeZero d] (Q : HCPolySupport.TriadicCube d) (sigmaInv : ℝ) (nsh msh : ℤ) (e : HCPolySupport.Vec d) {n : ℤ} (R : HCPolySupport.TriadicCube d) (hsc : R.scale = n) (hsub : HCPolySupport.openCubeSet R ⊆ HCPolySupport.openCubeSet Q) (wD : Cutoff.ShellSeq d → HCPolySupport.H10Function (HCPolySupport.openCubeSet Q)) (hsol : ∀ (omega : Cutoff.ShellSeq d), HCPolySupport.IsZeroTraceDirichletRhsWeakSolution (fun (x : HCPolySupport.Vec d) => 1) (HCPolySupport.openCubeSet Q) (wD omega) fun (x : HCPolySupport.Vec d) => -Corrector.streamForcing sigmaInv omega nsh msh e x) (hcoord : ∀ (omega : Cutoff.ShellSeq d) (k : Fin d), MeasureTheory.IntegrableOn (fun (x : HCPolySupport.Vec d) => (wD omega).grad x k) (HCPolySupport.openCubeSet R) MeasureTheory.volume) (hcoordsq : ∀ (omega : Cutoff.ShellSeq d) (k : Fin d), MeasureTheory.IntegrableOn (fun (x : HCPolySupport.Vec d) => (wD omega).grad x k ^ 2) (HCPolySupport.openCubeSet R) MeasureTheory.volume) : Measurable fun (omega : Cutoff.ShellSeq d) => meshOscillationCell n (wD omega).grad R

The oscillation cell of e.nablaw.oscillations is a measurable function of the sample: it is the fourth root of the measurable fourth power.

The composition: hmemOsc and hosc at the closure's Dirichlet family

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.exists_gamma0_step5OscillationLegs (d : ℕ) [NeZero d] (hd : 2 ≤ d) : ∃ (gamma0 : ℝ), 0 < gamma0 ∧ gamma0 ≤ 1 / 4 ∧ ∀ (M : ABKModel d), M.gamma ≤ gamma0 → ∀ (m0 : ℤ) (Eind : { Eb : ℝ // 1 ≤ Eb }), Frozen.Section3.inductionState M m0 Eind → ∀ (n : ℤ) (h K j : ℕ) (nmesh : ℤ), 0 < h → n ≤ m0 → ↑h ≤ 6 * Disorder.cstar M * M.gamma⁻¹ → 10 ^ 10 * M.gamma⁻¹ ≤ ↑↑K - ↑(n + ↑h) → nmesh = recurrenceMesoScale recurrenceGapMultiplier M.gamma (n + ↑h) ↑h → ↑j = ↑K - nmesh → ∀ (e : HCPolySupport.Vec d), HCPolySupport.Book.Ch02.vecNorm e ≤ 1 → (∀ R ∈ HCPolySupport.descendantsAtDepth (HCPolySupport.originCube d ↑K) j, MeasureTheory.MemLp (fun (omega : Cutoff.CutoffSample d) => meshOscillationCell nmesh (fun (x : HCPolySupport.Vec d) => (alongIncrementPath n h (closureDirichletFamily (↑(Annealed.sigmaBar M n))⁻¹ e K) ↑omega).grad x) R) 4 ↑(Cutoff.cutoffSampleLaw M)) ∧ ((gridFourthMomentRoot (↑(Cutoff.cutoffSampleLaw M)) (HCPolySupport.descendantsAtDepth (HCPolySupport.originCube d ↑K) j) fun (R : HCPolySupport.TriadicCube d) (omega : Cutoff.CutoffSample d) => meshOscillationCell nmesh (fun (x : HCPolySupport.Vec d) => (alongIncrementPath n h (closureDirichletFamily (↑(Annealed.sigmaBar M n))⁻¹ e K) ↑omega).grad x) R) + (↑(Annealed.sigmaBar M n))⁻¹ * gridFourthMomentRoot (↑(Cutoff.cutoffSampleLaw M)) (HCPolySupport.descendantsAtDepth (HCPolySupport.originCube d ↑K) j) fun (R : HCPolySupport.TriadicCube d) (omega : Cutoff.CutoffSample d) => 3 ^ ↑nmesh * shellDerivNormSum n (n + ↑h) (HCPolySupport.triadicCubeShift R) ↑omega) ≤ M.gamma ^ 15

hmemOsc and hosc, produced.

One threshold gamma0, produced before the model, such that in the manuscript's own parameter range the closure's Dirichlet family satisfies both oscillation legs of Step 5.

The composition is forced: the octic grid envelope produces its constant E before its own threshold and before the model, and the re-sited endpoint takes E as an argument; so E is taken first and the two thresholds are met at their minimum. The envelope's six spatial side conditions are discharged at the closure family from the single L^8 membership of the corrector gradient.

Proved from the ingredients listed in the module docstring.