PrincipalResponseDisplayTwo

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

Binder descriptions below are an informal inventory only, NOT a source certification; certification vocabulary is reserved for frozen source-facing declarations.

Provider: display 2 of leg (iv) of the principal response

Source display in ABK26, inside Step 3 of the proof of l.approximate.recurrence.formula (label):

  ( avsum_{z in 3^n Zd cap cu_K} E[ | bfAhom_{m-1}^{1/2} P_z |^4 ] )^{1/4}  <=  C .

What is assembled here

The chain has six links, five of which are supplied by the modules imported above and by the two proved engines:

1. the collapse of the normalization (annealedSqrtNormSq_principalPz_eq, from ellipticityBudget_eq) and the gauge transport to shom_{m-1} (sq_annealedSqrtNormSq_le_gaugeRatio_sq_mul), which together reduce the integrand to the raw averaged slope pair times the squared gauge ratio;
2. the vector Jensen inequality at the fourth power and the L^4 <= L^8 bridge on each localization cube (portable module CubeJensenVec);
3. the grid re-assembly to a single global L^8 norm on cu_K (descendantsAverage_sq_vecNormSq_add_cubeAverageVec_le);
4. e.nablaw.in.L.eight for the two corrector gradients, and e.km.kn.Lp at p = 8 for the extra forcing shom^{-1} h e' carried by the Neumann slot of e.Pz.def, merged into a single Gamma_1 lane by isBigOWith_gammaSigma_one_add;
5. the transport of that lane from the canonical shell law to the cutoff-sample law (isBigOWith_cutoffSampleLaw_of_isBigOWith); and
6. the expectation (integral_le_of_le_shift_add_kappa_sq, which runs the proved integral_rpow_two_le_of_shift_add_one_orlicz) and the fourth root.

The gauge factor is displayed, not absorbed

The manuscript writes the display at the gauge shom_{m-1}, while P_z is built at shom_{m-h}. The bound below therefore carries the explicit factor (gaugeRatio shom_{m-h} shom_{m-1})^{1/2}. It is not absorbed into C: the three scale gates that this theorem binds do not control shom_{m-1} (they constrain scales at most m0 >= m - h only), so the manuscript's remark that e.shom.h.bounds makes the ratio dimensional is an input this theorem does not have and does not silently assume. This is the same convention as the proved PrincipalResponseMomentsFourth, which names the ratio and does not bound it.

The two analytic binders

hmeasX is the measurability of the display's own integrand: the manuscript writes E[...], which presupposes that the bracket is a random variable. It is a well-definedness condition, not a step of the estimate; no bound and no conclusion of any predecessor is assumed. The two solution binders hwD, hwN are the manuscript's own definitions e.def.w of the two correctors, one per sample.

References

• ABK26, display, inside l.approximate.recurrence.formula; e.Pz.def; e.def.w (label; the proved FreshShellL8 cites, which is a citation drift, not a statement drift); e.recurrence.params; e.nablaw.in.L.eight; e.km.kn.Lp.

The pathwise grid bound

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.pathwise_descendantsAverage_sq_annealedSqrtNormSq_le {d : ℕ} (sigmaLow sigmaTop : Observable.PositiveScalar) (omega : Cutoff.ShellSeq d) (lowScale highScale : ℤ) (e e' : HCPolySupport.Vec d) (Q : HCPolySupport.TriadicCube d) (j : ℕ) (wD : HCPolySupport.H10Function (HCPolySupport.openCubeSet Q)) (wN : HCPolySupport.H1MeanZeroFunction (HCPolySupport.openCubeSet Q)) (hD : MeasureTheory.MemLp wD.grad 8 (HCPolySupport.normalizedCubeMeasure Q)) (hN : MeasureTheory.MemLp wN.toH1Function.grad 8 (HCPolySupport.normalizedCubeMeasure Q)) : (HCPolySupport.descendantsAverage Q j fun (R : HCPolySupport.TriadicCube d) => annealedSqrtNormSq sigmaTop (principalPz sigmaLow omega lowScale highScale e e' R wD wN) ^ 2) ≤ 16 * gaugeRatio sigmaLow sigmaTop ^ 2 * (HCPolySupport.vecNormSq e' ^ 2 + HCPolySupport.vecNormSq e ^ 2) + 16 * gaugeRatio sigmaLow sigmaTop ^ 2 * (Corrector.cubeEuclideanLpNorm Q 8 wD.grad ^ 2 + 2 * Corrector.cubeEuclideanLpNorm Q 8 wN.toH1Function.grad ^ 2 + 2 * Corrector.cubeEuclideanLpNorm Q 8 (Corrector.streamForcing (↑sigmaLow)⁻¹ omega lowScale highScale e') ^ 2) ^ 2

The pathwise grid form of display 2. Combining the collapse of the normalization, the gauge transport, the vector Jensen inequality at the fourth power, the grid re-assembly and the L^4 <= L^8 bridge:

  avsum_R | bfAhom_{sigmaTop}^{1/2} P_R |^4
    <=  16 rho^2 ( |e'|^4 + |e|^4 )
        + 16 rho^2 ( ‖grad w_D‖^2 + 2‖grad w_N‖^2 + 2‖shom^{-1} h e'‖^2 )^2 ,

with rho = gaugeRatio sigmaLow sigmaTop and every norm the volume-normalized Euclidean L^8 norm on Q.

Display 2 of leg (iv)

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.exists_const_fourthMoment_annealedSqrtNormSq_principalPz_le (d : ℕ) (hd : 2 ≤ d) : ∃ (C : ℝ), 0 < C ∧ ∃ (gamma0 : ℝ), 0 < gamma0 ∧ gamma0 ≤ 1 / 4 ∧ ∀ (M : ABKModel d), M.gamma ≤ gamma0 → ∀ (m0 : ℤ) (E : { E : ℝ // 1 ≤ E }), Frozen.Section3.inductionState M m0 E → ∀ (m K : ℤ) (h : ℕ), 0 < h → m - ↑h ≤ m0 → ↑h ≤ 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 : ℕ) (sigmaTop : Observable.PositiveScalar) (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 - ↑h)))⁻¹ (↑z) (m - ↑h) 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 - ↑h)))⁻¹ (↑z) (m - ↑h) m e' x) → (Measurable fun (z : Cutoff.CutoffSample d) => HCPolySupport.descendantsAverage (HCPolySupport.originCube d K) j fun (R : HCPolySupport.TriadicCube d) => annealedSqrtNormSq sigmaTop (principalPz (Annealed.sigmaBar M (m - ↑h)) (↑z) (m - ↑h) m e e' R (wD z) (wN z)) ^ 2) → (∫ (z : Cutoff.CutoffSample d), HCPolySupport.descendantsAverage (HCPolySupport.originCube d K) j fun (R : HCPolySupport.TriadicCube d) => annealedSqrtNormSq sigmaTop (principalPz (Annealed.sigmaBar M (m - ↑h)) (↑z) (m - ↑h) m e e' R (wD z) (wN z)) ^ 2 ∂↑(Cutoff.cutoffSampleLaw M)) ^ (1 / 4) ≤ gaugeRatio (Annealed.sigmaBar M (m - ↑h)) sigmaTop ^ (1 / 2) * C

Display 2 of leg (iv) of l.approximate.recurrence.formula.

  E[ avsum_R | bfAhom_{sigmaTop}^{1/2} P_R |^4 ]^{1/4}
      <=  ( gaugeRatio shom_{m-h} sigmaTop )^{1/2} * C ,

with R running over the triadic descendants of cu_K at depth j and P_R the localized load of e.Pz.def. At the manuscript's reading gauge sigmaTop = shom_{m-1} the displayed factor is the ratio the manuscript absorbs into C by e.shom.h.bounds; it is left visible here because the gates bound above do not constrain the scale m - 1.

The expectation stands outermost, which is the pathwise-then-integrate reading; the manuscript's own order avsum_[...] follows from it by the finite linearity of the grid average whenever the individual expectations exist.