JunctionDischargeStepFive

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

The Step-5 gauge junction: the per-cube expansion and the grid assembly

This module carries Closure.Step5GaugeEndpoint --- the finite-K form of e.lower.bound.pre2 --- down to the one display the manuscript's Step 5 actually argues about, and discharges everything else.

What is proved here

At the Step-6 branch e' = 0 and |e| = 1, the Neumann forcing -streamForcing shom_n^{-1} omega n (n+h) 0 vanishes identically, so the Neumann corrector's gradient is a.e. 0 on cu_K and its average over every descendant cube vanishes. The gauge collapse (ClosureGaugeCollapse.blockVecDot_gaugedPrincipalLoadShell_blockDiag_flux) then gives, per cube and per sample, the manuscript's own four-term display

  | Ahom^{1/2} G_{-(h)_R} Ahom^{-1/2} P_R |^2
    = |e|^2 + |(grad w_D^{(K)})_R|^2
      + shom^{-2} |(h)_R (grad w_D^{(K)})_R|^2
      - 2 shom^{-1} e . (h)_R (grad w_D^{(K)})_R
    = 1 + step5CellExcess ,

which is blockVecDot_gaugedPrincipalLoadShell_blockDiag_flux_expand. Averaging over the descendant grid and integrating in the sample then reduces the endpoint to a single inequality about step5CellExcess, which is step5GaugeEndpoint_of_cellDisplay.

What is charged forward: the binder hdisplay

hdisplay is exactly the manuscript's remaining Step-5 content, namely the two displays combined:

  avsum_R E[ step5CellExcess ]
    <= - E|| grad w_D^{(K)} ||^2_{L2(cu_K)}
       + Fend h^2 shom_n^{-4} 3^{4 cgamma (n+h)} + cgamma^15 .

Its two halves have named producers, neither of which is proved at the grid carrier yet:

• the energy identity e.what.nablaw.really.is, || grad w_D^{(K)} ||^2 = shom^{-1} avg_{cu_K} e. (h) grad w_D^{(K)}, obtained by testing e.def.w with its own solution. It converts the cross term -2 shom^{-1} avsum_[e. (h)_R (grad w_D)_R] into -2 E||grad w_D||^2, up to the difference between the product of the averages (h)_R (grad w_D)_R and the average of the product (h grad w_D)_R;
• that difference, together with Jensen for avsum_|(grad w_D)_R|^2 <= E||grad w_D||^2, is the cgamma^15 oscillation remainder e.lower.bound.oscillations, whose proved endpoint is exists_gamma0_freshShellDirichlet_step5MeshOscillation_le_gamma_pow_fifteen (stated as a fourth-moment mesh oscillation, so a Cauchy--Schwarz step is still needed to feed it in here);
• the positive term shom^{-2} avsum_|(h)_R (grad w_D)_R|^2 is bounded by Fend h^2 shom_n^{-4} 3^{4 cgamma (n+h)} through Closure.shellProduct_le_quadratic_error on l.km.kn.Lp and e.nablaw.in.L.eight.

hsampR is the sample integrability of the per-cube excess; its producer is Corrector.CorrectorMeasurableGradient together with the moment bounds above.

References

• ABK26, e.lower.bound.pre2; e.what.nablaw.really.is; e.lower.bound.oscillations.

Vector algebra

The Step-5 per-cube excess

noncomputable def Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.step5CellExcess {d : ℕ} (sigma : Observable.PositiveScalar) {Q : HCPolySupport.TriadicCube d} (R : HCPolySupport.TriadicCube d) (n m : ℤ) (e : HCPolySupport.Vec d) (wD : Cutoff.ShellSeq d → HCPolySupport.H10Function (HCPolySupport.openCubeSet Q)) (omega : Cutoff.ShellSeq d) : ℝ

The three non-constant terms of the Step-5 per-cube display:

  |(grad w_D)_R|^2 - 2 shom^{-1} e . (h)_R (grad w_D)_R
    + shom^{-2} |(h)_R (grad w_D)_R|^2 .

This is what remains of the gauged doubled quadratic form at the Step-6 branch e' = 0 and |e| = 1, after the constant |e|^2 = 1.

Equations

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

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.blockVecDot_gaugedPrincipalLoadShell_blockDiag_flux_expand {d : ℕ} (sigma : Observable.PositiveScalar) {Q : HCPolySupport.TriadicCube d} (R : HCPolySupport.TriadicCube d) (n m : ℤ) {e : HCPolySupport.Vec d} (he : HCPolySupport.vecNormSq e = 1) (wD : Cutoff.ShellSeq d → HCPolySupport.H10Function (HCPolySupport.openCubeSet Q)) (wN : Cutoff.ShellSeq d → HCPolySupport.H1MeanZeroFunction (HCPolySupport.openCubeSet Q)) (omega : Cutoff.ShellSeq d) (hzeroN : (HCPolySupport.cubeAverageVec R fun (x : HCPolySupport.Vec d) => (wN omega).toH1Function.grad x) = 0) : HCPolySupport.blockVecDot (gaugedPrincipalLoadShell sigma R n m e 0 wD wN omega) (HCPolySupport.blockMatVecMul (HCPolySupport.Book.Ch02.blockDiag (↑sigma • 1) ((↑sigma)⁻¹ • 1)) (gaugedPrincipalLoadShell sigma R n m e 0 wD wN omega)) = 1 + step5CellExcess sigma R n m e wD omega

The per-cube collapse at the Step-5 branch, expanded.

At e' = 0 the Neumann forcing vanishes, so (grad w_N)_R = 0; the gauged doubled quadratic form is then 1 + step5CellExcess, which is exactly the manuscript's four-term display.

The endpoint, from the averaged display

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.step5GaugeEndpoint_of_cellDisplay {d : ℕ} (M : ABKModel d) (n : ℤ) (h K j : ℕ) {e : HCPolySupport.Vec d} (he : HCPolySupport.vecNormSq e = 1) (Fend : ℝ) (wD : C(HCPolySupport.Vec d, HCPolySupport.Mat d) → HCPolySupport.H10Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d ↑K))) (wN : C(HCPolySupport.Vec d, HCPolySupport.Mat d) → HCPolySupport.H1MeanZeroFunction (HCPolySupport.openCubeSet (HCPolySupport.originCube d ↑K))) (hN : ∀ (omega : Cutoff.ShellSeq d), HCPolySupport.IsMeanZeroNeumannRhsWeakSolution (fun (x : HCPolySupport.Vec d) => 1) (HCPolySupport.openCubeSet (HCPolySupport.originCube d ↑K)) (alongIncrementPath n h wN omega) fun (x : HCPolySupport.Vec d) => -Corrector.streamForcing (↑(Annealed.sigmaBar M n))⁻¹ omega n (n + ↑h) 0 x) (hsampR : ∀ R ∈ HCPolySupport.descendantsAtDepth (HCPolySupport.originCube d ↑K) j, MeasureTheory.Integrable (fun (omega : Cutoff.CutoffSample d) => step5CellExcess (Annealed.sigmaBar M n) R n (n + ↑h) e (alongIncrementPath n h wD) ↑omega) ↑(Cutoff.cutoffSampleLaw M)) (hdisplay : (HCPolySupport.descendantsAverage (HCPolySupport.originCube d ↑K) j fun (R : HCPolySupport.TriadicCube d) => ∫ (omega : Cutoff.CutoffSample d), step5CellExcess (Annealed.sigmaBar M n) R n (n + ↑h) e (alongIncrementPath n h wD) ↑omega ∂↑(Cutoff.cutoffSampleLaw M)) ≤ -dirichletCubeEnergy M n h K wD + Fend * ↑h ^ 2 * (↑(Annealed.sigmaBar M n) ^ 4)⁻¹ * 3 ^ (4 * M.gamma * ↑(n + ↑h)) + M.gamma ^ 15) : Step5GaugeEndpoint M n h K j e Fend wD wN

Closure.Step5GaugeEndpoint from the manuscript's averaged Step-5 display.

hdisplay is the conjunction of the two displays --- the oscillation replacement of (h)_R (grad w_D)_R by (h grad w_D)_R and the Hoelder product of Closure.shellProduct_le_quadratic_error --- stated at the grid carrier the closure consumes and at the finite localization cube. hN is e.def.w, Neumann leg, read at the Step-6 branch direction e' = 0; hsampR is the sample integrability of the per-cube excess.

Everything else --- the gauge collapse, the vanishing of the Neumann corrector at the zero direction, the expansion into the manuscript's four terms and the grid arithmetic --- is discharged here.