PrincipalResponseEllipBudget

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 grid ellipticity budget, and the display consumer that

no longer binds it

Source displays in ABK26:

• the ellipticity budget itself: the sentence By~\eqref{e.nablaw.in.L.eight} we have and the display

    avsum_{z in 3^n Zd cap cu_K}
      E[ shom_{m-h} |p_z|^2 + shom_{m-h}^{-1} |q_z|^2 ]  <=  C ,
  

  which sits between the gauge-switch chain that ends and the independence sentence;
• e.nablaw.in.L.eight (label; display), the input the manuscript names;
• e.Pz.def (label; display), which defines P_z = (p_z ; q_z);
• e.lower.bound.principal.one (label) and e.lower.bound.principal.one.pre (label; display), the display whose consumer binds the budget;
• e.recurrence.params (label; display);
• e.def.w (label), the two finite-volume correctors;
• the display of leg (iv), whose fourth moment is the input used below.

What this module supplies

One thing.

The budget. exists_const_descendantsAverage_integral_switchEllipLoad_principalPz_le is the display at the actual carriers: the grid is the triadic descendants of cu_K at a free depth j, the sample carrier is Cutoff.CutoffSample d under (Cutoff.cutoffSampleLaw M).toMeasure, the load is the manuscript's own P_z of e.Pz.def (principalPz) built from a sample family of solutions of e.def.w, and the two weights are the manuscript's own shom_{m-h} and shom_{m-h}^{-1}.

An earlier second public declaration of this module, a display consumer named exists_const_descendantsAverage_integral_principalGoodEventEnergy_le_annealedCube, has been deleted. Only the budget above remains, and it is what that chain consumes.

Why switchEllipLoad and annealedSqrtNormSq are the same thing

switchEllipLoad S X = S |X.1|^2 + S^{-1} |X.2|^2 and annealedSqrtNormSq sigma Y = sigma |Y.1|^2 + sigma^{-1} |Y.2|^2 are the same term; annealedSqrtNormSq_eq_switchEllipLoad is rfl. This is what makes the fourth-moment display of leg (iv) an input to the first-moment budget rather than a separate estimate.

The route, and the loss it costs

The manuscript derives from e.nablaw.in.L.eight directly: Jensen on each localization cube, then the volume-normalized L^2 <= L^8 comparison on cu_K. What this repository already carries at the actual carriers is the fourth moment of exactly the same quantity, namely exists_const_fourthMoment_annealedSqrtNormSq_principalPz_le of ApproximateRecurrence.PrincipalResponseDisplayTwo, which itself already composes e.nablaw.in.L.eight for the two corrector gradients with e.km.kn.Lp at p = 8 for the extra forcing shom^{-1} h e' carried by the Neumann slot of e.Pz.def, merges the two into a single Gamma_1 lane, and transports that lane to the cutoff-sample law.

The budget is therefore obtained here by descent from the fourth moment to the first, which is Cauchy--Schwarz:

  avsum_R E[X_R]  <=  ( avsum_R E[X_R^2] )^{1/2} ,

implemented as the pointwise X <= C/2 + X^2/(2C) at C the square root of the right-hand side. The descent is lossy: the constant produced below is the square root of the fourth-moment constant, not the sharp first-moment constant the manuscript's own route would give.

The reading gauge is the load's own gauge shom_{m-h}, which is the gauge the manuscript writes. At that gauge gaugeRatio is 1 (gaugeRatio_self), so no reading-gauge factor and no reading-scale gate m - 1 <= m0 is incurred.

The constant, factor by factor

  Cell = C0^2 = ( 32 + 16 ( 2 ( (2 Chead + 2 Clp (24 . 3^18))
                                 + 6 orliczSecondMomentScale 1 ) )^2 )^{1/2}

• Chead -- the head of e.nablaw.in.L.eight, produced by Corrector.exists_cubeEuclideanL8_gradient_sq_sum_le_const_add_gammaPow;
• 24 . 3^18 -- Corrector.inv_sigmaBarSq_mul_shellWidth_le, the normalization shom_{m-h}^{-2} h 3^{2 cgamma m} <= 24 . 3^18 under the gates/7183 and e.recurrence.params;
• orliczSecondMomentScale 1 -- the second moment of a Gamma_1 variable, from the proved Orlicz layer;
• the 2s, 16 and 32 -- the elementary doublings (a+b)^2 <= 2(a^2+b^2), the Minkowski step on the Neumann slot, the vector Jensen inequality at the fourth power and the two direction bounds |e|, |e'| <= 1, all inside pathwise_descendantsAverage_sq_annealedSqrtNormSq_le;
• the outer square root -- the Cauchy--Schwarz descent of this module;
• the reading gauge contributes the factor 1, by gaugeRatio_self.

No factor is a fitted number: each is either produced by a named theorem or is an elementary constant of a named inequality.

What is NOT proved here

• The manuscript's own derivation is not reproduced. The L^2 <= L^8 route from e.nablaw.in.L.eight is not carried out; the fourth moment is used instead, at the cost recorded above.
• Nothing about the other binders of the consumer. hlam0, hshell, hgoodInt, hcubeInt, hindep and hbudget remain binders and are listed by name in the docstring of the final theorem.
• The corrector families are not selected. wD and wN are arbitrary sample families of solutions of e.def.w; no measurable selection is claimed or used, and the per-cube measurability of the load is a caller-supplied data condition (hmeasR), not a theorem of this module.
• e.lower.bound.principal.one is not derived. Only the budget quoted is produced, and only the consumer's hellip and hellipInt binders are removed.

Main results

• exists_const_descendantsAverage_integral_switchEllipLoad_principalPz_le

References

• ABK26, (the budget), quoting e.nablaw.in.L.eight (label; display); e.Pz.def (label; display); e.lower.bound.principal.one (label); e.lower.bound.principal.one.pre (label; display); e.recurrence.params (label; display); e.def.w (label); the display of leg (iv); e.km.kn.Lp.

The two finite-average bookkeeping steps

The Cauchy--Schwarz descent from the second moment to the first

The reading gauge, and the identification of the two integrands

The budget

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.exists_const_descendantsAverage_integral_switchEllipLoad_principalPz_le (d : ℕ) (hd : 2 ≤ d) : ∃ (Cell : ℝ), 0 < Cell ∧ ∃ (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 : ℤ) (hgap : ℕ), 0 < hgap → m - ↑hgap ≤ m0 → ↑hgap ≤ 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 → ∀ (j : ℕ) (wD : Cutoff.CutoffSample d → HCPolySupport.H10Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d K))) (wN : Cutoff.CutoffSample d → HCPolySupport.H1MeanZeroFunction (HCPolySupport.openCubeSet (HCPolySupport.originCube d K))), (∀ (z : Cutoff.CutoffSample d), HCPolySupport.IsZeroTraceDirichletRhsWeakSolution (fun (x : HCPolySupport.Vec d) => 1) (HCPolySupport.openCubeSet (HCPolySupport.originCube d K)) (wD z) fun (x : HCPolySupport.Vec d) => -Corrector.streamForcing (↑(Annealed.sigmaBar M (m - ↑hgap)))⁻¹ (↑z) (m - ↑hgap) m e x) → (∀ (z : Cutoff.CutoffSample d), HCPolySupport.IsMeanZeroNeumannRhsWeakSolution (fun (x : HCPolySupport.Vec d) => 1) (HCPolySupport.openCubeSet (HCPolySupport.originCube d K)) (wN z) fun (x : HCPolySupport.Vec d) => -Corrector.streamForcing (↑(Annealed.sigmaBar M (m - ↑hgap)))⁻¹ (↑z) (m - ↑hgap) m e' x) → (∀ R ∈ HCPolySupport.descendantsAtDepth (HCPolySupport.originCube d K) j, Measurable fun (z : Cutoff.CutoffSample d) => switchEllipLoad (↑(Annealed.sigmaBar M (m - ↑hgap))) (principalPz (Annealed.sigmaBar M (m - ↑hgap)) (↑z) (m - ↑hgap) m e e' R (wD z) (wN z))) → (∀ R ∈ HCPolySupport.descendantsAtDepth (HCPolySupport.originCube d K) j, MeasureTheory.Integrable (fun (z : Cutoff.CutoffSample d) => switchEllipLoad (↑(Annealed.sigmaBar M (m - ↑hgap))) (principalPz (Annealed.sigmaBar M (m - ↑hgap)) (↑z) (m - ↑hgap) m e e' R (wD z) (wN z)) ^ 2) ↑(Cutoff.cutoffSampleLaw M)) → (HCPolySupport.descendantsAverage (HCPolySupport.originCube d K) j fun (R : HCPolySupport.TriadicCube d) => ∫ (z : Cutoff.CutoffSample d), switchEllipLoad (↑(Annealed.sigmaBar M (m - ↑hgap))) (principalPz (Annealed.sigmaBar M (m - ↑hgap)) (↑z) (m - ↑hgap) m e e' R (wD z) (wN z)) ∂↑(Cutoff.cutoffSampleLaw M)) ≤ Cell

The grid ellipticity budget, at the actual carriers.

  avsum_R E[ shom_{m-h} |p_R|^2 + shom_{m-h}^{-1} |q_R|^2 ]  <=  Cell ,

with R running over the triadic descendants of cu_K at depth j, (p_R; q_R) = P_R the localized load of e.Pz.def, and the expectation taken on Cutoff.CutoffSample d under (Cutoff.cutoffSampleLaw M).toMeasure.

The constant is Cell =^2 with the constant of exists_const_fourthMoment_annealedSqrtNormSq_principalPz_le; the module docstring lists every factor and its origin, and records that the descent from the fourth moment to the first is lossy.

Reaches exactly the one frozen theorem Algsuperdiff.Frozen.External.calderon_zygmund, a proved external.

: this statement holds only under the propositions supplied by its binders -- hd; under the leading quantifiers, M.gamma <= gamma0, the induction state Algsuperdiff.Frozen.Section3.inductionState M m0 Eind, the parameter gates 0 < hgap, m - hgap <= m0, hgap <= 6 cstar cgamma^{-1}, 10^10 cgamma^{-1} <= K - m, and the two direction bounds; then the two solution families of e.def.w, and the two per-cube data conditions hmeasR (measurability in the sample of the load) and hintR (integrability in the sample of its square). It is a provider A, not a source-facing frozen declaration.