Step5InputSideConditions

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

The Step-5 typing side conditions at the closure's families

ABK26, Step 5 of l.approximate.recurrence.formula.

Besides the four mathematical legs (hshell, hgradM, hmemOsc, hosc), the basket Closure.Step5Basket.step5GaugeEndpoint_closureFamilies_of_momentLegs carries four typing binders: two sample measurabilities hmeasX, hmeasS, one spatial integrability hintP and one sample integrability hsampDef. This module discharges the first three at the closure's own families.

• hmeasX, hmeasS are products of the two measurable factors: the averaged fresh shell (ApproximateRecurrence.measurable_freshShellCubeAverage) and the potential average (ApproximateRecurrence.measurable_cubeAverageVec_freshShellDirichletGrad), both read at the full sigma-algebra.
• hintP is a spatial statement at a fixed sample: the fresh shell is continuous, hence bounded on the localization cube, and the corrector gradient is L^1 there, so the pairing is integrable.

hsampDef is not discharged here; it is discharged downstream, in Closure.Step5SampDefMeasurable (its measurability half) and Closure.Step5SampDef (the whole binder). See the disclosure.

References

• ABK26, l.approximate.recurrence.formula, Step 5.

Generic measurability of the two pairings

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.measurable_matVecMul_of_measurable {d : ℕ} {Omega : Type u_1} [MeasurableSpace Omega] {A : Omega → HCPolySupport.Mat d} {v : Omega → HCPolySupport.Vec d} (hA : Measurable A) (hv : Measurable v) : Measurable fun (omega : Omega) => HCPolySupport.matVecMul (A omega) (v omega)

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.measurable_vecDot_const {d : ℕ} {Omega : Type u_1} [MeasurableSpace Omega] (e : HCPolySupport.Vec d) {w : Omega → HCPolySupport.Vec d} (hw : Measurable w) : Measurable fun (omega : Omega) => HCPolySupport.vecDot e (w omega)

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.measurable_vecNormSq_of_measurable {d : ℕ} {Omega : Type u_1} [MeasurableSpace Omega] {w : Omega → HCPolySupport.Vec d} (hw : Measurable w) : Measurable fun (omega : Omega) => HCPolySupport.vecNormSq (w omega)

hmeasX and hmeasS at the closure's Dirichlet family

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.measurable_matVecMul_freshShellCubeAverage_cubeAverageVec {d : ℕ} [NeZero d] {Q R : HCPolySupport.TriadicCube d} {jd : ℕ} (hR : R ∈ HCPolySupport.descendantsAtDepth Q jd) (sigmaInv : ℝ) (n m : ℤ) (e : HCPolySupport.Vec d) (wD : Cutoff.ShellSeq d → HCPolySupport.H10Function (HCPolySupport.openCubeSet Q)) (hwD : ∀ (omega : Cutoff.ShellSeq d), HCPolySupport.IsZeroTraceDirichletRhsWeakSolution (fun (x : HCPolySupport.Vec d) => 1) (HCPolySupport.openCubeSet Q) (wD omega) fun (x : HCPolySupport.Vec d) => -Corrector.streamForcing sigmaInv omega n m e x) : Measurable fun (omega : Cutoff.CutoffSample d) => HCPolySupport.matVecMul (freshShellCubeAverage R (↑omega) n m) (HCPolySupport.cubeAverageVec R fun (x : HCPolySupport.Vec d) => (wD ↑omega).grad x)

The measurable pair of the Step-5 per-cube quadratic: the averaged fresh shell applied to the potential average.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.aestronglyMeasurable_step5PairingX {d : ℕ} [NeZero d] (M : ABKModel d) (n : ℤ) (h K : ℕ) (e : HCPolySupport.Vec d) {R : HCPolySupport.TriadicCube d} {j : ℕ} (hR : R ∈ HCPolySupport.descendantsAtDepth (HCPolySupport.originCube d ↑K) j) : MeasureTheory.AEStronglyMeasurable (fun (omega : Cutoff.CutoffSample d) => HCPolySupport.vecDot e (HCPolySupport.matVecMul (freshShellCubeAverage R (↑omega) n (n + ↑h)) (HCPolySupport.cubeAverageVec R fun (x : HCPolySupport.Vec d) => (alongIncrementPath n h (closureDirichletFamily (↑(Annealed.sigmaBar M n))⁻¹ e K) ↑omega).grad x))) ↑(Cutoff.cutoffSampleLaw M)

hmeasX at the closure's Dirichlet family.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.aestronglyMeasurable_step5PairingS {d : ℕ} [NeZero d] (M : ABKModel d) (n : ℤ) (h K : ℕ) (e : HCPolySupport.Vec d) {R : HCPolySupport.TriadicCube d} {j : ℕ} (hR : R ∈ HCPolySupport.descendantsAtDepth (HCPolySupport.originCube d ↑K) j) : MeasureTheory.AEStronglyMeasurable (fun (omega : Cutoff.CutoffSample d) => HCPolySupport.vecNormSq (HCPolySupport.matVecMul (freshShellCubeAverage R (↑omega) n (n + ↑h)) (HCPolySupport.cubeAverageVec R fun (x : HCPolySupport.Vec d) => (alongIncrementPath n h (closureDirichletFamily (↑(Annealed.sigmaBar M n))⁻¹ e K) ↑omega).grad x))) ↑(Cutoff.cutoffSampleLaw M)

hmeasS at the closure's Dirichlet family.

hintP: the spatial pairing on the localization cube

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.integrableOn_cubeSet_vecDot_matVecMul_finiteShellIncrement {d : ℕ} (Q : HCPolySupport.TriadicCube d) (omega : Cutoff.ShellSeq d) (n m : ℤ) (e : HCPolySupport.Vec d) {u : HCPolySupport.Vec d → HCPolySupport.Vec d} (hu : MeasureTheory.MemLp u 8 (HCPolySupport.normalizedCubeMeasure Q)) : MeasureTheory.IntegrableOn (fun (x : HCPolySupport.Vec d) => HCPolySupport.vecDot e (HCPolySupport.matVecMul ((Cutoff.finiteShellIncrement omega n m).toFun x) (u x))) (HCPolySupport.cubeSet Q) MeasureTheory.volume

hintP, at a fixed sample. The fresh shell is continuous, hence bounded on the closed localization cube; the corrector gradient is L^1 there, because it is L^8; so their pairing against a fixed direction is integrable.