LocalizationEnvelopeWire

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.

The oscillation grid fourth moment with the sample-space binders gone

Source displays in ABK26:

• e.lower.bound.oscillations (label; display);
• e.nablaw.in.L.eight (label; display);
• e.def.w (label);
• e.recurrence.params (label).

What this module is

LocalizationEnvelopeGrid proves the grid fourth-moment bound with the envelope derived, but its own inventory lists three sample-space hypotheses it must assume:

• hTm : A Tfluct mu;
• hcellInt, integrability in the sample of the window fourth energies;
• hglobInt, integrability in the sample of the global fourth energy.

This module removes all three, using the quartic measurability of Corrector.CorrectorMeasurableQuartic. Two observations do the work.

1. A measurable fluctuation dominated by the given one. Write G(omega) = fint_{cu_K} |u(omega)|^4 for the global fourth energy. This is a measurable function of the sample, by the quartic layer. Put

     T'(omega) = max( sqrt(G(omega)) - Chead , 0 ) .
   

   Then T' is measurable and nonnegative by construction; it satisfies G <= (Chead + T')^2 by construction; and T' <= T pointwise, because the spatial L^4 <= L^8 bridge turns the caller's L^8 bound into G <= (Chead + T)^2. A pointwise-smaller variable inherits the stretched-exponential tail (IsBigOWith.of_le), so T' is an O_{Gamma_1}(A) variable with the same amplitude. The whole envelope derivation now runs on T', whose measurability is a theorem rather than a hypothesis.

2. Integrability by domination. G is measurable and squeezed between 0 and 2 Chead^2 + 2 T'^2, whose second moment is finite by the tail; and each window fourth energy is measurable and at most a fixed volume ratio times G, the window being contained in cu_K.

What is proved

• gridFourthMoment_mesoWindowEnergy_le_of_measurable_fourthEnergy -- the generic form: the grid fourth-moment bound with hTm, hcellInt and hglobInt replaced by measurability of the two fourth-energy observables.
• exists_freshShell_gridFourthMoment_mesoWindowEnergy_le_wired -- the same at the actual correctors of e.def.w, where the two measurability hypotheses are themselves theorems, so that no sample-space binder of any kind survives.

Which binders die and which survive

Relative to exists_freshShell_gridFourthMoment_mesoWindowEnergy_le, the three sample-space binders A Tfluct, hcellInt and hglobInt are gone. What survives, and is disclosed below, is exactly:

• the model and parameter gates of e.recurrence.params and the two direction bounds -- unchanged;
• the two interior-grid scale gates n <= K - 1, n + N <= K - 1 -- unchanged;
• the caller's family of weak solutions of e.def.w -- unchanged;
• the spatial binders hmem (L^8 membership on cu_K), hcoord, hsq, hfour (integrability on cu_K of the coordinate squares, of |u|^2 and of |u|^4). These are statements about a single sample point; nothing in the measurability layer bears on them and none of them is assumed away.

In the generic form one further binder appears that the source form did not need: hChead : 0 <= Chead. It is used to compare sqrt(G) with Chead + T, and at the actual correctors it is supplied by the positivity of Chead that e.nablaw.in.L.eight produces.

What is not proved here

• The second inequality, <= cgamma^{15}, is untouched.
• The forcing term of the display is untouched.
• The per-site estimate e.nablaw.oscillations is not inserted here.
• No measurable selection of correctors is used. The corrector families are arbitrary weak-solution families; their gradients are measurable because the solution operator is continuous, not because a selection was made.

Scope

It records no availability status.

Divergences from the printed statement

The divergences of LocalizationEnvelopeGrid carry over unchanged:, and the two added interior scale gates. No new divergence is introduced.

References

• ABK26, e.lower.bound.oscillations; e.nablaw.in.L.eight; e.def.w, display (label); e.recurrence.params, display (label), with the h gate.

The window is dominated by the cube

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.mesoWindowFourthEnergy_le_ratio_mul_originCubeFourthEnergy {d : ℕ} {K ell : ℤ} {R : HCPolySupport.TriadicCube d} (u : HCPolySupport.Vec d → HCPolySupport.Vec d) (hsub : HCPolySupport.Book.Ch03.openCubeAtScale (HCPolySupport.triadicCubeShift R) ell ⊆ HCPolySupport.openCubeSet (HCPolySupport.originCube d K)) (hfour : MeasureTheory.IntegrableOn (fun (x : HCPolySupport.Vec d) => HCPolySupport.vecNormSq (u x) ^ 2) (HCPolySupport.openCubeSet (HCPolySupport.originCube d K)) MeasureTheory.volume) : mesoWindowFourthEnergy ell u R ≤ (MeasureTheory.volume (HCPolySupport.Book.Ch03.openCubeAtScale (HCPolySupport.triadicCubeShift R) ell)).toReal⁻¹ * (MeasureTheory.volume (HCPolySupport.openCubeSet (HCPolySupport.originCube d K))).toReal * originCubeFourthEnergy K u

The window fourth energy is at most the volume ratio times the global fourth energy, for any window contained in cu_K.

: the caller supplies hsub (the containment) and hfour (integrability of |u|^4 on cu_K).

The generic wired form

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.gridFourthMoment_mesoWindowEnergy_le_of_measurable_fourthEnergy {d : ℕ} {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {K n : ℤ} {N : ℕ} (hn : n ≤ K - 1) (hN : n + ↑N ≤ K - 1) (u : Ω → HCPolySupport.Vec d → HCPolySupport.Vec d) {Chead A : ℝ} (hChead : 0 ≤ Chead) (hA : 0 < A) {T : Ω → ℝ} (hT0 : ∀ (ω : Ω), 0 ≤ T ω) (hT : HCPolySupport.IndependentSums.IsBigOWith μ (HCPolySupport.IndependentSums.gammaSigma 1) T A) (hmem : ∀ (ω : Ω), MeasureTheory.MemLp (fun (x : HCPolySupport.Vec d) => HCPolySupport.Book.Ch02.vecNorm (u ω x)) 8 (HCPolySupport.normalizedCubeMeasure (HCPolySupport.originCube d K))) (hpath : ∀ (ω : Ω), Corrector.cubeEuclideanLpNorm (HCPolySupport.originCube d K) 8 (u ω) ^ 2 ≤ Chead + T ω) (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) (hglobMeas : Measurable fun (ω : Ω) => originCubeFourthEnergy K (u ω)) (hcellMeas : ∀ R ∈ interiorMesoCubeGrid d K n (n + ↑N - 1), Measurable fun (ω : Ω) => mesoWindowFourthEnergy (n + ↑N) (u ω) R) : (gridFourthMoment μ (interiorMesoCubeGrid d K n (n + ↑N - 1)) fun (R : HCPolySupport.TriadicCube d) (ω : Ω) => mesoWindowEnergy (n + ↑N) (u ω) R) ≤ 3 ^ d * freshShellFourthEnergyConst Chead A

The grid fourth-moment bound with the three sample-space binders gone.

The hypotheses hTm : A T mu, hcellInt and hglobInt of gridFourthMoment_mesoWindowEnergy_le_of_cubeEuclideanL8_pathwise are replaced by measurability of the two fourth-energy observables, which the quartic layer proves outright at the correctors. The fluctuation T itself is still allowed to be an arbitrary nonnegative O_{Gamma_1}(A) variable with no measurability property: the proof never uses T except through the pointwise-smaller measurable variable T' built from the global fourth energy.

Complete binder census, beyond the typing binders d, Omega, its MeasurableSpace instance, mu, K, n, N, u, Chead, A, T:

• [IsProbabilityMeasure mu] -- instance binder;
• hn : n <= K - 1, hN : n + N <= K - 1 -- the interior-grid scale gates;
• hChead : 0 <= Chead, hA : 0 < A;
• hT0 : forall omega, 0 <= T omega;
• hT : IsBigOWith mu (gammaSigma 1) T A;
• hmem, hpath -- the spatial L^8 membership and the pathwise L^8 bound;
• hcoord, hsq, hfour -- the three spatial integrability families on cu_K;
• hglobMeas, hcellMeas -- measurability in the sample of the global and of the window fourth energies.

No a.e.-measurability of T and no integrability in the sample is assumed.

The consumer at the actual fresh-shell correctors

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.exists_freshShell_gridFourthMoment_mesoWindowEnergy_le_wired (d : ℕ) (hd : 2 ≤ d) : ∃ (Chead : ℝ), 0 < Chead ∧ ∃ (gamma0 : ℝ), 0 < gamma0 ∧ gamma0 ≤ 1 / 4 ∧ ∀ (M : ABKModel d), M.gamma ≤ gamma0 → ∀ (m0 : ℤ) (Eind : { E : ℝ // 1 ≤ E }), Frozen.Section3.inductionState M m0 Eind → ∀ (m K : ℤ) (hh : ℕ), 0 < hh → m - ↑hh ≤ m0 → ↑hh ≤ 6 * Disorder.cstar M * M.gamma⁻¹ → 10 ^ 10 * M.gamma⁻¹ ≤ ↑K - ↑m → ∀ (e e' : HCPolySupport.Vec d), HCPolySupport.Book.Ch02.vecNorm e ≤ 1 → HCPolySupport.Book.Ch02.vecNorm e' ≤ 1 → ∃ (Tfluct : Cutoff.ShellSeq d → ℝ), (∀ (omega : Cutoff.ShellSeq d), 0 ≤ Tfluct omega) ∧ HCPolySupport.IndependentSums.IsBigOWith (↑M.P) (HCPolySupport.IndependentSums.gammaSigma 1) Tfluct (M.gamma ^ 100) ∧ (∀ (n : ℤ) (N : ℕ), n ≤ K - 1 → n + ↑N ≤ K - 1 → ∀ (wD : Cutoff.ShellSeq d → HCPolySupport.H10Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d K))), (∀ (omega : Cutoff.ShellSeq d), HCPolySupport.IsZeroTraceDirichletRhsWeakSolution (fun (x : HCPolySupport.Vec d) => 1) (HCPolySupport.openCubeSet (HCPolySupport.originCube d K)) (wD omega) fun (x : HCPolySupport.Vec d) => -Corrector.streamForcing (↑(Annealed.sigmaBar M (m - ↑hh)))⁻¹ omega (m - ↑hh) m e x) → (∀ (omega : Cutoff.ShellSeq d), MeasureTheory.MemLp (fun (x : HCPolySupport.Vec d) => HCPolySupport.Book.Ch02.vecNorm ((wD omega).grad x)) 8 (HCPolySupport.normalizedCubeMeasure (HCPolySupport.originCube d K))) → (∀ (omega : Cutoff.ShellSeq d) (k : Fin d), MeasureTheory.IntegrableOn (fun (x : HCPolySupport.Vec d) => (wD omega).grad x k ^ 2) (HCPolySupport.openCubeSet (HCPolySupport.originCube d K)) MeasureTheory.volume) → (∀ (omega : Cutoff.ShellSeq d), MeasureTheory.IntegrableOn (fun (x : HCPolySupport.Vec d) => HCPolySupport.vecNormSq ((wD omega).grad x)) (HCPolySupport.openCubeSet (HCPolySupport.originCube d K)) MeasureTheory.volume) → (∀ (omega : Cutoff.ShellSeq d), MeasureTheory.IntegrableOn (fun (x : HCPolySupport.Vec d) => HCPolySupport.vecNormSq ((wD omega).grad x) ^ 2) (HCPolySupport.openCubeSet (HCPolySupport.originCube d K)) MeasureTheory.volume) → (gridFourthMoment (↑M.P) (interiorMesoCubeGrid d K n (n + ↑N - 1)) fun (R : HCPolySupport.TriadicCube d) (omega : ℤ → Frozen.Assumptions.ShellField d) => mesoWindowEnergy (n + ↑N) (wD omega).grad R) ≤ 3 ^ d * freshShellFourthEnergyConst Chead (M.gamma ^ 100)) ∧ ∀ (n : ℤ) (N : ℕ), n ≤ K - 1 → n + ↑N ≤ K - 1 → ∀ (wN : Cutoff.ShellSeq d → HCPolySupport.H1MeanZeroFunction (HCPolySupport.openCubeSet (HCPolySupport.originCube d K))), (∀ (omega : Cutoff.ShellSeq d), HCPolySupport.IsMeanZeroNeumannRhsWeakSolution (fun (x : HCPolySupport.Vec d) => 1) (HCPolySupport.openCubeSet (HCPolySupport.originCube d K)) (wN omega) fun (x : HCPolySupport.Vec d) => -Corrector.streamForcing (↑(Annealed.sigmaBar M (m - ↑hh)))⁻¹ omega (m - ↑hh) m e' x) → (∀ (omega : Cutoff.ShellSeq d), MeasureTheory.MemLp (fun (x : HCPolySupport.Vec d) => HCPolySupport.Book.Ch02.vecNorm ((wN omega).toH1Function.grad x)) 8 (HCPolySupport.normalizedCubeMeasure (HCPolySupport.originCube d K))) → (∀ (omega : Cutoff.ShellSeq d) (k : Fin d), MeasureTheory.IntegrableOn (fun (x : HCPolySupport.Vec d) => (wN omega).toH1Function.grad x k ^ 2) (HCPolySupport.openCubeSet (HCPolySupport.originCube d K)) MeasureTheory.volume) → (∀ (omega : Cutoff.ShellSeq d), MeasureTheory.IntegrableOn (fun (x : HCPolySupport.Vec d) => HCPolySupport.vecNormSq ((wN omega).toH1Function.grad x)) (HCPolySupport.openCubeSet (HCPolySupport.originCube d K)) MeasureTheory.volume) → (∀ (omega : Cutoff.ShellSeq d), MeasureTheory.IntegrableOn (fun (x : HCPolySupport.Vec d) => HCPolySupport.vecNormSq ((wN omega).toH1Function.grad x) ^ 2) (HCPolySupport.openCubeSet (HCPolySupport.originCube d K)) MeasureTheory.volume) → (gridFourthMoment (↑M.P) (interiorMesoCubeGrid d K n (n + ↑N - 1)) fun (R : HCPolySupport.TriadicCube d) (omega : ℤ → Frozen.Assumptions.ShellField d) => mesoWindowEnergy (n + ↑N) (wN omega).toH1Function.grad R) ≤ 3 ^ d * freshShellFourthEnergyConst Chead (M.gamma ^ 100)

e.lower.bound.oscillations, first term, at the actual correctors of e.def.w, with every sample-space binder gone.

  3^d ( 2 Chead^2 + 32 e^2 (cgamma^100)^2 ) .

Relative to exists_freshShell_gridFourthMoment_mesoWindowEnergy_le the three sample-space hypotheses -- A Tfluct M.P.toMeasure, the window fourth-energy integrability hcellInt, and the global fourth-energy integrability hglobInt -- do not appear. The first is bypassed by the measurable dominating fluctuation described in the module docstring; the other two follow from measurability of the fourth-energy observables together with the L^8 bound. Tfluct is still chosen before the sample point, before the scales and before the correctors, so no measurable selection of correctors is claimed or used.

Complete surviving binder census:

• hd : 2 <= d;
• under the leading quantifiers, M.gamma <= gamma0, the induction state Algsuperdiff.Frozen.Section3.inductionState M m0 Eind, and the parameter gates 0 < hh, m - hh <= m0, hh <= 6 cstar M gamma^{-1}, 10^10 gamma^{-1} <= K - m of e.recurrence.params, together with the two direction bounds vecNorm e <= 1 and vecNorm e' <= 1;
• then, per leg, the interior-grid gates hn : n <= K - 1 and hNle : n + N <= K - 1; the caller's sample family of solutions together with its weak-solution property hsol; the spatial L^8 membership family hmem; and the three spatial integrability families hcoord, hsq, hfour on cu_K.

Every one of the surviving per-leg binders is a statement about a single sample point. No hypothesis about the sample space remains.