GammaTenInteriorMinkowski

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

The oscillation cell is subadditive, and the flux leg splits

ABK26, e.nablaw.oscillations, e.Fz.def, 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' ,

so the oscillation input of Step 2 at the flux leg has to be read at a sum. Closure.GammaTenDepthStreamForcing.meshOscillationCell_streamForcing_le bounds the second summand; what is missing is the triangle inequality that lets the two be added, at the oscillation (mean-subtracted) cell rather than at the deviation from a fixed constant.

What is proved

• volumeAverageVec_add --- linearity of the vector volume average.
• sqrt_meanSquareOscillationVecOn_add_le_of_memVectorL2 --- the triangle inequality for the mean-square oscillation, from the proved deviation form Corrector.HarmonicReplaceMinkowski.sqrt_meanSquareDeviationVecOn_add_le_of_memVectorL2 read at the two fields' own averages. Only the two L^2 memberships are assumed: no continuity is required of either summand.
• meshOscillationCell_add_le --- the same at the mesh cell of e.nablaw.oscillations.
• meshOscillationCell_neumannFluxField_le --- the flux-leg split: the oscillation cell of the Neumann flux field is the oscillation cell of grad w_N plus the deterministic shell-derivative term of the forcing.

Binders

The two L^2 memberships on the oscillation cube, 0 <= sigmaInv and the scale gate n <= lowScale of the forcing bound. No smallness gate, no model, no probability and no corrector estimate 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, e.nablaw.oscillations, e.Fz.def, e.def.w, e.W.1.inf.bound.

Linearity of the vector volume average

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.integrableOn_coord_of_memVectorL2 {d : ℕ} {V : Set (HCPolySupport.Vec d)} [MeasureTheory.IsFiniteMeasure (HCPolySupport.volumeMeasureOn V)] {f : HCPolySupport.Vec d → HCPolySupport.Vec d} (hf : HCPolySupport.MemVectorL2 V f) (k : Fin d) : MeasureTheory.IntegrableOn (fun (x : HCPolySupport.Vec d) => f x k) V MeasureTheory.volume

Coordinates of an L^2 vector field on a finite-measure set are integrable.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.volumeAverageVec_add {d : ℕ} {V : Set (HCPolySupport.Vec d)} {f g : HCPolySupport.Vec d → HCPolySupport.Vec d} (hf : ∀ (k : Fin d), MeasureTheory.IntegrableOn (fun (x : HCPolySupport.Vec d) => f x k) V MeasureTheory.volume) (hg : ∀ (k : Fin d), MeasureTheory.IntegrableOn (fun (x : HCPolySupport.Vec d) => g x k) V MeasureTheory.volume) : (HCPolySupport.volumeAverageVec V fun (x : HCPolySupport.Vec d) => f x + g x) = HCPolySupport.volumeAverageVec V f + HCPolySupport.volumeAverageVec V g

Linearity of the vector volume average. Conditional only on coordinatewise integrability.

The triangle inequality at the mean-square oscillation

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.sqrt_meanSquareOscillationVecOn_add_le_of_memVectorL2 {d : ℕ} {V : Set (HCPolySupport.Vec d)} [MeasureTheory.IsFiniteMeasure (HCPolySupport.volumeMeasureOn V)] {f g : HCPolySupport.Vec d → HCPolySupport.Vec d} (hf : HCPolySupport.MemVectorL2 V f) (hg : HCPolySupport.MemVectorL2 V g) : √(HCPolySupport.Book.Ch01.meanSquareOscillationVecOn V fun (x : HCPolySupport.Vec d) => f x + g x) ≤ √(HCPolySupport.Book.Ch01.meanSquareOscillationVecOn V f) + √(HCPolySupport.Book.Ch01.meanSquareOscillationVecOn V g)

The triangle inequality for the mean-square oscillation of L^2 fields.

|| (f + g) - avg (f + g) ||_{L2bar(V)} <= || f - avg f ||_{L2bar(V)} + || g - avg g ||_{L2bar(V)} on any finite-measure set, with no continuity hypothesis.

only on the two L^2 memberships.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.meshOscillationCell_add_le {d : ℕ} (n : ℤ) {f g : HCPolySupport.Vec d → HCPolySupport.Vec d} (R : HCPolySupport.TriadicCube d) (hf : HCPolySupport.MemVectorL2 (HCPolySupport.Book.Ch03.openCubeAtScale (HCPolySupport.triadicCubeShift R) n) f) (hg : HCPolySupport.MemVectorL2 (HCPolySupport.Book.Ch03.openCubeAtScale (HCPolySupport.triadicCubeShift R) n) g) : meshOscillationCell n (fun (x : HCPolySupport.Vec d) => f x + g x) R ≤ meshOscillationCell n f R + meshOscillationCell n g R

The oscillation cell of e.nablaw.oscillations is subadditive.

only on the two L^2 memberships on the oscillation cube.

The flux leg

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.meshOscillationCell_neumannFluxField_le {d : ℕ} {sigma : Observable.PositiveScalar} (omega : Cutoff.ShellSeq d) (lowScale highScale : ℤ) (e' : HCPolySupport.Vec d) {Qc : HCPolySupport.TriadicCube d} (wN : HCPolySupport.H1MeanZeroFunction (HCPolySupport.openCubeSet Qc)) (n : ℤ) (hn : n ≤ lowScale) (R : HCPolySupport.TriadicCube d) (hgrad : HCPolySupport.MemVectorL2 (HCPolySupport.Book.Ch03.openCubeAtScale (HCPolySupport.triadicCubeShift R) n) wN.toH1Function.grad) (hforce : HCPolySupport.MemVectorL2 (HCPolySupport.Book.Ch03.openCubeAtScale (HCPolySupport.triadicCubeShift R) n) (Corrector.streamForcing (↑sigma)⁻¹ omega lowScale highScale e')) : meshOscillationCell n (neumannFluxField sigma omega lowScale highScale e' wN) R ≤ meshOscillationCell n wN.toH1Function.grad R + 3 ^ n * ((↑sigma)⁻¹ * ↑d * HCPolySupport.Book.Ch02.vecNorm e' * shellDerivNormSum lowScale highScale (HCPolySupport.triadicCubeShift R) omega)

The oscillation cell of the Neumann flux field splits.

  osc_n (neumannFluxField sigma omega lo hi e' wN) (R)
    <=  osc_n (grad w_N) (R)
        + 3^n . sigma^{-1} . d . |e'|_2 . shellDerivNormSum lo hi z_R omega .

The second summand is the proved deterministic bound Closure.GammaTenDepthStreamForcing.meshOscillationCell_streamForcing_le; the dimensional factor there is d, not sqrt d, and it is not absorbed here.

on the two L^2 memberships on the oscillation cube, on 0 <= sigma^{-1} and on the scale gate n <= lowScale.