AnnealedLimitPassage #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The annealed limit passage P . bfAhom_m P = lim_K E[P . bfA_m(cu_K) P] #
Step 6 of l.approximate.recurrence.formula opens with the chain
(e'; e) . bfAhom_{m-h}^{-1/2} bfAhom_m bfAhom_{m-h}^{-1/2} (e'; e)
= P . bfAhom_m P
= lim_{K -> infty} E[ P . bfA_m(cu_K) P ] .
The second equality is what this module supplies, at an arbitrary fixed
doubled load P : BlockVec d (the probe load recurrenceP of e.recurrence.P.def
is only one instance, recorded at the end).
Why the passage is available, and from what #
bfAhom_m is defined in the manuscript, at e.homs.defs, as the
infinite-volume limit lim_{n} E[bfA_m(cu_n)] of the annealed cube matrices.
In this repository that definition is carried by the unique-choice
characterization Annealed.sigmaBar_characterization, read through
annealedLimitBlock as
ApproximateRecurrence.annealedLimitBlock_sigmaBar_characterization: the
doubled annealed matrices of the genuine coefficient cutoff converge, in the
finite dimensional space FullBlockMat d, to annealedLimitBlock (sigmaBar M m).
The passage is therefore not an analytic input: it is the continuity of a fixed doubled quadratic form on a finite-dimensional matrix space, composed with that convergence. Nothing probabilistic is added.
The bridge chain, link by link #
The manuscript writes the finite-volume side as an expectation
E[P . bfA_m(cu_K) P], while the repository's annealed layer carries the
matrix bfAhom_m(cu_K) = E[bfA_m(cu_K)] (Ch04.annealedBlockMatrixAtScale).
The two are identified here in five steps.
blockVecDot_blockMatVecMul_eq_sum--- the doubled quadratic form is the finite bilinear expansionsum_{alpha,beta} P_alpha A_{alpha beta} P_betaoverBlockCoord d. Pure algebra.tendsto_blockVecDot_blockMatVecMul_of_tendsto_toFullBlockMat--- entrywise convergence of block matrices gives convergence of every fixed doubled quadratic form. Pure topology ofPilimits.blockVecDot_annealedBlockMatrix_eq_integral--- because the annealed matrix is defined entrywise by integration, its doubled quadratic form is the expectation of the doubled quadratic form of the coarse matrix. This is the only step with a hypothesis of substance: it needs entrywise integrability. Both halves are CoarseGraining'sCh04.integral_blockVecDot_blockMatVecMul_eq_of_integrable_entriesandCh04.integrable_blockVecDot_blockMatVecMul_of_integrable_entries, fed the provedProvider.Annealed.coefficientCutoffLaw_integrable_blockMatEntry_coarseBlockMatrix.integral_coefficientCutoffLaw_eq_integral_cutoffSampleLaw--- the genuine coefficient law is by definition the pushforward ofcutoffSampleLaw MalongcoefficientCutoff M.nu m, so the expectation can be read on the sample carrierCutoffSample dthat the closure junctions integrate over.coarseBlockMatrix_cubeSet_coefficientCutoff_eq_ch02--- the annealed layer's coarse matrix is built on theSet/RegCoeffFieldcarrier (CoarseGraining.coarseBlockMatrix (cubeSet Q) a.toFun), whereas the proved structural split of Steps 1--3 (LocalizationRecurrenceMesh.exists_localizationRecurrenceMeshSplit_le_descendantsAverage_expanded) states its left-hand side on theDomain/CoeffOncarrier (Ch02.coarseBlockMatrix (cubeDomain Q) ((coefficientCutoffTriadicCoeffFamily M m omega).coeffOn Q)). The two carriers are identified by CoarseGraining'scoarseBlockMatrix_cubeSet_eq_ch02_coarseBlockMatrix_of_aelocallyUniformlyEllipticFieldtogether withCh02.coarseBlockMatrix_eq_ofAEEq, exactly asProvider.Base.AnnealedPlateaualready does for the upper-left block. This link is what makes the finite-volume side of the passage literally the expectation of the split's left-hand side.
What consumers actually use #
Downstream the passage is consumed in its one-sided, finite-volume form
blockVecDot_annealedLimitBlock_le_annealedBlockMatrixAtScale, its expectation readingblockVecDot_annealedLimitBlock_le_integral_coarseBlockMatrix_cutoffSampleLaw, and that reading at the structural split's carrier,blockVecDot_annealedLimitBlock_le_integral_ch02CoarseBlockMatrix:
the annealed limit form is below the annealed cube form at every single
scale, because the annealed cube matrices are Loewner nonincreasing (ABK26,
proved as
Provider.Annealed.coefficientCutoffLaw_blockMatLoewnerLE_annealedBlockMatrixAtScale).
That is what lets a bound proved at one finite grid be transported to the limit
without ever forming a limsup. records the same principle for
e.lower.bound.pre1: a limsup bound implies nothing at any fixed grid, so
the finite-volume display is the one a junction can consume.
References #
- ABK26,
e.homs.defs.U.pre,e.homs.defs. - ABK26,
l.approximate.recurrence.formula, Step 6.
The doubled quadratic form as a finite bilinear expansion #
The doubled bilinear form X . A Y expanded over the doubled coordinate
type BlockCoord d = Fin d + Fin d.
Continuity of a fixed doubled quadratic form #
Continuity of the doubled bilinear form. If a family of block matrices converges entrywise, then its doubled bilinear form at any fixed pair of doubled vectors converges to the form of the limit. Conditional helper: the convergence hypothesis is supplied by the caller.
The passage at the annealed cube matrices #
e.homs.defs at a fixed doubled load. The doubled quadratic forms of the
annealed cube matrices of the genuine coefficient cutoff converge to the
doubled quadratic form of annealedLimitBlock (sigmaBar M m). Unconditional.
The one-sided finite-volume form of the passage. By ABK26 the annealed cube matrices are Loewner nonincreasing in the scale, so the infinite-volume doubled form sits below the annealed doubled form at every single cube scale. Unconditional.
The annealed matrix's quadratic form as an expectation #
The doubled quadratic form of the coarse cube matrix is integrable for the genuine coefficient cutoff law. Unconditional: the entrywise integrability is the proved cutoff moment layer.
e.homs.defs.U.pre at a fixed doubled load. Since the annealed matrix
bfAhom_m(U) = E[bfA_m(U)] is defined entrywise by integration, its doubled
bilinear form is the expectation of the coarse doubled bilinear form.
Unconditional.
The genuine coefficient cutoff law is by construction the pushforward of the
canonical sample law along coefficientCutoff, so its expectations are
expectations over CutoffSample d. Conditional helper: a.e. strong
measurability is supplied by the caller.
The doubled quadratic form of the annealed cube matrix, read on the sample
carrier CutoffSample d that the closure junctions integrate over.
Unconditional.
The passage #
The consumable one-sided form. The infinite-volume doubled quadratic
form is below the finite-volume expectation at every cube scale K. This is
the form in which the passage is used by the closure junctions: a bound proved
at one finite grid transports to the annealed limit with no limsup.
Unconditional.
The same, at the Ch02 carrier of the proved structural split #
The proved split of Steps 1--3 states its left-hand side with
Ch02.coarseBlockMatrix on Ch02.cubeDomain, at the triadic coefficient
family of the cutoff, rather than with the annealed layer's cube-set coarse
matrix. The two agree.
The annealed layer's coarse cube matrix of the genuine cutoff coincides with the Chapter 2 coarse matrix at the cutoff's triadic coefficient family --- the carrier in which the proved structural split of Steps 1--3 is stated. Unconditional.
The consumable one-sided form at the split's carrier. The infinite-volume
doubled quadratic form is below the expectation of the Chapter 2 coarse doubled
form on cu_K at every cube scale K. Unconditional.
The passage at the probe load P and at the split's carrier: the exact
expectation of the left-hand side of
LocalizationRecurrenceMesh.exists_localizationRecurrenceMeshSplit_le_descendantsAverage_expanded
dominates the closure junction's annealed side. Unconditional.