LocalizationFluctuationOscillationBridge

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

The oscillation cell of e.nablaw.oscillations bounds the Besov depth term

Step 2 of l.approximate.recurrence.formula feeds e.lower.bound.oscillations into the duality leg, which is stated in the finite-depth positive q = 2 Besov seminorms of CoarseGraining's cubeBesovPositiveVectorPartialSeminormTwo. The two are written in different languages:

• the oscillation display carries meshOscillationCell n u R, the square root of Book.Ch01.meanSquareOscillationVecOn (openCubeAtScale (triadicCubeShift R) n) u -- the manuscript's ‖grad w - (grad w)_{z + cu_n}‖_{L2bar(z + cu_n)}, based at the cube's own site z;
• the Besov tower carries cubeBesovPositiveVectorDepthAverage, built from (cubeLpNorm R' (2) (cubeFluctuationVec R' u))^2 on the triadic descendants.

This module identifies the carriers and proves the (only) comparison the Step-2 chain needs. Two facts do the work.

1. openCubeAtScale_triadicCubeShift_eq_openCubeSet: at a cube's own scale, the site-based open window is the open cube -- an identity, not an inclusion.
2. sq_cubeLpNorm_two_cubeFluctuationVec_le_meanSquareOscillationVecOn: the two L^2 fluctuation quantities differ only by the ambient norm used, the CoarseGraining cubeLpNorm reading the Pi sup norm and meanSquareOscillationVecOn the coordinate sum. Since ‖v‖_infty^2 <= sum_k v_k^2 pointwise, the comparison holds with constant 1 in the direction Step 2 uses (the Besov seminorm is the smaller quantity), so no dimensional loss enters the fluctuation estimate.

The consequence cubeBesovPositiveVectorDepthAverage_le_descendantsAverage_sq is the form the multi-depth fold consumes: the depth-j term of the tower on a cube Q is at most the depth-j descendant average of the squared oscillation cells at scale Q.scale - j, which is exactly the quantity the free-buffer oscillation display bounds at buffer Q.scale - j.

Binders

hu, the L^2 membership of the field on the cube(s), is the standing integrability of every quantity in sight and is a conditional A obligation of this module, discharged by the caller from e.nablaw.in.L.eight. Nothing else is assumed: no smallness, no moment, no measurability and no sample-space proposition occurs.

Scope

There is no sorry.

References

• ABK26, e.nablaw.oscillations, e.lower.bound.oscillations, the duality leg of Step 2.

The site-based window is the cube

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.openCubeAtScale_triadicCubeShift_eq_openCubeSet {d : ℕ} (R : HCPolySupport.TriadicCube d) : HCPolySupport.Book.Ch03.openCubeAtScale (HCPolySupport.triadicCubeShift R) R.scale = HCPolySupport.openCubeSet R

At a cube's own scale the site-based open window is the open cube. Unconditional.

The two L^2 fluctuation quantities

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.norm_sq_le_vecNormSq {d : ℕ} (v : HCPolySupport.Vec d) : ‖v‖ ^ 2 ≤ HCPolySupport.vecNormSq v

The Pi sup norm is dominated by the coordinate L^2 norm.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.cubeAverageVec_eq_volumeAverageVec_openCubeSet {d : ℕ} (Q : HCPolySupport.TriadicCube d) (u : HCPolySupport.Vec d → HCPolySupport.Vec d) : HCPolySupport.cubeAverageVec Q u = HCPolySupport.volumeAverageVec (HCPolySupport.openCubeSet Q) u

The cube average of a vector field is its volume average over the open cube. Unconditional; the cube boundary is Lebesgue null.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.sq_cubeLpNorm_two_cubeFluctuationVec_le_meanSquareOscillationVecOn {d : ℕ} (Q : HCPolySupport.TriadicCube d) (u : HCPolySupport.Vec d → HCPolySupport.Vec d) (hu : MeasureTheory.MemLp u 2 (HCPolySupport.normalizedCubeMeasure Q)) : HCPolySupport.cubeLpNorm Q 2 (HCPolySupport.cubeFluctuationVec Q u) ^ 2 ≤ HCPolySupport.Book.Ch01.meanSquareOscillationVecOn (HCPolySupport.openCubeSet Q) u

The Besov depth term is below the oscillation cell. The squared L^2 cube norm of the fluctuation is at most the mean-square oscillation on the same cube, the comparison constant being 1.

on the L^2 membership hu.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.sq_cubeLpNorm_two_cubeFluctuationVec_le_sq_meshOscillationCell {d : ℕ} {n : ℤ} (Q : HCPolySupport.TriadicCube d) (hsc : Q.scale = n) (u : HCPolySupport.Vec d → HCPolySupport.Vec d) (hu : MeasureTheory.MemLp u 2 (HCPolySupport.normalizedCubeMeasure Q)) : HCPolySupport.cubeLpNorm Q 2 (HCPolySupport.cubeFluctuationVec Q u) ^ 2 ≤ meshOscillationCell n u Q ^ 2

The bridge at the display's own name. On a cube of scale n the Besov depth term is at most the square of the oscillation cell of e.nablaw.oscillations.

on the L^2 membership hu.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.cubeBesovPositiveVectorDepthAverage_le_descendantsAverage_sq {d : ℕ} (Q : HCPolySupport.TriadicCube d) (u : HCPolySupport.Vec d → HCPolySupport.Vec d) (j : ℕ) (hu : ∀ R ∈ HCPolySupport.descendantsAtDepth Q j, MeasureTheory.MemLp u 2 (HCPolySupport.normalizedCubeMeasure R)) : HCPolySupport.cubeBesovPositiveVectorDepthAverage Q u j ≤ HCPolySupport.descendantsAverage Q j fun (R : HCPolySupport.TriadicCube d) => meshOscillationCell (Q.scale - ↑j) u R ^ 2

The multi-depth form. The depth-j term of the positive q = 2 Besov tower on Q is at most the depth-j descendant average of the squared oscillation cells at scale Q.scale - j.

on the L^2 memberships on the descendants.