LocalizationEnvelopeMesh

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

NOTE: this module is an ordinary Provider helper / conditional A. The binder descriptions below are an informal inventory only.

Provider: the meso-window energy primitives, on a small cone

Source displays in ABK26:

• e.lower.bound.oscillations (label; display);
• e.nablaw.oscillations (label; display, claim opened);
• e.nablaw.in.L.eight (label; display).

Why this module exists

The window energy ‖grad w‖_{L2bar(z + cu_{m-h})} that e.nablaw.oscillations puts on its right-hand side is a low-level quantity: a normalized L^2 deviation on one translated triadic cube. In the development it was first written down inside LocalizationOscillationDisplay, a module that also carries the whole assembly and therefore drags in the nested Campanato tower, the harmonic-approximation layer and the shell-derivative gauge. Any consumer that needs only the low-level quantity pays for all of it.

This module re-states the three low-level carriers from first principles on the CoarseGraining cube/volumeAverage A, and re-derives the covering discharge on top of them, so that the discharge sits on a cone consisting of exactly LocalizationGrid, Corrector.OscillationCubeFamily, LocalizationOverlapCount, LocalizationOverlapTransfer, LocalizationOscillationTail and LocalizationOscillationGridMoment.

The carriers are definitionally equal to the ones in LocalizationOscillationDisplay and LocalizationOverlapCoarse (mesoWindowEnergy = meshEnergyCell, mesoWindowFourthEnergy = meshFourthEnergyCell, originCubeFourthEnergy = cubeFourthEnergy, each by rfl); the equalities are recorded in the separate bridge module, which is the only place where the large cone is paid for.

What is proved

• mesoWindowEnergy, mesoWindowFourthEnergy, originCubeFourthEnergy -- the window energy ‖u‖_{L2bar(z+cu_ell)}, the window fourth energy fint_{z+cu_ell} |u|^4, and the global fourth energy fint_{cu_K} |u|^4, the last two written with CoarseGraining's vecNormSq so that originCubeFourthEnergy K u is exactly ‖u‖_{L4bar(cu_K)}^4 in the manuscript's normalization.
• mesoWindowEnergy_rpow_four_le -- the per-window Jensen step ‖u‖^4_{L2bar(W)} <= fint_W |u|^4, with constant 1.
• gridFourthMoment_mesoWindowEnergy_le -- the covering discharge. The grid fourth moment of the window energies over the interior meso grid is at most 3^d times the annealed global fourth energy on cu_K. The overlap multiplicity 3^{dN} of LocalizationOverlapCount cancels exactly against the window volume; the surviving 3^d is the interior-grid deficit of card_mesoCubeGrid_le_three_pow_mul_card_interior. Restating it with the amplitude (3^d E)^{1/4}, in the shape a display binder has, is left to the consumer.

What is NOT proved here

• The envelope is still a binder in this module. henv asks for int_Omega fint_{cu_K} |u|^4 <= E; deriving it from the manuscript's e.nablaw.in.L.eight is the business of the companion modules LocalizationEnvelopeSpatial, LocalizationEnvelopeMoment and LocalizationEnvelopeHenv, and is not attempted below.
• No integrability or measurability side condition is discharged. Fourth power integrability on cu_K in space, and integrability in the sample of the window and global fourth energies, are binders.

Divergences from the printed statement

• The Jensen step is at p = 2, not Minkowski. ‖u‖^4_{L2bar(W)} is bounded by fint_W |u|^4 with constant 1; this is normalized Cauchy--Schwarz and no constant is lost.

References

• ABK26, e.lower.bound.oscillations; e.nablaw.oscillations; e.nablaw.in.L.eight.

The three low-level carriers

noncomputable def Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.mesoWindowEnergy {d : ℕ} (ell : ℤ) (u : HCPolySupport.Vec d → HCPolySupport.Vec d) (R : HCPolySupport.TriadicCube d) : ℝ

The window energy of e.nablaw.oscillations: the normalized L^2 size of u on the meso window z + cu_ell based at the site z = triadicCubeShift R, i.e. ‖u‖_{L2bar(z+cu_ell)}.

This is definitionally LocalizationOscillationDisplay.meshEnergyCell.

Equations

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

noncomputable def Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.mesoWindowFourthEnergy {d : ℕ} (ell : ℤ) (u : HCPolySupport.Vec d → HCPolySupport.Vec d) (R : HCPolySupport.TriadicCube d) : ℝ

The normalized fourth energy of u on the meso window z + cu_ell: fint_{z+cu_ell} |u|^4.

This is definitionally LocalizationOverlapCoarse.meshFourthEnergyCell.

Equations

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

noncomputable def Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.originCubeFourthEnergy {d : ℕ} (K : ℤ) (u : HCPolySupport.Vec d → HCPolySupport.Vec d) : ℝ

The normalized fourth energy of u on cu_K: fint_{cu_K} |u|^4, i.e. ‖u‖_{L4bar(cu_K)}^4 in the manuscript's normalization.

This is definitionally LocalizationOverlapCoarse.cubeFourthEnergy.

Equations

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

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.mesoWindowFourthEnergy_nonneg {d : ℕ} (ell : ℤ) (u : HCPolySupport.Vec d → HCPolySupport.Vec d) (R : HCPolySupport.TriadicCube d) : 0 ≤ mesoWindowFourthEnergy ell u R

Unconditional: the window fourth energy is nonnegative.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.originCubeFourthEnergy_nonneg {d : ℕ} (K : ℤ) (u : HCPolySupport.Vec d → HCPolySupport.Vec d) : 0 ≤ originCubeFourthEnergy K u

Unconditional: the global fourth energy is nonnegative.

Cauchy--Schwarz against the constant, re-derived

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.sq_setIntegral_le_volume_mul_setIntegral_sq {d : ℕ} {V : Set (HCPolySupport.Vec d)} (hfin : MeasureTheory.volume V ≠ ⊤) (hpos : 0 < (MeasureTheory.volume V).toReal) {g : HCPolySupport.Vec d → ℝ} (hg : MeasureTheory.IntegrableOn g V MeasureTheory.volume) (hg2 : MeasureTheory.IntegrableOn (fun (x : HCPolySupport.Vec d) => g x ^ 2) V MeasureTheory.volume) : (∫ (x : HCPolySupport.Vec d) in V, g x) ^ 2 ≤ (MeasureTheory.volume V).toReal * ∫ (x : HCPolySupport.Vec d) in V, g x ^ 2

Cauchy--Schwarz against 1 on a finite-measure set: (int_V g)^2 <= |V| int_V g^2.

: the caller supplies hfin : volume V ≠ ⊤, hpos : 0 < (volume V).toReal, and the two integrability hypotheses hg, hg2.

The per-window Jensen step

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.mesoWindowEnergy_rpow_four_le {d : ℕ} (ell : ℤ) (u : HCPolySupport.Vec d → HCPolySupport.Vec d) (R : HCPolySupport.TriadicCube d) (hcoord : ∀ (k : Fin d), MeasureTheory.IntegrableOn (fun (x : HCPolySupport.Vec d) => u x k ^ 2) (HCPolySupport.Book.Ch03.openCubeAtScale (HCPolySupport.triadicCubeShift R) ell) MeasureTheory.volume) (hsq : MeasureTheory.IntegrableOn (fun (x : HCPolySupport.Vec d) => HCPolySupport.vecNormSq (u x)) (HCPolySupport.Book.Ch03.openCubeAtScale (HCPolySupport.triadicCubeShift R) ell) MeasureTheory.volume) (hfour : MeasureTheory.IntegrableOn (fun (x : HCPolySupport.Vec d) => HCPolySupport.vecNormSq (u x) ^ 2) (HCPolySupport.Book.Ch03.openCubeAtScale (HCPolySupport.triadicCubeShift R) ell) MeasureTheory.volume) : mesoWindowEnergy ell u R ^ 4 ≤ mesoWindowFourthEnergy ell u R

The per-window Jensen step. The fourth power of the window energy ‖u‖_{L2bar(z+cu_ell)} is at most the window's normalized fourth energy. The constant is 1.

: the caller supplies hcoord, integrability on the window of the coordinate squares of u; hsq, integrability on the window of |u|^2 = vecNormSq o u; and hfour, integrability on the window of |u|^4 = (vecNormSq o u)^2. No other hypothesis is used.

The window containment supplied by the interior grid

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.openCubeAtScale_subset_openCubeSet_of_mem_interiorMesoCubeGrid {d : ℕ} {K n : ℤ} {N : ℕ} {R : HCPolySupport.TriadicCube d} (hR : R ∈ interiorMesoCubeGrid d K n (n + ↑N - 1)) : HCPolySupport.Book.Ch03.openCubeAtScale (HCPolySupport.triadicCubeShift R) (n + ↑N) ⊆ HCPolySupport.openCubeSet (HCPolySupport.originCube d K)

Unconditional: membership in the interior grid at outer scale n + N - 1 is exactly the containment z + cu_{n+N} subset cu_K printed.

The covering discharge

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.gridFourthMoment_mesoWindowEnergy_le {d : ℕ} {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) {K n : ℤ} {N : ℕ} (hn : n ≤ K - 1) (hN : n + ↑N ≤ K - 1) (u : Ω → HCPolySupport.Vec d → HCPolySupport.Vec d) {E : ℝ} (hcoord : ∀ (ω : Ω) (k : Fin d), MeasureTheory.IntegrableOn (fun (x : HCPolySupport.Vec d) => u ω x k ^ 2) (HCPolySupport.openCubeSet (HCPolySupport.originCube d K)) MeasureTheory.volume) (hsq : ∀ (ω : Ω), MeasureTheory.IntegrableOn (fun (x : HCPolySupport.Vec d) => HCPolySupport.vecNormSq (u ω x)) (HCPolySupport.openCubeSet (HCPolySupport.originCube d K)) MeasureTheory.volume) (hfour : ∀ (ω : Ω), MeasureTheory.IntegrableOn (fun (x : HCPolySupport.Vec d) => HCPolySupport.vecNormSq (u ω x) ^ 2) (HCPolySupport.openCubeSet (HCPolySupport.originCube d K)) MeasureTheory.volume) (hcellInt : ∀ R ∈ interiorMesoCubeGrid d K n (n + ↑N - 1), MeasureTheory.Integrable (fun (ω : Ω) => mesoWindowFourthEnergy (n + ↑N) (u ω) R) μ) (hglobInt : MeasureTheory.Integrable (fun (ω : Ω) => originCubeFourthEnergy K (u ω)) μ) (henv : ∫ (ω : Ω), originCubeFourthEnergy K (u ω) ∂μ ≤ E) : (gridFourthMoment μ (interiorMesoCubeGrid d K n (n + ↑N - 1)) fun (R : HCPolySupport.TriadicCube d) (ω : Ω) => mesoWindowEnergy (n + ↑N) (u ω) R) ≤ 3 ^ d * E

The meso-window energy average, from the global fourth energy.

This is the manuscript's step "by e.nablaw.in.L.eight", made explicit: the grid fourth moment of the window energies over the interior meso grid is at most 3^d times the annealed global fourth energy on cu_K.

The overlap multiplicity 3^{dN} of LocalizationOverlapCount cancels exactly against the window volume; the surviving 3^d is the interior-grid deficit of card_mesoCubeGrid_le_three_pow_mul_card_interior.

Complete binder census, beyond the typing binders d, Omega, inst, mu, K, n, N, u, E:

• hn : n <= K - 1 -- interior-grid scale gate;
• hN : n + N <= K - 1 -- interior-grid outer scale gate;
• hcoord -- integrability on cu_K, for every sample, of the coordinate squares of u omega;
• hsq -- integrability on cu_K, for every sample, of |u omega|^2;
• hfour -- integrability on cu_K, for every sample, of |u omega|^4;
• hcellInt -- integrability in the sample of the window fourth energy, for every cube of the interior grid;
• hglobInt -- integrability in the sample of the global fourth energy;
• henv -- the envelope int_Omega fint_{cu_K} |u|^4 dmu <= E.

None of them is discharged here. No measurability of u in the sample is assumed, and none is used: every sample-space statement above is an Integrable hypothesis supplied by the caller.