JunctionDischargeStepFiveDisplay #

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

The Step-5 gauge junction: the averaged display and the endpoint #

ABK26, l.approximate.recurrence.formula, Step 5, together with e.what.nablaw.really.is and e.lower.bound.oscillations.

Closure.JunctionDischargeStepFive reduces Closure.Step5GaugeEndpoint to one binder, hdisplay:

  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 .

This module proves that display, and then the endpoint.

The three pieces of the display #

e.what.nablaw.really.is, proved here as cubeAverage_vecNormSq_grad_eq_shellPairing: the Dirichlet weak formulation of e.def.w tested with its own solution --- legitimate because IsZeroTraceDirichletRhsWeakSolution tests against all of H10Function U and the solution is one --- gives, with the identity coefficient field and the forcing g = -streamForcing shom_n^{-1} omega n (n+h) e,
```
  fint_{cu_K} |grad w_D|^2 = shom_n^{-1} fint_{cu_K} e . (h grad w_D) ,
```
the sign being fixed by the pointwise skew-symmetry of the fresh shell (Cutoff.finiteShellIncrement_skew), through vecDot_matVecMul_skew. This is the manuscript's own second equality in e.what.nablaw.really.is.
product of averages vs average of product. step5CrossDefect names the per-cube cost of replacing (h)_R (grad w_D)_R by (h grad w_D)_R, and descendantsAverage_shellPairing_eq is the exact tiling identity that carries it to the grid. The defect is charged to the two factors of e.lower.bound.oscillations by the binder hdefect, and the sum form of that endpoint is turned into the product the cross term produces by the Cauchy--Schwarz chain proved here: integral_rpow_two_le_rpow_integral_rpow_four (Lyapunov in the sample), integral_mul_le_rpowFourRoot_mul_rpowFourRoot (Cauchy--Schwarz in the sample, in the fourth-moment spelling), cubeFamilyAverage_rpowFourRoot_mul_le (Hoelder for the fourth roots on the grid) and cubeFamilyAverage_integral_mul_le_gridFourthMomentRoot_mul_root (the two combined, delivering exactly gridFourthMomentRoot against the gauge's own fourth-moment root). The final fold is crossOscillationFold, in the form
```
  2 sinv DD <= Cdef (2 A B) <= Cdef (A+B)^2/2
            <= (Cdef cgamma^15 / 2) cgamma^15 <= cgamma^15 ,
```
the last step being the gate hgate.
the quadratic error: Closure.shellProduct_le_quadratic_error instantiated at prod = avsum_ |(h)_R (grad w_D)_R|^2, Fend = * C2.

Carrier transports the caller must supply on `hosc` #

The proved Lean endpoint exists_gamma0_freshShellDirichlet_meshOscillation_le_gamma_pow_sixteen (LocalizationOscillationEndpointSixteen.lean) proves e.lower.bound.oscillations

on the interior meso grid interiorMesoCubeGrid, whereas the manuscript's display --- and Closure.Step5GaugeEndpoint, whose carrier is descendantsAtDepth (originCube d K) j --- averages over the full mesh. This is the known manuscript gap; closing it needs either the interior average or a boundary-strip argument; hosc is stated at the full mesh, i.e. faithfully to the source, and the transport from the interior endpoint is the remaining chain;
against the shell-sequence law M.P.toMeasure, whereas the closure's carrier is the cutoff sample law (cutoffSampleLaw M).toMeasure. The two are related by Cutoff.map_cutoffSampleLaw_val; the change of variables is the second remaining chain.

Neither transport is performed here, and neither is assumed away: both live inside the single binder hosc, which is the manuscript's own display.

References #

ABK26, e.lower.bound.pre2; the Step-5 estimate; e.what.nablaw.really.is; e.nablaw.oscillations; e.lower.bound.oscillations; e.km.kn.Lp; e.nablaw.in.L.eight.

`e.what.nablaw.really.is` #

source

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.vecDot_matVecMul_skew {d : ℕ} (A : HCPolySupport.Mat d) (hA : Matrix.transpose A = -A) (u v : HCPolySupport.Vec d) :

HCPolySupport.vecDot (HCPolySupport.matVecMul A u) v = -HCPolySupport.vecDot u (HCPolySupport.matVecMul A v)

Skew-symmetry moves a matrix across the dot product with a sign change.

source

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.cubeAverage_vecNormSq_grad_eq_shellPairing {d : ℕ} (Q : HCPolySupport.TriadicCube d) (c : ℝ) (omega : Cutoff.ShellSeq d) (n m : ℤ) (e : HCPolySupport.Vec d) (w : HCPolySupport.H10Function (HCPolySupport.openCubeSet Q)) (hw : HCPolySupport.IsZeroTraceDirichletRhsWeakSolution (fun (x : HCPolySupport.Vec d) => 1) (HCPolySupport.openCubeSet Q) w fun (x : HCPolySupport.Vec d) => -Corrector.streamForcing c omega n m e x) :

(HCPolySupport.cubeAverage Q fun (x : HCPolySupport.Vec d) => HCPolySupport.vecNormSq (w.grad x)) = c * HCPolySupport.cubeAverage Q fun (x : HCPolySupport.Vec d) => HCPolySupport.vecDot e (HCPolySupport.matVecMul ((Cutoff.finiteShellIncrement omega n m).toFun x) (w.grad x))

e.what.nablaw.really.is, Dirichlet leg.

The Cauchy--Schwarz step that feeds the fourth-moment endpoint #

source

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.integral_rpow_two_le_rpow_integral_rpow_four {Omega : Type u_1} [MeasurableSpace Omega] (mu : MeasureTheory.Measure Omega) [MeasureTheory.IsProbabilityMeasure mu] {X : Omega → ℝ} (hX : ∀ (omega : Omega), 0 ≤ X omega) (hXm : MeasureTheory.MemLp X 4 mu) :

∫ (omega : Omega), X omega ^ 2 ∂mu ≤ (∫ (omega : Omega), X omega ^ 4 ∂mu) ^ 2⁻¹

Lyapunov's inequality on a probability space, in the rpow spelling.

source

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.integral_mul_le_rpowFourRoot_mul_rpowFourRoot {Omega : Type u_1} [MeasurableSpace Omega] (mu : MeasureTheory.Measure Omega) [MeasureTheory.IsProbabilityMeasure mu] {X Y : Omega → ℝ} (hX : ∀ (omega : Omega), 0 ≤ X omega) (hY : ∀ (omega : Omega), 0 ≤ Y omega) (hXm : MeasureTheory.MemLp X 4 mu) (hYm : MeasureTheory.MemLp Y 4 mu) :

∫ (omega : Omega), X omega * Y omega ∂mu ≤ (∫ (omega : Omega), X omega ^ 4 ∂mu) ^ 4⁻¹ * (∫ (omega : Omega), Y omega ^ 4 ∂mu) ^ 4⁻¹

Cauchy--Schwarz in the sample, in the fourth-moment spelling.

source

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.sq_cubeFamilyAverage_le_cubeFamilyAverage_sq {d : ℕ} (I : Finset (HCPolySupport.TriadicCube d)) (F : HCPolySupport.TriadicCube d → ℝ) :

cubeFamilyAverage I F ^ 2 ≤ cubeFamilyAverage I fun (R : HCPolySupport.TriadicCube d) => F R ^ 2

Cauchy--Schwarz on a finite cube family.

The grid Cauchy--Schwarz for a per-cube second factor #

The one-sided step above is the shape the display needed while the forcing gauge of e.nablaw.oscillations was read at a single window z0. The gauge is sited at the cube's own base point, so the second factor of the cross term is itself a grid family, and the grid step must be Hoelder in both factors. The three lemmas below supply that.

source

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.cubeFamilyAverage_sqrt_le {d : ℕ} (I : Finset (HCPolySupport.TriadicCube d)) (G : HCPolySupport.TriadicCube d → ℝ) (hG : ∀ R ∈ I, 0 ≤ G R) :

(cubeFamilyAverage I fun (R : HCPolySupport.TriadicCube d) => G R ^ 2⁻¹) ≤ cubeFamilyAverage I G ^ 2⁻¹

Jensen for the concave square root, at the finite cube family.

source

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.sq_cubeFamilyAverage_mul_le {d : ℕ} (I : Finset (HCPolySupport.TriadicCube d)) (u v : HCPolySupport.TriadicCube d → ℝ) :

(cubeFamilyAverage I fun (R : HCPolySupport.TriadicCube d) => u R * v R) ^ 2 ≤ (cubeFamilyAverage I fun (R : HCPolySupport.TriadicCube d) => u R ^ 2) * cubeFamilyAverage I fun (R : HCPolySupport.TriadicCube d) => v R ^ 2

Cauchy--Schwarz for the finite cube-family average.

source

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.cubeFamilyAverage_rpowFourRoot_mul_le {d : ℕ} (I : Finset (HCPolySupport.TriadicCube d)) (a b : HCPolySupport.TriadicCube d → ℝ) (ha : ∀ R ∈ I, 0 ≤ a R) (hb : ∀ R ∈ I, 0 ≤ b R) :

(cubeFamilyAverage I fun (R : HCPolySupport.TriadicCube d) => a R ^ 4⁻¹ * b R ^ 4⁻¹) ≤ cubeFamilyAverage I a ^ 4⁻¹ * cubeFamilyAverage I b ^ 4⁻¹

Hoelder on the grid at a pair of fourth roots.

source

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.cubeFamilyAverage_integral_mul_le_gridFourthMomentRoot_mul_root {d : ℕ} {Omega : Type u_1} [MeasurableSpace Omega] (mu : MeasureTheory.Measure Omega) [MeasureTheory.IsProbabilityMeasure mu] (I : Finset (HCPolySupport.TriadicCube d)) (X Y : HCPolySupport.TriadicCube d → Omega → ℝ) (hX : ∀ (R : HCPolySupport.TriadicCube d) (omega : Omega), 0 ≤ X R omega) (hY : ∀ (R : HCPolySupport.TriadicCube d) (omega : Omega), 0 ≤ Y R omega) (hXm : ∀ R ∈ I, MeasureTheory.MemLp (X R) 4 mu) (hYm : ∀ R ∈ I, MeasureTheory.MemLp (Y R) 4 mu) :

(cubeFamilyAverage I fun (R : HCPolySupport.TriadicCube d) => ∫ (omega : Omega), X R omega * Y R omega ∂mu) ≤ gridFourthMomentRoot mu I X * gridFourthMomentRoot mu I Y

The two-sided grid/sample Cauchy--Schwarz that feeds the re-sited e.lower.bound.oscillations.

The per-cube cross defect and the grid identity #

source

noncomputable def Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.step5CrossDefect {d : ℕ} (R : HCPolySupport.TriadicCube d) (omega : Cutoff.ShellSeq d) (n m : ℤ) (e : HCPolySupport.Vec d) (u : HCPolySupport.Vec d → HCPolySupport.Vec d) :

ℝ

The Step-5 per-cube cross defect: the cube average of the product h grad w, tested against e, minus the product of the two cube averages. It is the entire cost of replacing (h)_R (grad w)_R by (h grad w)_R.

Equations

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

Instances For

source

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.descendantsAverage_shellPairing_eq {d : ℕ} (Q : HCPolySupport.TriadicCube d) (j : ℕ) (omega : Cutoff.ShellSeq d) (n m : ℤ) (e : HCPolySupport.Vec d) (u : HCPolySupport.Vec d → HCPolySupport.Vec d) (hint : MeasureTheory.IntegrableOn (fun (x : HCPolySupport.Vec d) => HCPolySupport.vecDot e (HCPolySupport.matVecMul ((Cutoff.finiteShellIncrement omega n m).toFun x) (u x))) (HCPolySupport.cubeSet Q) MeasureTheory.volume) :

(HCPolySupport.descendantsAverage Q j fun (R : HCPolySupport.TriadicCube d) => HCPolySupport.vecDot e (HCPolySupport.matVecMul (freshShellCubeAverage R omega n m) (HCPolySupport.cubeAverageVec R u))) = (HCPolySupport.cubeAverage Q fun (x : HCPolySupport.Vec d) => HCPolySupport.vecDot e (HCPolySupport.matVecMul ((Cutoff.finiteShellIncrement omega n m).toFun x) (u x))) - HCPolySupport.descendantsAverage Q j fun (R : HCPolySupport.TriadicCube d) => step5CrossDefect R omega n m e u

The grid form of the cross term: the descendant average of the products of the averages is the cube average of the product, minus the grid average of the defects. This is the exact tiling bookkeeping.

The fourth-root gauge normalization #

The two arithmetic folds of the display #

The four legs of the averaged display #

The averaged Step-5 display #

source

(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 + C1 * C2 * ↑h ^ 2 * (↑(Annealed.sigmaBar M n) ^ 4)⁻¹ * 3 ^ (4 * M.gamma * ↑(n + ↑h)) + M.gamma ^ 15

The averaged Step-5 display, at the closure's grid carrier and the finite localization cube. This is exactly the binder hdisplay of step5GaugeEndpoint_of_cellDisplay.

The endpoint #

source

Step5GaugeEndpoint M n h K j e (C1 * C2) wD wN

Closure.Step5GaugeEndpoint, from the two correctors and the named legs, at a per-cube forcing gauge. This is the Step-5 mirror of Closure.JunctionDischargeStepFour.step4GaugeEndpoint_of_correctors.

The gauge family gauge R omega is the right factor of e.nablaw.oscillations read at the cube R's own base point; the producer instantiates it at `3^nmesh

shellDerivNormSum n (n+h) (triadicCubeShift R) omega`.

Documentation

LeanPool.Superdiffusion.Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.JunctionDischargeStepFiveDisplay

JunctionDischargeStepFiveDisplay #

The Step-5 gauge junction: the averaged display and the endpoint #

The three pieces of the display #

Carrier transports the caller must supply on `hosc` #

References #

`e.what.nablaw.really.is` #

The Cauchy--Schwarz step that feeds the fourth-moment endpoint #

The grid Cauchy--Schwarz for a per-cube second factor #

The per-cube cross defect and the grid identity #

The fourth-root gauge normalization #

The two arithmetic folds of the display #

The four legs of the averaged display #

The averaged Step-5 display #

The endpoint #

JunctionDischargeStepFiveDisplay #

The Step-5 gauge junction: the averaged display and the endpoint #

The three pieces of the display #

Carrier transports the caller must supply on hosc #

References #

e.what.nablaw.really.is #

The Cauchy--Schwarz step that feeds the fourth-moment endpoint #

The grid Cauchy--Schwarz for a per-cube second factor #

The per-cube cross defect and the grid identity #

The fourth-root gauge normalization #

The two arithmetic folds of the display #

The four legs of the averaged display #

The averaged Step-5 display #

The endpoint #

Carrier transports the caller must supply on `hosc` #

`e.what.nablaw.really.is` #