UnionSiteProducers #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Per-site producers for the grid concentration display #
The Section 3.5 grid concentration display (ABK26, proof of
p.homogenization.step) averages, over the lattice 3 ^ n Z^d cap square_m, the centered response
X_u = J(u + square_n, sigmabar_L^{-1/2} e, sigmabar_L^{1/2} e; a_L) - E[...].
The concentration engine itself is available separately; what it consumes at
each site u is a package of four facts about X_u. This module supplies
that package on the genuine cutoff sample law:
The translated-cube observable and its literal identification. The one measurable coarse-block evaluation
Observable.cutoffResponseJFromCommonCoarseBlock M L Q p qexists for every triadic cubeQ; here it is identified, on one probability-one event and simultaneously in both loads, with the literalResponseJ (cubeSet Q) p qof the actual coefficient cutoff. The proved identification was available only at the origin cube.Cube locality. Every entry of the coarse block matrix of the cutoff on
cubeSet Qis integral-local, hence so is the quadratic-form evaluation; the almost-everywhere passage to the chosen representative is absorbed by the local sigma-field, which is theSubtype.val-comap of theM.P- lower-shell local sigma-field (Cutoff.lowerShellLocalCompletion) and therefore already contains the ambient null sets; the absorption lemma is the provedmeasurableSet_cutoffSampleLocalSigma_of_ae_eq(Provider/BadEvents/LambdaLocal.lean), not a new assumption. At the site cube this gives measurability forcutoffSampleLocalSigma M L (siteRegion n {u}).Centering. The genuine cutoff sample law is invariant under every real translation, and the Chapter 2 response is translation covariant, so the site observable is the origin observable composed with the sample translation. Its mean is therefore the mean at the origin cube, and the recentred variable integrates to zero.
The per-site two-term tail. From a two-term
(Gamma_2, Gamma_{1/2})bound on the mixed-scale homogenization error at the observation cubesquare_nand cutoffa_L, the pathwise dominationJ <= E^2and the square rule for stretched exponentials give a two-term(Gamma_1, Gamma_{1/4})bound for the absolute value of the recentred site response, at the two squared amplitudes. The mean shift is absorbed into the same two lanes through the first-moment bound of each lane.
The last section assembles the four producers: the deterministic mixed
allocation splits each recentred site response into a Gamma_1 lane and a
Gamma_{1/4} lane, both still local for the site's own cube tree and both
centered, and the two-lane grid concentration estimate then produces the
display of ABK26 for every unit direction and every corridor pair L <= n,
at the grid gain 3 ^ (-d k / 2) on both amplitudes.
References #
- ABK26, Proposition
p.homogenization.step. - ABK26, (2.4), definition of
J(U, p, q; a).
Producer 1: the translated-cube observable and its literal value #
The general-cube literal identification of the common coarse-block
response. On one probability-one event, and simultaneously for both loads,
the scalar evaluation of the single measurable coarse-block representative at
an arbitrary triadic cube Q is the literal manuscript quantity J(Q, p, q; a_L). The proved instance of this statement was restricted to the origin
cube.
Producer 2: cube locality #
The function form of the almost-everywhere absorption of the cutoff-sample local sigma-field: a modification on a null set of a locally measurable map is locally measurable, in every codomain.
Every entry of the coarse block matrix of the actual cutoff on a cube is
integral-local. The four block-entry formulas of CoarseGraining express each
entry through the coarse energy Mu, whose locality on the closed cube is
proved.
The translated-cube response observable is cube-local. It reads only
the integral-local information of the cutoff a_L on any region containing the
closed cube.
The closed site cube sits inside the observation region of its own site.
Producer 2. The site response observable reads only the integral-local
information of the cutoff a_L on the cube tree of its own site, which is the
locality hypothesis consumed by the grid concentration engine.
The site observable #
The Section 3.5 per-site response observable: the common coarse-block
evaluation on the site cube u + square_n at the loads
sigmabar_L^{-1/2} e , sigmabar_L^{1/2} e of the manuscript.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The literal value of the site observable. On one probability-one event
the site observable is the manuscript's
J(u + square_n, sigmabar_L^{-1/2} e, sigmabar_L^{1/2} e; a_L).
Producer 3: translation covariance and centering #
Translation covariance of the literal cutoff response. The response of the cutoff on a triadic cube is the response on the concentric origin cube of the translated sample.
The site observable is the origin observable of the translated sample. This is the exact form in which the manuscript's stationarity is used at the site cubes of the grid.
Producer 3, stationarity half. The mean of the site observable does not depend on the site: it is the mean at the origin cube of the same scale.
The recentred site observable of the grid display.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Producer 3, centering half. The recentred site observable integrates to zero, which is the centering hypothesis consumed by the grid concentration engine. Integrability is the only input; it is produced by the per-site tail below.
Producer 4: the per-site two-term tail #
The per-site lane constant at a stretched-exponential exponent: the square
rule of the two-term error bound costs a factor 2, and absorbing the mean
shift into the same lane costs one more first-moment constant.
Equations
Instances For
Producer 4, integrability half. The site observable is integrable, so the centering integral of Producer 3 is available.
Producer 4. The absolute recentred site response carries the
two-term one-sided weak-Orlicz relation at the exponents 1 and 1/4, with
the two amplitudes obtained by squaring the amplitudes of the preceding-error
clause. This is the per-member tail hypothesis consumed by the grid
concentration engine, and it is the un-decayed form of the two amplitudes
printed at ABK26.
The centering identity of Producer 3, with its integrability input supplied by the per-site tail.
Assembly: the grid concentration display #
The averaged quantity is the manuscript's. Because all site means
coincide (Producer 3), the grid average of the recentred site responses is the
grid average of the responses themselves minus the single number
E[J(square_n, sigmabar_L^{-1/2} e, sigmabar_L^{1/2} e; a_L)], which is what
ABK26 subtracts.
The Section 3.5 grid concentration display at the genuine cutoff law
(ABK26, proof of p.homogenization.step).
For every unit direction e and every corridor pair L <= n, the grid average
over 3 ^ n Z^d cap square_m (written at relative depth k = m - n) of the
recentred site responses satisfies the one-sided two-term weak-Orlicz relation
at the exponents 1 and 1/4, with both amplitudes carrying the manuscript's
grid gain 3 ^ (-d k / 2): the Gamma_1 amplitude is a constant times the
square of the linear amplitude of the preceding-error clause, and the
Gamma_{1/4} amplitude is a constant times the square of its rare amplitude.
All constants depend only on d.
The four per-site inputs of the concentration engine are the producers above; the engine itself, the colouring, and the deterministic lane allocation are consumed, not re-derived. This is a Provider endpoint and carries no source-node status by itself.