CombineGoodEvent #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The good-event branch of Step 1 of the corrected combine proposition #
Step 1 of Proposition p.combine.under.S splits the response of the ordinary
central child along the event e.goodevent.combine
G = { sigmabar_L / 2 <= lambda_{1/4,1}(cu_m; a_L) <= Lambda_{1/4,1}(cu_m; a_L) <= 2 sigmabar_L }
and estimates the G-part by the weak-norm chain, the G^c-part being the
separate bad-event branch. This module carries the G-part, in the pointwise
form that precedes every expectation: the printed chain
l.J.bound.by.Besov, consumed as the committed compositeBesov.exists_restrictionResponseJ_centralChild_le_jBoundByBesovDisplay;- the two prefactor facts,
(Lambda/lambda)^{1 + s/(1-2s)} 1_G <= CandLambda 1_G <= 2 sigmabar_L; l.Besov.normsatr = 1, consumed as the committed four-term displayBesov.centredMultiscaleAverageSum_le_fourTerm;- the square expansion of the four terms, with Cauchy--Schwarz in the scale sum
converting the printed discount
3^{-(1-s)(m-n)}of the defect term into the printed weight3^{-(m-n)}ofe.initial.JL.bound; - the reabsorption of the energy term through
e.Jenergyv.nosymm, under the printed constraintC 3^{-(1-s)(m-L)} <= 1/4; - the merge of the two constant tails (the centring tail of the
l.J.bound.by.Besovdisplay and the fourth printed term ofl.Besov.norms), which are the same|sigma_*^{-1}(cu_m)(q + kappa_L(cu_m)p) - p|^2.
Everything here is a sample-by-sample inequality, so the reabsorbed energy term
appears as 1/2 J(cu_m) on the right-hand side, exactly as in the printed proof
where 1/2 E[J(cu_m)] sits on both sides of e.initial.JL.bound.
The subadditivity digging room Sum_{R child of cu_m} 2 (J(R) - J(cu_m)) that
the l.J.bound.by.Besov composite carries is merged into the printed defect sum
at the single scale n = m - 1; the defect summands are nonnegative by
e.subaddJ.nosymm, so the merge only enlarges the right-hand side.
Scale conventions #
The printed discount is s = 1/4 and the printed exponent is q = 1, which is
where Provider/Homogenization/CombineBadEvent.lean places the good/bad split.
At s = 1/4 the printed prefactor exponent s / (1 - 2s) is 1/2 and the
printed discount 1 - s is 3/4.
References #
- ABK26, Section 3.5, proof of
p.combine.under.S, Step 1.
Arithmetic cores over abstract reals #
The two geometric scale series #
The printed weight 3^{-(m-n)} sums to at most 3/2 on the corridor.
The subadditivity digging room as a single defect scale #
The good-event branch of Step 1 #
The good-event branch of Step 1 of p.combine.under.S, sample by sample
and on the actual coefficient field.
On the printed good event e.goodevent.combine at the printed discount
s = 1/4 and printed exponent q = 1, that is under the two clauses
sigma / 2 <= lambda_{1/4,1}(cu_m; a) and Lambda_{1/4,1}(cu_m; a) <= 2 sigma,
and under the printed smallness constraint C 3^{-(1-s)(m-L)} <= 1/4, the response
of the ordinary central child obeys the display the printed proof reaches: the
maximizing energy term has been reabsorbed through e.Jenergyv.nosymm, so half
the response at the parent scale sits on the right-hand side, and the remaining
three amplitudes are the printed defect sum with the printed weight
3^{-(m-n)} over the finite corridor L <= n <= m, the printed coarse-matrix
variation in its avsum form, and the printed constant tail, each carrying a
single power of the comparator.
This is NOT the labelled display e.initial.JL.bound, whose second and third
blocks are the variances and whose comparator prefactor is sigmabar_L^2 after
the normalization |q|^2 = sigmabar_L, |p|^2 = sigmabar_L^{-1} of
e.pq.normed and the sandwich sigmabar_{L,*}(cu_m) <= sigmabar_L <= 2 sigmabar_{L,*}(cu_m). The variance split, that normalization, the expectation
lane and stationarity are not performed here. The middle printed clause
lambda_{1/4,1} <= Lambda_{1/4,1} of e.goodevent.combine is not assumed: the
estimate holds from the two outer clauses alone, so the hypothesis set here is
weaker than the printed event.
The constant depends only on d, and on nothing else: it is quantified before
the field, the scales, the comparator and the loads.
This is a local Provider theorem and makes no source-node status claim.
The good-event branch of Step 1 on the Section 3 cutoff carrier.
The good event is the complement of observationScaleBadEvent M L m, which
mem_observationScaleBadEvent_iff identifies with the printed
e.goodevent.combine at s = 1/4, q = 1, on the genuine cutoff family; the
comparator is the running diffusivity sigmabar_L and the loads are the
manuscript ones, p = sigmabar_L^{-1/2} e and q = sigmabar_L^{1/2} e.
The two response scales are read through the one common measurable representative, so the estimate holds off a single null set. The response defect, the coarse-matrix variation and the constant tail are still the deterministic field quantities: taking expectations of them, through stationarity and the annealed identities, is the next step of the printed proof and is not performed here.
This is a local Provider theorem and makes no source-node status claim.