GammaTenDepthStreamForcing #

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

The oscillation cell of the fresh-shell forcing itself #

ABK26, e.nablaw.oscillations, e.def.w.

Why this is needed #

The Neumann leg of bfF_z is not the Neumann corrector's gradient: by PrincipalResponsePz.neumannFluxField it is

  neumannFluxField sigma omega lo hi e' wN
    = wN.grad + streamForcing sigma^{-1} omega lo hi e' ,

and the proved oscillation display of LocalizationOscillationDisplay bounds the oscillation of the gradient only. The second summand is a deterministic C^1 field, so its oscillation on a cube of scale n is controlled by the cube side 3^n times the sup of its differential --- and that differential is exactly the shell-derivative gauge shellDerivNormSum in which the display's own forcing term is already written.

What is proved #

openCubeAtScale_subset_of_le --- concentric open cubes are monotone in the scale.
meshOscillationCell_streamForcing_le --- the bound: for n <= lowScale,
```
  meshOscillationCell n (streamForcing sigmaInv omega lo hi e') R
    <=  3^n * (sigmaInv * d * |e'|_2 *
          shellDerivNormSum lo hi (triadicCubeShift R) omega) .
```
The dimensional factor is d, not sqrt d: one sqrt d is the sup-to-Euclidean conversion on the input of the coordinate differential (StreamForcingDeriv.norm_fderiv_streamForcing_coord_le) and the second is the coordinate-sum of the mean-square deviation (OscillationApproxForcing.sqrt_meanSquareOscillationVecOn_le_of_norm_fderiv_le). Neither is absorbed.

Binders #

0 <= sigmaInv and the scale gate n <= lowScale, which is what makes the shell-derivative gauge --- read on z + cu_{lowScale} --- a majorant on the oscillation cube z + cu_n. No model, no probability, no corrector and no smallness gate occurs; the statement is deterministic pointwise calculus about the forcing.

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, e.nablaw.oscillations, e.def.w, e.W.1.inf.bound.

source

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.openCubeAtScale_subset_of_le {d : ℕ} (z : HCPolySupport.Vec d) {n ell : ℤ} (h : n ≤ ell) :

HCPolySupport.Book.Ch03.openCubeAtScale z n ⊆ HCPolySupport.Book.Ch03.openCubeAtScale z ell

Concentric open cubes are monotone in the scale. Unconditional.

source

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.meshOscillationCell_streamForcing_le {d : ℕ} {sigmaInv : ℝ} (hsigma : 0 ≤ sigmaInv) (omega : Cutoff.ShellSeq d) (lowScale highScale : ℤ) (e' : HCPolySupport.Vec d) (n : ℤ) (hn : n ≤ lowScale) (R : HCPolySupport.TriadicCube d) :

meshOscillationCell n (Corrector.streamForcing sigmaInv omega lowScale highScale e') R ≤ 3 ^ n * (sigmaInv * ↑d * HCPolySupport.Book.Ch02.vecNorm e' * shellDerivNormSum lowScale highScale (HCPolySupport.triadicCubeShift R) omega)

The oscillation cell of the fresh-shell forcing.

On the cube z + cu_n based at the cell's own site z = triadicCubeShift R, the normalized L^2 oscillation of streamForcing sigmaInv omega lo hi e' is at most the cube side 3^n times sigmaInv * d * |e'|_2 times the summed first-derivative shell gauges of e.W.1.inf.bound read at base point z.

only on 0 <= sigmaInv and on n <= lowScale, which puts the oscillation cube inside the cube on which the gauge is read.

Documentation