CombineExpectation #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The expectation lane of Step 1 of the corrected combine proposition #
Step 1 of Proposition p.combine.under.S is printed as a chain of
expectations. The two sample-by-sample halves are available separately: the
good-event display
exists_cutoffGoodEvent_cutoffResponseJ_le_preVarianceSplitDisplay
(Provider/Homogenization/CombineGoodEvent.lean) and the bad-event integral
bound exists_relativeCutoff_observationScale_badEvent_bound
(Provider/Homogenization/CombineBadEvent.lean). This module carries the
passage from the first of them to expectations:
- integrability of the response observable
J(cu_n, sigmabar_L^{-1/2} e, sigmabar_L^{1/2} e; a_L)at every observation scale of the printed corridorL <= n <= m, from the pathwise dominationJ <= mathcal E^2(Provider/Homogenization/ResponseCommonDomination.lean) against theGamma_{1/4}control of the squared error; - stationarity (
a.j.frd#stationary): the mean of the response at a depth-(m - n)descendant ofcu_mis the mean at the origin cubecu_n, so the mean of the deterministic defect averageWeakNormsMaximizer.responseDefectAverageAtScale m nis the printed single cube differenceE[J(cu_n)] - E[J(cu_m)]; - subadditivity in expectation:
E[J(cu_m)] <= E[J(cu_{m-1})], which is the first line of the printed chain, obtained from the deterministic depth-one subadditivitye.subaddJ.nosymmthrough the same stationarity conversion; - the indicator split
E[J(cu_{m-1})] = E[J(cu_{m-1}) 1_G] + E[J(cu_{m-1}) 1_B]over the good eventG = B^cwithB = observationScaleBadEvent M L m, the integration of the good-event display overG, and the assembly with the bad-event contribution.
The last public also performs the printed reabsorption of 1/2 E[J(cu_m)],
which is legitimate here precisely because the integrability lane supplies
E[J(cu_m)] < infinity at the same hypotheses.
What this module does not do #
The variance split is not performed: the second and third blocks of the
right-hand side are still the expectations of the deterministic field
quantities coarseMatrixVariationBlock and coarseScaleSeparationBlock over
the good event, carrying one power of sigmabar_L and an avsum, not
sigmabar_L^2 and the two variances of e.initial.JL.bound. The use of the
e.pq.normed normalization inside that split (the passage from 6|q|^2 and
6|p|^2 to sigmabar_L^2), the sandwich, e.annealed.khom.zero,
d.mathcalS.def, and the induction-regime hypotheses of the source node are
all absent here as well; the normalization itself is present, as the binder
he.
References #
- ABK26, Section 3.5, proof of
p.combine.under.S, Step 1, and the corrected Step 4.
The integrability lane #
The response observable is nonnegative and dominated, off one null set, by the
square of the observation-cube homogenization error read from the same common
representative. A Gamma_{1/4} upper-tail bound for that square therefore
gives a first-moment majorant.
Integrability of the cutoff response from a Gamma_{1/4} bound on the
squared error. The observation cube cu_n and the coefficient cutoff scale
L remain separate arguments.
Integrability along the printed corridor. At every observation scale
L <= n <= m the response is integrable under the genuine cutoff sample law.
At the diagonal n = L the datum is the frozen preceding-error clause
itself, through the proved per-site integrability producer; above the diagonal
it is the proved observation-scale finite cover, which merges the two lanes
into a single Gamma_{1/4} envelope -- enough for a first moment, although not
for the two-lane concentration display.
Integrability transports to every site cube of the same scale, because the site observable is the origin observable of the translated sample and the genuine cutoff sample law is translation invariant.
The stationarity conversion (a.j.frd#stationary) #
The descendant average of the literal response is integrable as soon as the origin-cube response at the descendant scale is.
The stationarity conversion of the descendant average. All the
depth-(m - n) descendants of cu_m have the same response mean as the origin
cube cu_n, so the mean of the descendant average is E[J(cu_n)]. This is the
form in which a.j.frd#stationary is used at this consumer.
The deterministic parent-child defect of e.subaddJ.nosymm is integrable
along the corridor.
The printed defect identity. Taking the expectation of the
deterministic depth-(m - n) defect average and using stationarity gives the
printed single-cube difference E[J(cu_n)] - E[J(cu_m)].
Subadditivity of the response in expectation. The deterministic depth-one
subadditivity e.subaddJ.nosymm and the stationarity conversion give the first
line of the printed chain.
The three deterministic blocks of the good-event display #
The first block of the good-event display: the weighted corridor sum of the deterministic parent-child response defects.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The second block of the good-event display: the weighted corridor sum of the
descendant averages of the coarse-matrix variation, the avsum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The third block of the good-event display: the squared coarse scale separation at the parent cube, the constant tail.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The defect block is pointwise nonnegative, by the response subadditivity of
each corridor summand (e.subaddJ.nosymm).
The defect block is integrable once the response is integrable at every
corridor scale (supplied by integrable_cutoffResponseJ_of_precedingError).
The expectation of the first block. Stationarity turns each deterministic defect average into the printed difference of single-cube means.
The indicator split and the assembly #
The expectation lane of Step 1 at the genuine cutoff sample law.
The good-event display is integrated over G = B^c, the split E[J(cu_{m-1})] = E[J(cu_{m-1}) 1_G] + E[J(cu_{m-1}) 1_B] is performed, and the first block is
converted by stationarity into the printed corridor sum of E[J(cu_n)] - E[J(cu_m)]. The reabsorbed energy term of the good-event display appears as
1/2 E[J(cu_m)] on the right, exactly as in the printed proof; the bad-event
contribution is left as the set integral that the proved bad-event endpoint
bounds.
The second and third blocks remain the expectations of the deterministic field
quantities over the good event: their conversion into the two variances of
e.initial.JL.bound is the variance split and is not performed here. Their
integrability over G is a caller obligation.
This is a local Provider theorem and makes no source-node status claim.
The reabsorbed expectation display of Step 1.
Subadditivity in expectation places E[J(cu_m)] below E[J(cu_{m-1})], so the
1/2 E[J(cu_m)] produced by the good-event branch may be reabsorbed -- the
integrability lane is what makes the reabsorption legitimate -- and the
bad-event contribution is replaced by the proved corrected Step-4 bound. The
result is the printed e.initial.JL.bound with its second and third blocks
still in pre-variance-split form.
This is a local Provider theorem and makes no source-node status claim.