LocalizationFluctuationMuMeasCell

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

The three integrability producers of the gamma^{10} endpoint

ABK26, l.approximate.recurrence.formula, Steps 1--2, read at the recurrence pair (n, n+h).

integral_blockVecDot_recurrenceP_le_principalSwitchEnergyAverage_add carries exactly three analytic binders --- hintLHS, hintPrincipal, hintFluctuation. This module supplies them.

• hintLHS is discharged unconditionally (integrable_blockVecDot_coarseBlockMatrix_cutoffSampleLaw): the load is the constant recurrenceP, so the integrand is a fixed quadratic form in the coarse block matrix, and the entrywise integrability of that matrix under the genuine cutoff law is the proved moment layer (Provider.Annealed.coefficientCutoffLaw_integrable_blockMatEntry_coarseBlockMatrix) transported along the pushforward coefficientCutoffLaw = coefficientCutoff_* cutoffSampleLaw.

• hintPrincipal is reduced to one almost-sure upper bound on the switch energy (integrable_switchCubeEnergy_of_le): its measurability half is the proved PrincipalResponseGoodEnergy.aestronglyMeasurable_switchCubeEnergy at a measurable load family, and its lower half is the unconditional nonnegativity of the coarse quadratic form. The upper bound itself is the Step-3 good-event/bad-event budget and is not proved here; it is an explicit binder.

• hintFluctuation is reduced to a fixed-competitor statement (integrable_meshFluctuationCellIntegrand). The cell integrand is 2 mu_field - P_z . bfA P_z, and mu_field is squeezed between 0 and the energy of the background field P_z + bfF_z itself (LocalizationFluctuationMuMeasCore.{doubledMuField_nonneg, doubledMuField_le_self}), while its measurability is the countable-competitor identity of the same module. What remains is therefore: measurability of the fixed-competitor energies, and integrability of the one background energy. No measurable selection of a minimizer occurs anywhere.

References

• ABK26, l.approximate.recurrence.formula, e.lower.bound.basic.split, Step 2, the switch display.

The coarse block matrix of the genuine cutoff, read on the sample

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.integrable_blockMatEntry_switchCubeMatrix {d : ℕ} [NeZero d] (M : ABKModel d) (m : ℤ) (R : HCPolySupport.TriadicCube d) (alpha beta : HCPolySupport.BlockCoord d) : MeasureTheory.Integrable (fun (omega : Cutoff.CutoffSample d) => HCPolySupport.blockMatEntry (switchCubeMatrix M m R omega) alpha beta) ↑(Cutoff.cutoffSampleLaw M)

Every entry of the cell's coarse block matrix is sample-integrable. The proved entrywise integrability under the genuine coefficient-cutoff law, transported to the sample carrier CutoffSample d along the pushforward. Unconditional.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.integrable_blockVecDot_coarseBlockMatrix_cutoffSampleLaw {d : ℕ} (M : ABKModel d) (m : ℤ) (Q : HCPolySupport.TriadicCube d) (X : HCPolySupport.BlockVec d) : MeasureTheory.Integrable (fun (omega : Cutoff.CutoffSample d) => HCPolySupport.blockVecDot X (HCPolySupport.blockMatVecMul (HCPolySupport.Book.Ch02.coarseBlockMatrix (HCPolySupport.Book.Ch02.cubeDomain Q) ((Cutoff.coefficientCutoffTriadicCoeffFamily M m omega).coeffOn Q)) X)) ↑(Cutoff.cutoffSampleLaw M)

The hintLHS producer. For a constant doubled load the coarse quadratic form of the cutoff cell matrix is sample-integrable. Unconditional.

This is verbatim the hintLHS binder of integral_blockVecDot_recurrenceP_le_principalSwitchEnergyAverage_add once the cube is originCube d Kc and the load is recurrenceP (Annealed.sigmaBar M n) e e'.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.integrable_recurrenceP_coarseBlockMatrix {d : ℕ} (M : ABKModel d) (n Kc : ℤ) (h : ℕ) (e e' : HCPolySupport.Vec d) : MeasureTheory.Integrable (fun (omega : Cutoff.CutoffSample d) => HCPolySupport.blockVecDot (recurrenceP (Annealed.sigmaBar M n) e e') (HCPolySupport.blockMatVecMul (HCPolySupport.Book.Ch02.coarseBlockMatrix (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d Kc)) ((Cutoff.coefficientCutoffTriadicCoeffFamily M (n + ↑h) omega).coeffOn (HCPolySupport.originCube d Kc))) (recurrenceP (Annealed.sigmaBar M n) e e'))) ↑(Cutoff.cutoffSampleLaw M)

The hintLHS binder of the endpoint, at its own carriers. Unconditional.

The hintPrincipal producer

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.switchCubeEnergy_nonneg {d : ℕ} (M : ABKModel d) (m : ℤ) (R : HCPolySupport.TriadicCube d) (X : HCPolySupport.BlockVec d) (omega : Cutoff.CutoffSample d) : 0 ≤ switchCubeEnergy M m R X omega

The switch energy is nonnegative: the coarse doubled quadratic form of an elliptic coefficient is a nonnegative quadratic form. Unconditional.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.integrable_switchCubeEnergy_of_le {d : ℕ} (M : ABKModel d) (m : ℤ) (R : HCPolySupport.TriadicCube d) {X : Cutoff.CutoffSample d → HCPolySupport.BlockVec d} (hX : Measurable X) {g : Cutoff.CutoffSample d → ℝ} (hg : MeasureTheory.Integrable g ↑(Cutoff.cutoffSampleLaw M)) (hle : ∀ᵐ (omega : Cutoff.CutoffSample d) ∂↑(Cutoff.cutoffSampleLaw M), switchCubeEnergy M m R (X omega) omega ≤ g omega) : MeasureTheory.Integrable (fun (omega : Cutoff.CutoffSample d) => switchCubeEnergy M m R (X omega) omega) ↑(Cutoff.cutoffSampleLaw M)

The hintPrincipal producer. The switch energy at a measurable load family is sample-integrable as soon as it admits an almost-sure integrable upper bound; the lower bound is the unconditional nonnegativity of the coarse doubled quadratic form.

exactly on hX (measurability of the load family, a regularity property of the caller's corrector data, not a proof step) and on the a.s. domination hle, which is the Step-3 budget and is not proved here.

The cell carriers of the hintFluctuation producer

Three abbreviations for the sample-dependent data the Step-2 cell integrand is built from. Each is a plain unfolding of the endpoint's own expression; the rfl lemmas below record that.

noncomputable def Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.meshCellCoeff {d : ℕ} (M : ABKModel d) (m : ℤ) (R : HCPolySupport.TriadicCube d) (omega : Cutoff.CutoffSample d) : HCPolySupport.Book.Ch02.CoeffOn (HCPolySupport.Book.Ch02.cubeDomain R)

The cell's coefficient along the sample, bfA_m(z + cu_n).

Equations

• Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.meshCellCoeff M m R omega = (Algsuperdiff.Section3.Cutoff.coefficientCutoffTriadicCoeffFamily M m omega).coeffOn R

noncomputable def Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.meshCellLoad {d : ℕ} (M : ABKModel d) (n : ℤ) (h : ℕ) (Kc : ℤ) (e e' : HCPolySupport.Vec d) (wD : Cutoff.ShellSeq d → HCPolySupport.H10Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d Kc))) (wN : Cutoff.ShellSeq d → HCPolySupport.H1MeanZeroFunction (HCPolySupport.openCubeSet (HCPolySupport.originCube d Kc))) (R : HCPolySupport.TriadicCube d) (omega : Cutoff.CutoffSample d) : HCPolySupport.BlockVec d

The cell's principal load along the sample, P_z of e.Pz.def.

Equations

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

noncomputable def Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.meshCellBackground {d : ℕ} (M : ABKModel d) (n : ℤ) (h : ℕ) (Kc : ℤ) (e e' : HCPolySupport.Vec d) (wD : Cutoff.ShellSeq d → HCPolySupport.H10Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d Kc))) (wN : Cutoff.ShellSeq d → HCPolySupport.H1MeanZeroFunction (HCPolySupport.openCubeSet (HCPolySupport.originCube d Kc))) (R : HCPolySupport.TriadicCube d) (omega : Cutoff.CutoffSample d) : HCPolySupport.Book.Ch02.DoubledField d

The cell's background doubled field along the sample, P_z + bfF_z. It is the slope datum of the field-slope variational problem whose minimum is the fluctuation number, and it is itself an admissible competitor.

Equations

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

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.meshFluctuationCellIntegrand_eq {d : ℕ} (M : ABKModel d) (n : ℤ) (h : ℕ) (Kc : ℤ) (e e' : HCPolySupport.Vec d) (wD : Cutoff.ShellSeq d → HCPolySupport.H10Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d Kc))) (wN : Cutoff.ShellSeq d → HCPolySupport.H1MeanZeroFunction (HCPolySupport.openCubeSet (HCPolySupport.originCube d Kc))) (R : HCPolySupport.TriadicCube d) (omega : Cutoff.CutoffSample d) : meshFluctuationCellIntegrand M n h Kc e e' wD wN R omega = 2 * doubledMuField (HCPolySupport.Book.Ch02.cubeDomain R) (meshCellCoeff M (n + ↑h) R omega) (meshCellBackground M n h Kc e e' wD wN R omega) - switchCubeEnergy M (n + ↑h) R (meshCellLoad M n h Kc e e' wD wN R omega) omega

The cell integrand is twice the field-slope minimum minus the switch energy. Definitional.

The hintFluctuation producer

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.integrable_meshFluctuationCellIntegrand {d : ℕ} (M : ABKModel d) (n : ℤ) (h : ℕ) (Kc : ℤ) (e e' : HCPolySupport.Vec d) (wD : Cutoff.ShellSeq d → HCPolySupport.H10Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d Kc))) (wN : Cutoff.ShellSeq d → HCPolySupport.H1MeanZeroFunction (HCPolySupport.openCubeSet (HCPolySupport.originCube d Kc))) (R : HCPolySupport.TriadicCube d) (hpot : ∀ (omega : Cutoff.CutoffSample d), HCPolySupport.MemVectorL2 (HCPolySupport.Book.Ch02.cubeDomain R).carrier (meshCellBackground M n h Kc e e' wD wN R omega).potential) (hflux : ∀ (omega : Cutoff.CutoffSample d), HCPolySupport.MemVectorL2 (HCPolySupport.Book.Ch02.cubeDomain R).carrier (meshCellBackground M n h Kc e e' wD wN R omega).flux) (hcomp : ∀ (k : ℕ), AEMeasurable (fun (omega : Cutoff.CutoffSample d) => HCPolySupport.Book.Ch02.doubledMuValue (HCPolySupport.Book.Ch02.cubeDomain R) (meshCellCoeff M (n + ↑h) R omega) (meshCellBackground M n h Kc e e' wD wN R omega + doubledMuFieldCompetitor (HCPolySupport.Book.Ch02.cubeDomain R) k)) ↑(Cutoff.cutoffSampleLaw M)) (hbg : MeasureTheory.Integrable (fun (omega : Cutoff.CutoffSample d) => HCPolySupport.Book.Ch02.doubledMuValue (HCPolySupport.Book.Ch02.cubeDomain R) (meshCellCoeff M (n + ↑h) R omega) (meshCellBackground M n h Kc e e' wD wN R omega)) ↑(Cutoff.cutoffSampleLaw M)) (hprin : MeasureTheory.Integrable (fun (omega : Cutoff.CutoffSample d) => switchCubeEnergy M (n + ↑h) R (meshCellLoad M n h Kc e e' wD wN R omega) omega) ↑(Cutoff.cutoffSampleLaw M)) : MeasureTheory.Integrable (fun (omega : Cutoff.CutoffSample d) => meshFluctuationCellIntegrand M n h Kc e e' wD wN R omega) ↑(Cutoff.cutoffSampleLaw M)

The hintFluctuation producer, at one cell.

The Step-2 cell integrand is sample-integrable once

• the background field P_z + bfF_z is vector-L^2 on the cell for every sample (hpot, hflux) --- a typing property of the corrector data;
• every fixed-competitor energy mu(a_omega; P_z + bfF_z + D_k) is sample-measurable (hcomp), D being the canonical countable competitor family of LocalizationFluctuationMuMeasCore;
• the one background energy mu(a_omega; P_z + bfF_z) is sample-integrable (hbg); and
• the switch energy at P_z is sample-integrable (hprin), which is the endpoint's own hintPrincipal.

No estimate on the fluctuation is used, and no minimizer is selected: the variational minimum enters only through the two unconditional bounds 0 <= mu_field <= mu(background) and through the countable-infimum identity.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.integrable_meshFluctuationCellIntegrand' {d : ℕ} (M : ABKModel d) (n : ℤ) (h : ℕ) (Kc : ℤ) (e e' : HCPolySupport.Vec d) (wD : Cutoff.ShellSeq d → HCPolySupport.H10Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d Kc))) (wN : Cutoff.ShellSeq d → HCPolySupport.H1MeanZeroFunction (HCPolySupport.openCubeSet (HCPolySupport.originCube d Kc))) (R : HCPolySupport.TriadicCube d) (hpot : ∀ (omega : Cutoff.CutoffSample d), HCPolySupport.MemVectorL2 (HCPolySupport.Book.Ch02.cubeDomain R).carrier (meshCellBackground M n h Kc e e' wD wN R omega).potential) (hflux : ∀ (omega : Cutoff.CutoffSample d), HCPolySupport.MemVectorL2 (HCPolySupport.Book.Ch02.cubeDomain R).carrier (meshCellBackground M n h Kc e e' wD wN R omega).flux) (hcomp : ∀ (Y : HCPolySupport.Book.Ch02.DoubledField d), HCPolySupport.Book.Ch02.IsDoubledTestField (HCPolySupport.Book.Ch02.cubeDomain R) Y → AEMeasurable (fun (omega : Cutoff.CutoffSample d) => HCPolySupport.Book.Ch02.doubledMuValue (HCPolySupport.Book.Ch02.cubeDomain R) (meshCellCoeff M (n + ↑h) R omega) (meshCellBackground M n h Kc e e' wD wN R omega + Y)) ↑(Cutoff.cutoffSampleLaw M)) (hbg : MeasureTheory.Integrable (fun (omega : Cutoff.CutoffSample d) => HCPolySupport.Book.Ch02.doubledMuValue (HCPolySupport.Book.Ch02.cubeDomain R) (meshCellCoeff M (n + ↑h) R omega) (meshCellBackground M n h Kc e e' wD wN R omega)) ↑(Cutoff.cutoffSampleLaw M)) (hprin : MeasureTheory.Integrable (fun (omega : Cutoff.CutoffSample d) => switchCubeEnergy M (n + ↑h) R (meshCellLoad M n h Kc e e' wD wN R omega) omega) ↑(Cutoff.cutoffSampleLaw M)) : MeasureTheory.Integrable (fun (omega : Cutoff.CutoffSample d) => meshFluctuationCellIntegrand M n h Kc e e' wD wN R omega) ↑(Cutoff.cutoffSampleLaw M)

The hintFluctuation producer at one cell, in the choice-free form. The fixed-competitor hypothesis quantifies over every test field on the cell, so the canonical (choice-named) competitor family occurs in no hypothesis.