UnionSubadditivity #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Response subadditivity at the union display #
The first inequality of the cutoff-union display of ABK26 (proof of
p.homogenization.step) is the deterministic statement
J(square_m, sigmabar_L^{-1/2} e, sigmabar_L^{1/2} e; a_L)
<= avsum_{z in 3^n Z^d cap square_m}
J(z + square_n, sigmabar_L^{-1/2} e, sigmabar_L^{1/2} e; a_L) ,
read at the genuine cutoff sample law and therefore almost surely, since both sides are the measurable representatives of the two literal quantities.
This module carries that step and the recentred corollary,
J(square_m, ...) <= | avsum_z ( J(z + square_n, ...) - E[J(square_n, ...)] ) |
+ E[J(square_n, ...)] ,
which is the shape the two-lane grid concentration endpoint
isTwoTermBigOWith_gridAverage_siteCenteredResponseJ consumes: the first term
is exactly the averaged recentred site response whose two-term weak-Orlicz
relation is proved, and the second is the single number produced by the mean
lane.
The three ingredients, all proved #
Deterministic depth-
ksubadditivity. The nonnegativity of the Chapter 5 defectWeakNormsMaximizer.responseDefectAverageAtScale m n p q a, proved upstream asresponseDefectAverageAtScale_nonneg_of_aelocallyUniformlyEllipticField, is the inequalityJ(square_m) <= descendantsAverageat relative depth(m - n).toNatonce the definition is unfolded.The enumeration of the descendant family by the site family. The depth-
kdescendants ofsquare_mare exactly the site cubessiteCube n uatn = m - kwithuranging overcubeFinset k, which is the manuscript's grid3^n Z^d cap square_min the cube-side units ofProvider/Percolation/Coloring.lean. This is proved below from the index bound of the triadic child recursion plus the two cardinalities3^(d k).The two literal identifications.
Observable.cutoffResponseJ M m L eis the literal parent response off one null set (Observable.ae_forall_cutoffResponseJ_eq_literal), andsiteResponseJ M L n u eis the literal response ofsiteCube n uoff one null set per site (ae_siteResponseJ_eq_responseJ).
Null-set accounting #
The main almost-sure statement spends two events: the parent literal event,
and the single event obtained from the finitely many site literal events by
Filter.eventually_all_finset over cubeFinset (m - n).toNat (a finite set of
cardinality 3^(d (m-n))). Both are consumed in one filter_upwards. The
recentred corollary adds no further event: the identity
gridAverage_siteCenteredResponseJ_eq_sub_integral is pointwise in omega.
References #
- ABK26, proof of
p.homogenization.step. - ABK26, (2.4), definition of
J(U, p, q; a). - ABK26,
e.subaddJ.nosymm, the deterministic response subadditivity.
The grid enumeration of the descendant family #
The grid enumeration. For integer scales n <= m the depth-(m - n)
descendants of square_m are exactly the site cubes siteCube n u with u
ranging over cubeFinset (m - n).toNat; that is, ABK26's grid
3^n Z^d cap square_m in the cube-side units of Provider/Percolation. The
containment is the index bound, and the reverse inclusion is forced by the two
equal cardinalities 3^(d (m - n)).
The descendant average is the grid average. Any real functional of
cubes averaged over the depth-(m - n) descendants of square_m is its own
average over the manuscript grid, indexed by cubeFinset (m - n).toNat.
The deterministic subadditivity step #
Response subadditivity at the union display, deterministically (ABK26,
proof of p.homogenization.step). For every genuine cutoff realization and
every pair of loads, the literal response of the parent cube square_m is at
most the grid average, over 3^n Z^d cap square_m, of the literal responses of
the site cubes.
This is WeakNormsMaximizer.responseDefectAverageAtScale_nonneg_of_aelocallyUniformlyEllipticField
read at the pointwise ellipticity of the cutoff and reindexed by the grid
enumeration; no null set is spent.
The almost-sure statements at the genuine cutoff sample law #
Response subadditivity at the union display (ABK26, proof of
p.homogenization.step). Almost surely under the genuine cutoff sample law,
the measurable parent response at cube scale m is at most the grid average of
the proved site responses at cube scale n, over the manuscript grid 3^n Z^d cap square_m written at relative depth (m - n).toNat.
Two events are spent: the parent literal identification
Observable.ae_forall_cutoffResponseJ_eq_literal, and the finite intersection
over cubeFinset (m - n).toNat of the per-site literal identifications
ae_siteResponseJ_eq_responseJ. This is a Provider result and carries no
source-node status by itself.
The recentred union display (ABK26, proof of p.homogenization.step).
Almost surely under the genuine cutoff sample law, the measurable parent
response at cube scale m is at most the absolute value of the grid average of
the recentred site responses plus the single number E[J(square_n, sigmabar_L^{-1/2} e, sigmabar_L^{1/2} e; a_L)].
The first summand is exactly the random variable of the proved two-lane grid
concentration endpoint isTwoTermBigOWith_gridAverage_siteCenteredResponseJ,
and the second is the quantity iterated by the mean lane. The split is the
proved pointwise identity gridAverage_siteCenteredResponseJ_eq_sub_integral,
whose mean identification is
integral_siteResponseJ_eq_integral_cutoffResponseJ; no further null set is
spent beyond the two of the previous theorem, and no integrability binder is
needed for the inequality. Disclosure: absent such a binder the Bochner
integral in the statement is the convention 0 whenever
Observable.cutoffResponseJ M n L e is not integrable, and the bound then
degenerates to the (still true) bound by the unrecentred grid average; the
integrability that makes this term the genuine expectation E[J(square_n..)]
is produced by the proved integrable_cutoffResponseJ_of_precedingError and is
bound only in integral_gridAverage_siteCenteredResponseJ_eq_zero below.