InitialJLBound #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
(e.initial.JL.bound), Part C: the assembly of Step 1 of the corrected combine #
ABK26 (the display e.initial.JL.bound) and its proof.
Content part carried by this file #
This module is the second of the two files into which the Step-1 assembly
of the corrected combine is split. It carries Part C: the discharge of the
five Integrable clauses of the proved variance split, the corridor summation,
the anchor wiring and the absorption that turn the proved pre-variance-split
display into the printed e.initial.JL.bound. This is items (5)(6)(7) of the
depgraph record for node p.combine.corrected, the finite good-event Besov step.
Parts A and B --- the unconditional descendant envelope of the
sigma_*^{-1}kappa channel, the pointwise envelopes of the two deterministic
good-event blocks, their global integrability, and the discharge of the two
IntegrableOn binders of the proved CombineExpectation endpoints --- are in
Provider/Homogenization/InitialJLBoundIntegrability.lean, which this file
imports. Every declaration was moved verbatim. This half is still above the
800-line preference: about a third of it is this docstring, and the display
assembly is a single theorem with a 255-line proof, so no further cut is
available that does not split one proof. Both halves are well under the
1500-line cap.
Part C: the assembly into (e.initial.JL.bound) #
The five Integrable clauses of
coefficientCutoffLaw_sigmaBar_mul_integral_descendantsAverage_le
(VarianceSplit.lean) are discharged from the Part-A envelopes: the two
sigma_*^{-1} clauses are bounded by a deterministic constant (the
lower-right envelope carries no E), and the two sigma_*^{-1}kappa clauses
and the left-hand descendant average are dominated by quadratic polynomials in
E.
The two set integrals of the proved endpoint
exists_integral_cutoffResponseJ_le_reabsorbedExpectationDisplay
(CombineExpectation.lean) are then bounded by the global integrals
(setIntegral_le_integral, both blocks being pointwise nonnegative, by the
Part-A nonnegativity statements), the second block is summed over the printed
corridor, and the third block is bounded by the proved third-block split with
its deterministic residual bounded by 4 delta_1^2 through the anchor
coefficientCutoffLaw_sq_sigmaBar_mul_annealedSigmaStarInvScalarAtScale_sub_one_le
(SigmaBarAnchor.lean).
Shape match against, with every deviation #
The printed display is
E[J(cu_m)] <= C sum_{n=L}^m 3^{-(m-n)} E[J(cu_n) - J(cu_m)] + C sigmabar_L^2 sum_{n=L}^m 3^{-(m-n)} (var[sigma_{L,*}^{-1}(cu_n)] + |mean gap|^2) + C sum_{n=L}^m 3^{-(m-n)} var[sigma_{L,*}^{-1}(cu_n) kappa_L(cu_n)] +[J(cu_{m-1}) 1_B].
The deviations are:
The factor
2onC_badis the printed reabsorption of1/2 E[J(cu_m)], already performed by the proved endpoint.The constant here is
24 C_base <= C.Two amplitudes appear where the manuscript has one.
delta_1is the amplitude of the printed premisee.moment.bound.onmathcalE, carried as a binder withdelta_1 in (0, 1/2];10^9 E^2 gammais the lane's Step-4 amplitude hard-coded by the proved bad-event endpoint. Both amplitudes appear here only because the amplitude bridge --- which produces the fourth-moment premise ats = 1/4from the preceding-error clause --- is not yet proved; that bridge is the recurrence unit's item, not this file's, and adding10^9 E^2 gamma <= delta_1as a binder here would be a smuggled hypothesis. The deviation is inherited from the proved Step-4 endpoint, not introduced here.var[cu_m]absorbed. The printed derivation producesvar[cu_m] + |gap|^2 + var[cu_n]; the printed display carries only thecu_nvariance. The absorption performed here is the printed one:var[cu_m]is then = mterm of the corridor sum (the mean gap vanishes there), and the corridor weight sums to at most3/2.Constants, and the gate's
s.Cis existential with1 <= C; the deliveredCis36 C_basewithC_basethe constant of the proved endpoint. The delivered statement decouples the two: the gate binderhgateCis hard-coded at thes = 1/4endpoint, i.e. at the exponent3/4, while the moment premise runs on a freesMomentwith onlyhsMoment : 0 < sMoment. Fors < 1/4the delivered gate is therefore a stronger hypothesis than the printed one, and the printed weaker form is derived inside the proof; the sole consumer usess = 1/4. It makes the delivered statement stronger, not weaker.Regime data. The
Chom,E,epsilonregime binders and the printed window are inherited verbatim from the proved endpoint; they are the corrected Step-4 regime data ofA.3, not new premises.
Declaration census #
Eleven of the module's eighteen exported statements live here; the other seven
live in InitialJLBoundIntegrability.lean. Ten private helpers live here.
References #
- ABK26, Section 3.5, proof of
p.combine.under.S, Step 1.
The hQlr/hRlr clauses of
coefficientCutoffLaw_integral_descendantsAverage_coarseBlockMatrixVariationSq_le,
discharged unconditionally. The sigma_*^{-1} fluctuation is bounded by a
deterministic constant at every cube, because the lower-right envelope is 4 d nu⁻¹ with no event.
The hQll/hRll clauses of
coefficientCutoffLaw_integral_descendantsAverage_coarseBlockMatrixVariationSq_le,
discharged unconditionally. The sigma_*^{-1}kappa fluctuation is bounded by
(4 d nu⁻¹ E(R) + c)^2, a quadratic polynomial in the integrable envelope.
Integrability of one descendant summand of the coarse-matrix variation at the coefficient cutoff law.
The hLHS clause of
coefficientCutoffLaw_integral_descendantsAverage_coarseBlockMatrixVariationSq_le,
discharged unconditionally.
Global integrability of the squared comparison vector at the coefficient cutoff law.
The second block of e.initial.JL.bound at one corridor scale, with every
integrability clause discharged. This is
coefficientCutoffLaw_sigmaBar_mul_integral_descendantsAverage_le
(VarianceSplit.lean) with its five Integrable binders supplied from the
unconditional envelopes above, and with the operator-norm mean gap rewritten as
the printed scalar gap |sigmabar_{L,*}^{-1}(cu_m) - sigmabar_{L,*}^{-1}(cu_n)|^2
through coefficientCutoffLaw_annealedLowerRightGap_eq (VarianceSplit.lean).
The third block of e.initial.JL.bound at the genuine cutoff sample law,
with its integrability discharged. The pointwise third-block split
coefficientCutoffLaw_sigmaBar_mul_vecNormSq_coarseBlockScaleSeparation_le
(VarianceSplit.lean) is integrated against the genuine cutoff law; the
deterministic residual (sigmabar_L sigmabar_{L,*}^{-1}(cu_m) - 1)^2 is
displayed, not bounded, here. It is bounded by 4 delta_1^2 in the final
assembly through the proved anchor
coefficientCutoffLaw_sq_sigmaBar_mul_annealedSigmaStarInvScalarAtScale_sub_one_le.
The second block of e.initial.JL.bound at the genuine cutoff sample
law, summed over the printed corridor, with every integrability clause
discharged. The corridor integral is transferred to the coefficient cutoff law
by the pushforward identity and bounded scale by scale.
The manuscript variance var[sigma_{L,*}^{-1}(cu_n)] is nonnegative.
The manuscript variance var[sigma_{L,*}^{-1}(cu_n) kappa_L(cu_n)] is
nonnegative.
(e.initial.JL.bound) at the genuine cutoff sample law.
The delivered display is
E[J(cu_m)] <= C sum_{n=L}^m 3^{-(m-n)} (E[J(cu_n)] - E[J(cu_m)])
+ C sigmabar_L^2 sum_{n=L}^m 3^{-(m-n)}
(var[sigma_{L,*}^{-1}(cu_n)] + |sigmabar_{L,*}^{-1}(cu_m) - sigmabar_{L,*}^{-1}(cu_n)|^2)
+ C sum_{n=L}^m 3^{-(m-n)} var[sigma_{L,*}^{-1}(cu_n) kappa_L(cu_n)]
+ C delta_1^2 + C_bad (10^9 E^2 gamma)^2,
which is the printed display with its fourth block C E[J(cu_{m-1}) 1_B] already
replaced by the proved corrected Step-4 bad-event bound, and with the + C delta_1^2 mandated. Every deviation is listed in the module docstring.
This is a local Provider theorem and makes no source-node status claim.