Bridge #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
From averaged local responses to the squared homogenization error #
This module proves the display of ABK26,
avsum_{z in 3^{-h} Zd cap cu_0} J(z + cu_{-h}, sigma0^{-1/2} e, sigma0^{1/2} e; a) <= 3^{2 t h} mathcal E_{t,2,2}(cu_0; a, sigma0)^2,
as a named node, for every depth h in N, every t > 0 and every unit vector
e in R^d.
The aggregation identity the bridge is derived from #
For p = q = 2 CoarseGraining's Ch02.HomogenizationErrorOnCube Q t (.finite 2) (.finite 2) squares to a single geometric aggregate. Writing N(R):= Ch02.normalizedBlockResponseMax a0 for the one-cube quantity max_{|e| = 1} bfJ(R, bfA_0^{-1/2} e, bfA_0^{1/2} e; a) of Definition d.mathcal.E, the p = 2 scale response is the square root of the descendant average of N, so
squaring removes every root and leaves
mathcal E_{t,2,2}(Q; a, a0)^2 = sum_{l = 0}^infty c_{t,2} 3^{-2 t l} avsum_{R at depth l} N(R),
c_{t,2} = 1 - 3^{-2 t},
which is homogenizationErrorOnCube_finite_two_two_sq_eq_tsum below. The
weights c_{t,2} 3^{-2 t l} form a probability density on N, so a single
term of this series would only give the constant c_{t,2}^{-1} 3^{2 t h}, which
degenerates as t -> 0. The sharp constant 3^{2 t h} of the source display
comes from using the whole tail l >= h, together with the monotonicity in the
depth of the averaged responses, which is exactly the subadditivity patching of
ResponseSubadditivity.lean:
avsum_h J <= avsum_l J <= avsum_l N for every l >= h,
sum_{l >= h} c_{t,2} 3^{-2 t l} = 3^{-2 t h}.
Contents #
homogenizationErrorOnCube_finite_two_two_sq_eq_tsum- the aggregation identity above (no summability hypothesis: both sides are0when the series diverges);summable_geometricWeight_mul_descendantsAverage_normalizedBlockResponseMax- the series does converge, by CoarseGraining's uniform descendant bound;
descendantsAverage_responseJ_scalarLoading_le_rpow_mul_homogenizationErrorOnCube_sq- the bridge for an arbitrary root cube;
descendantsAverage_responseJ_scalarLoading_le_rpow_mul_unitCubeHomogenizationError_sq- the same statement against the frozen unit-cube quantity, reached through
the frozen characterization theorem (
Classical.chooseis never unfolded).
- the same statement against the frozen unit-cube quantity, reached through
the frozen characterization theorem (
An abstract tail estimate #
The arithmetic of the bridge is a statement about one nonnegative weighted series and is isolated here, away from the multiscale definitions.
Elementary facts about the geometric weights #
The p = q = 2 aggregation identity #
The exact p = q = 2 aggregation identity for mathcal E. Squaring
the homogenization error at p = q = 2 produces exactly the geometrically
weighted sum, over all depths, of the descendant averages of the one-cube
normalized block responses.
Convergence of the aggregate #
The p = q = 2 aggregate converges for every positive exponent.
The bridge #
The homogenization-error bridge. For a positive scalar background
sigma0, a unit vector e in R^d, a positive exponent t and any depth
h, the unweighted average over the depth-h descendants of the
sigma0-loaded scalar responses is bounded by 3^{2 t h} times the squared
homogenization error of the root cube. This is the display of ABK26.
The bridge against the frozen unit-cube homogenization error. Routed
through the frozen characterization theorem; Classical.choose is never
unfolded.