GammaTenCloserMoments

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

The two L^4 memberships of the Step-2 grid fold

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

The gap this module fills

Closure.GammaTenAssemblyMoments.descendantsAverage_integral_fold_le_of_memLp_four_grid_load asks for three L^4 legs. The two deterministic ones have moment producers but no membership producer:

• the ellipticity leg is measurable only at the origin cube (LocalizationFluctuationNumericEllipticity.measurable_gaugedEllipticitySum_originCube), while the fold reads it at the cell's own scale-(n+h) ancestor;
• the load leg has a grid fourth moment (Closure.GammaTenLoad.exists_gammaTenLoadConst_root) but a grid moment bound is not an integrability statement --- an undefined Bochner integral is 0.

Both are supplied here.

What is proved

• measurePreserving_translateCutoffSample --- the cutoff-sample law is translation invariant, in the MeasurePreserving spelling (Cutoff.Symmetry.map_translateCutoffSample_cutoffSampleLaw repackaged).
• memLp_gaugedEllipticitySum_of_scale --- L^p membership of the gauged ellipticity sum transports from cu_m to any cube of scale m, by the pathwise covariance LocalizationFluctuationStationarity.gaugedEllipticitySum_scale_eq_originCube composed with the measure-preserving translation.
• exists_regime_memLp_four_gaugedEllipticitySum_ancestorAtScale --- the ellipticity leg is in L^4 at the ancestor, under exactly the two clauses of Closure.ClosureRegime that LocalizationFluctuationSplitFoldArithmetic.exists_regime_gaugedEllipticitySum_pow_four_le uses. The membership comes from the L^8 conjunct of LocalizationFluctuationNumericEllipticity.integral_gaugedEllipticitySum_rpow_eight_le.
• memLp_four_of_integrable_pow_four, le_card_mul_descendantsAverage --- two elementary devices.
• measurable_gammaTenLoadLeg, memLp_four_gammaTenLoadLeg --- the load leg is in L^4 at every cell: measurable by Closure.SplitProducerLoad.measurable_meshCellLoad, and dominated cellwise by the pathwise majorant of Closure.GammaTenLoad.exists_gammaTenLoadPathwiseConst whose sample moment is Closure.Step5InputGradMoment's exists_integral_streamIncrementLpNorm_eight_pow_four_le.

Binders

Regime binders only for the ellipticity leg (the induction state, the two largeness clauses and a produced cgamma-threshold); for the load leg the parameters of e.recurrence.params and the two direction bounds. No smallness gate is assumed and every threshold is produced.

Scope

There is no sorry, no admit, no custom axiom and no set_option maxHeartbeats.

References

• ABK26, l.approximate.recurrence.formula Step 2, the load display, e.nablaw.in.L.eight.

The ellipticity leg

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.measurePreserving_translateCutoffSample {d : ℕ} (M : ABKModel d) (v : HCPolySupport.Vec d) : MeasureTheory.MeasurePreserving (Cutoff.translateCutoffSample v) ↑(Cutoff.cutoffSampleLaw M) ↑(Cutoff.cutoffSampleLaw M)

The cutoff-sample law is invariant under a real translation of the shell field, in the MeasurePreserving spelling.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.memLp_gaugedEllipticitySum_of_scale {d : ℕ} (M : ABKModel d) (L m : ℤ) {T : HCPolySupport.TriadicCube d} (hT : T.scale = m) (sigmaBar s : ℝ) (p : ENNReal) (hmem : MeasureTheory.MemLp (fun (omega : Cutoff.CutoffSample d) => gaugedEllipticitySum sigmaBar (HCPolySupport.originCube d m) s (Cutoff.coefficientCutoffTriadicCoeffFamily M L omega)) p ↑(Cutoff.cutoffSampleLaw M)) : MeasureTheory.MemLp (fun (omega : Cutoff.CutoffSample d) => gaugedEllipticitySum sigmaBar T s (Cutoff.coefficientCutoffTriadicCoeffFamily M L omega)) p ↑(Cutoff.cutoffSampleLaw M)

L^p membership of the gauged ellipticity sum transports from the origin cube to an arbitrary cube of the same scale.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.exists_regime_memLp_four_gaugedEllipticitySum_ancestorAtScale (d : ℕ) : ∃ (Cell : ℝ) (gamma0 : ℝ), 0 < Cell ∧ 0 < gamma0 ∧ gamma0 ≤ 1 / 4 ∧ ∀ (M : ABKModel d) (m : ℤ) (Ec : { E : ℝ // 1 ≤ E }), M.gamma ≤ gamma0 → Frozen.Section3.inductionState M (m - 1) Ec → Cell * (Disorder.cstar M)⁻¹ ≤ ↑Ec → M.gamma ≤ ↑Ec ^ (-5) → ∀ (R : HCPolySupport.TriadicCube d), R.scale ≤ m → MeasureTheory.MemLp (fun (omega : Cutoff.CutoffSample d) => gaugedEllipticitySum (↑(Annealed.sigmaBar M (m - 1))) (ancestorAtScale R m) M.gamma (Cutoff.coefficientCutoffTriadicCoeffFamily M m omega)) 4 ↑(Cutoff.cutoffSampleLaw M)

The L^4 membership of the Step-2 ellipticity leg at the cell's own scale-m ancestor, under exactly the two regime clauses that LocalizationFluctuationSplitFoldArithmetic.exists_regime_gaugedEllipticitySum_pow_four_le uses and below a produced cgamma-threshold.

The membership at cu_m is the L^8 conjunct of LocalizationFluctuationNumericEllipticity.integral_gaugedEllipticitySum_rpow_eight_le; memLp_gaugedEllipticitySum_of_scale transports it to the ancestor.

exactly on the four listed premises.

The load leg

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.memLp_four_of_integrable_pow_four {Omega : Type u_1} [MeasurableSpace Omega] {mu : MeasureTheory.Measure Omega} {f : Omega → ℝ} (hf : ∀ (w : Omega), 0 ≤ f w) (hm : MeasureTheory.AEStronglyMeasurable f mu) (hint : MeasureTheory.Integrable (fun (w : Omega) => f w ^ 4) mu) : MeasureTheory.MemLp f 4 mu

L^4 membership of a nonnegative measurable function with an integrable fourth power.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.le_card_mul_descendantsAverage {d : ℕ} (Q : HCPolySupport.TriadicCube d) (j : ℕ) (F : HCPolySupport.TriadicCube d → ℝ) (hF : ∀ R ∈ HCPolySupport.descendantsAtDepth Q j, 0 ≤ F R) {R : HCPolySupport.TriadicCube d} (hR : R ∈ HCPolySupport.descendantsAtDepth Q j) : F R ≤ ↑(HCPolySupport.descendantsAtDepth Q j).card * HCPolySupport.descendantsAverage Q j F

Each member of a nonnegative family is below the cardinality times its descendant average.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.measurable_gammaTenLoadLeg {d : ℕ} [NeZero d] (M : ABKModel d) (n : ℤ) (h K : ℕ) (e e' : HCPolySupport.Vec d) {j : ℕ} {R : HCPolySupport.TriadicCube d} (hR : R ∈ HCPolySupport.descendantsAtDepth (HCPolySupport.originCube d ↑K) j) : Measurable fun (omega : Cutoff.CutoffSample d) => √(annealedSqrtNormSq (Annealed.sigmaBar M n) (meshCellLoad M n h (↑K) e e' (closureDirichletAlong M n h K e) (closureNeumannAlong M n h K e') R omega))

The Step-2 load leg is measurable in the sample, at every cell of the closure mesh and at the closure's own corrector families.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.memLp_four_gammaTenLoadLeg {d : ℕ} [NeZero d] (hd : 2 ≤ d) (M : ABKModel d) (n : ℤ) (h K : ℕ) (e e' : HCPolySupport.Vec d) (he : HCPolySupport.Book.Ch02.vecNorm e ≤ 1) (he' : HCPolySupport.Book.Ch02.vecNorm e' ≤ 1) (hh : 0 < h) (hmK : n + ↑h ≤ ↑K) {j : ℕ} {R : HCPolySupport.TriadicCube d} (hR : R ∈ HCPolySupport.descendantsAtDepth (HCPolySupport.originCube d ↑K) j) : MeasureTheory.MemLp (fun (omega : Cutoff.CutoffSample d) => √(annealedSqrtNormSq (Annealed.sigmaBar M n) (meshCellLoad M n h (↑K) e e' (closureDirichletAlong M n h K e) (closureNeumannAlong M n h K e') R omega))) 4 ↑(Cutoff.cutoffSampleLaw M)

The Step-2 load leg is in L^4, at every cell of the closure mesh.

The grid fourth moment of Closure.GammaTenLoad.exists_gammaTenLoadConst_root is a bound on a Bochner integral and therefore not by itself an integrability statement; the membership comes from the pathwise majorant of Closure.GammaTenLoad.exists_gammaTenLoadPathwiseConst, read at a single cell (one factor of the grid cardinality, which is harmless because the statement is per cell), whose sample moment is Closure.Step5InputGradMoment.exists_integral_streamIncrementLpNorm_eight_pow_four_le.

on the parameters of e.recurrence.params and the two direction bounds.