PrincipalResponseComposeDisplayTwo #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Provider: display 2 of leg (iv) in the manuscript's own printed shape #
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 .
The proved exists_const_fourthMoment_annealedSqrtNormSq_principalPz_le
(PrincipalResponseDisplayTwo) delivers this display in two respects weaker
than printed:
- its right-hand side carries the visible gauge factor
(gaugeRatio shom_{m-h} sigmaTop)^{1/2}instead of the bareC, because the three scale gates that theorem binds constrain no scale abovem0 >= m - h, hence say nothing about the reading scalem - 1.
This module removes both gaps, and nothing else.
The order swap #
descendantsAverage Q j is by definition (card)^{-1} times a finite
Finset sum, so the swap is the linearity of the Bochner integral over a
finite index set (integral_const_mul and integral_finsetSum). What
linearity costs is exactly one side condition: each individual expectation must
exist. That is hintR below, a per-cube integrability binder. It is a
well-definedness condition on the manuscript's own E[ ... ], of the same
class as the measurability binder hmeasX already carried by the proved
display, and it is not a bound: no numerical estimate, and no conclusion of
any predecessor node, is assumed by it. hmeasR is the matching per-cube
measurability, from which the proved display's own composite hmeasX is
produced here rather than demanded of the caller.
The bare C #
gaugeRatio sigmaLow sigmaTop = max (sigmaTop / sigmaLow) (sigmaLow / sigmaTop). At the manuscript's own pair of scales, sigmaLow = shom_{m-h}
and sigmaTop = shom_{m-1}, the two-sided envelope e.shom.h.bounds (the
first clause of d.mathcalS.def) controls both quotients through the two
proved running-diffusivity comparisons
shom_i <= 4 . 3^{cgamma (i - j)} . shom_j , shom_j <= 4 shom_i
(j <= i <= m_0) .
Since h >= 1 we have m - h <= m - 1, and the shell budget h <= 6 cstar cgamma^{-1}/7183 -- a gate the proved display already binds -- together with
cstar <= 3/2 gives cgamma ((m-1) - (m-h)) = cgamma (h - 1) <= 6 cstar <= 9,
so the exponential factor is at most 3^9. Hence
gaugeRatio shom_{m-h} shom_{m-1} <= 4 . 3^9 ,
an absolute constant. The only genuinely new input is the gate m - 1 <= m_0
(hm1), which places the reading scale inside the range on which the induction
state is available; it is carried as an explicit binder, never discharged and
never hidden. The manuscript's "by e.shom.h.bounds" is exactly this step, and
this is where its scale requirement becomes visible.
Binders #
Every theorem below is a **** provider result: each is stated under propositions the caller must supply, and none of them is a source-facing frozen declaration. What the caller owes, plainly:
integral_descendantsAverage_eq_descendantsAverage_integral_realandmeasurable_descendantsAverage_realask only for per-cube integrability respectively per-cube measurability of the family being averaged. These are well-definedness conditions on the manuscript's ownE[ . ], not estimates.gaugeRatio_sigmaBar_le_readingConstasks for the induction statehS(d.mathcalS.def, supplyinge.shom.h.bounds), the shell budgethh(h <= 6 cstar cgamma^{-1},/7183) and the reading-scale gatehm1(m - 1 <= m0).hm1is the one genuinely new input; it is the scale requirement the manuscript leaves implicit when it appeals toe.shom.h.boundsat the reading scale.exists_const_gridAverage_fourthMoment_annealedSqrtNormSq_principalPz_leasks forhS, the two corrector definitionshwD/hwN(e.def.w), the four scale gateshm(m - h <= m0),hm1,hhandhK(e.recurrence.params), and the two per-cube regularity bindershmeasR/hintR.
No proof step of the source argument, and no conclusion of a predecessor node, is assumed by any of them.
References #
- ABK26, display, inside
l.approximate.recurrence.formula;e.Pz.def;e.def.w;e.recurrence.params;e.shom.h.bounds(first clause ofd.mathcalS.def); ABK26 (the running-diffusivity comparison at constant4).
The order of the two averages #
Expectation and grid average commute. descendantsAverage Q j is a
normalized finite Finset sum, so the manuscript's avsum_z E[ . ] and the
pathwise-then-integrate E[ avsum_z . ] agree as soon as each individual
expectation exists.
: this statement holds only under the propositions supplied by its binders; it is a provider A, not a source-facing frozen declaration.
Per-cube measurability upgrades to measurability of the grid average.
: this statement holds only under the propositions supplied by its binders; it is a provider A, not a source-facing frozen declaration.
The reading gauge #
The gauge factor is an absolute constant at the manuscript's own pair of scales.
On the range where the induction state is available -- m - h <= m - 1 <= m0
-- e.shom.h.bounds gives shom_{m-1} <= 4 . 3^{cgamma (h-1)} shom_{m-h} and
shom_{m-h} <= 4 shom_{m-1}. The shell budget h <= 6 cstar cgamma^{-1}/7183
together with cstar <= 3/2 caps the exponent at 9, so both quotients are at
most 4 . 3^9.
hm1 is the reading-scale gate: it is a genuine input, not derivable from the
gates, and is carried as a binder.
: this statement holds only under the propositions supplied by its binders; it is a provider A, not a source-facing frozen declaration.
Display 2 in the printed shape #
Display 2 of leg (iv) of l.approximate.recurrence.formula, in the
manuscript's own order and with the printed bare constant.
There is a dimension-free constant C and a positive threshold gamma0 such
that, for every ABK model with cgamma <= gamma0, every valid induction state
S(m0, E), every m, K, h obeying the four scale gates m - h <= m0,
m - 1 <= m0, h <= 6 cstar cgamma^{-1} and K >= m + 10^10 cgamma^{-1}, all
directions e, e' of Euclidean length at most one, every localization depth j
and every sample family of solutions of the two problems e.def.w,
( avsum_R E[ | bfAhom_{m-1}^{1/2} P_R |^4 ] )^{1/4} <= C ,
with R running over the triadic descendants of cu_K at depth j and P_R
the localized load of e.Pz.def, read at the manuscript's own gauge
shom_{m-1}.
hmeasR and hintR are the per-cube well-definedness binders of the printed
E[ . ]; hm1 is the reading-scale gate discussed in the module header.
: this statement holds only under the propositions supplied by its binders; it is a provider A, not a source-facing frozen declaration.