SplitObligationsPrincipal

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

Obligation (1) of SplitScaleObligations: the switch energy is sample-integrable

ABK26, l.approximate.recurrence.formula, Steps 1--3, e.Pz.def, the switch display.

What this module supplies

Closure.SplitProducerFold.SplitScaleObligations's first conjunct: per mesoscopic cell of the closure mesh,

  omega |->  P_z . bfA_{n+h}(z + cu_n) P_z    is integrable under  cutoffSampleLaw M .

LocalizationFluctuationMuMeasCell.integrable_switchCubeEnergy_of_le reduces it to a measurable load family and one almost-surely integrable dominator. The measurability half is the proved Closure.SplitProducerLoad.measurable_principalPz_cutoffSample. The dominator is produced here, from two proved moment layers and nothing else:

• the pathwise coarse-quadratic bound Closure.SplitObligationsQuadratic.switchCubeEnergy_le_ellipticityUpper, which replaces the coarse matrix by the realised upper ellipticity constant Lam_omega := Cutoff.coefficientCutoffCubeEllipticityUpper M (n+h) omega R of the cell and the two squared component lengths of the load; and
• the two integrability facts Cutoff.integrable_coefficientCutoffCubeEllipticityUpper_pow (every finite moment of Lam_omega, under the genuine cutoff law) and PrincipalResponseGoodEnergy.exists_gamma0_integrable_switchEllipLoad_principalPz_sq (the second moment of the ellipticity load shom |p_z|^2 + shom^{-1} |q_z|^2 of e.Pz.def).

The two are combined by plain domination: writing L for the ellipticity load, |p_z|^2 <= shom^{-1} L and |q_z|^2 <= shom L, and each of Lam L, Lam^2 L, L is dominated by half a sum of squares whose two summands are Lam^2, Lam^4, L^2 and 1. No Holder inequality and no selection occurs.

Binders

Beyond the typing binders: the parameter block of e.recurrence.params in the shape Closure.ClosureRegime supplies (the induction state, 0 < h, the cgamma threshold through Cterm (cstar M)^{-1} <= Ec and cgamma <= Ec^{-5}, and h <= 6 cstar cgamma^{-1}), the large-cube gate, the two direction bounds, and the two weak-solution properties of e.def.w for the corrector families. No measurability, smallness or selection property of the families is assumed.

Scope

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

References

• ABK26, l.approximate.recurrence.formula, Steps 1--3, e.Pz.def, e.recurrence.params, e.nablaw.in.L.eight.

Two elementary measurability facts

Domination by half a sum of squares

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.integrable_mul_of_sq_integrable {Omega : Type u_1} [MeasurableSpace Omega] {mu : MeasureTheory.Measure Omega} {A B : Omega → ℝ} (hA0 : ∀ (omega : Omega), 0 ≤ A omega) (hB0 : ∀ (omega : Omega), 0 ≤ B omega) (hAB : MeasureTheory.AEStronglyMeasurable (fun (omega : Omega) => A omega * B omega) mu) (hA : MeasureTheory.Integrable (fun (omega : Omega) => A omega ^ 2) mu) (hB : MeasureTheory.Integrable (fun (omega : Omega) => B omega ^ 2) mu) : MeasureTheory.Integrable (fun (omega : Omega) => A omega * B omega) mu

Two nonnegative square-integrable functions have an integrable product. Plain arithmetic--geometric-mean domination; no Holder inequality is used.

The per-cell integrability, from the ellipticity load's second moment

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.integrable_switchCubeEnergy_of_integrable_switchEllipLoad_sq {d : ℕ} (M : ABKModel d) (sigma : Observable.PositiveScalar) (m : ℤ) (R : HCPolySupport.TriadicCube d) {X : Cutoff.CutoffSample d → HCPolySupport.BlockVec d} (hX : Measurable X) (hL : MeasureTheory.Integrable (fun (omega : Cutoff.CutoffSample d) => switchEllipLoad (↑sigma) (X omega) ^ 2) ↑(Cutoff.cutoffSampleLaw M)) : MeasureTheory.Integrable (fun (omega : Cutoff.CutoffSample d) => switchCubeEnergy M m R (X omega) omega) ↑(Cutoff.cutoffSampleLaw M)

Obligation (1) at one cell, from the second moment of the ellipticity load.

exactly on hX (measurability of the load family, a regularity property of the caller's corrector data) and hL, the second moment of switchEllipLoad at the load. No estimate of the manuscript is used.