High-contrast homogenization: Entry.Response.Core.AdaptedEuclideanComparison #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
The Euclidean-versus-adapted annealed block comparison #
This file proves the two Euclidean-versus-adapted grid comparisons of HC Lemma 2.15, the E1 and E2
kernels that p.response.transfer uses to normalize its source term. A capped Whitney-type
covering of a cube by maximal adapted cells gives a row-volume bound and a summable total mass;
the geometrically decaying rows below the cap are then controlled by the source bound and
recombined into an annealed-block comparison for the actual capped partition. Two elementary
Loewner-order lemmas — a forward form absorbing a scaled error into a bound, and a reverse form
subtracting one out to isolate a lower bound — turn this partition comparison into the E1
inequality 𝐀hom_{t+ℓ,Id} ≤ (1+C·𝔢(m)·3^{-ℓ})·𝐀hom_{t,q} and the E2 inequality
𝐀hom_{t+ℓ+r,q} ≤ 𝐀hom_{t+ℓ,Id} + C·𝔢(m)·3^{-r}·𝐀hom_{t,q}.
Plan for E1, then E2 (HC).
- Establish identity-grid and integer-translation support, and integrate the source bound for standard cells at arbitrary locations. The bounded-window multiplier is used after translating an aligned ancestor into its window.
- Apply standard Whitney subadditivity to obtain an annealed source estimate for every rounded adapted cell, without inserting an eccentricity factor: the inverse norm of the rounded grid is at most two.
- Tile a Euclidean cube by maximal adapted cells capped at t. The cap has expectation adaptedMean q t by integer stationarity. Lower rows use step 2, with a direct relative inverse-norm bound of order e (the general gridRatio API raises distortion to power 2d and would lose the required dependence). Sum the geometric deficit series, then apply reference normalization. Antitonicity does not bound smaller means by the cap mean; only the cap uses stationarity, and every smaller row uses the source estimate.
- Only after E1 closes, exchange grids for E2, cap at t+ell, and normalize the source error at t. Constants are chosen before every law and metric.
Every lemma is compiled under the package lock with warnings as errors.
No result from the response-transfer skeleton
HCPoly.Entry.Multiscale.ResponseTransferSkeleton is consumed.
The adapted cell of the identity grid at generation j is the centered cube of side
3 ^ j.
Any generation-j standard cell centered at w has a generation-j recentered copy,
centered at some u, that lies inside the generation-J centered cube for j ≤ J; the two
centers differ by an integer translation v at generation J.
The rounded-grid analogue of standard_recenter: a generation-j adapted cell indexed by
w, j ≤ J, has a recentered index u whose cell lies inside the generation-J adapted cell,
and the annealed block over the two cells agrees, since integer translation of an adapted cell
does not change its annealed block under a stationary law.
Averaging a pointwise Loewner bound coarseBlock U a ≤ c * X a * E (a.e. in a, X
integrable) gives the corresponding bound on the annealed block, scaled by the expectation of
X.
The source bound for aligned cells has no eccentricity cost: the local Whitney proof only uses the inverse-norm bound two. Recenter fine cells at J, and use stationarity and monotonicity for coarser cells.
The capped Whitney row bound uses only the inverse norm of the relative matrix. In particular its constant is linear in that norm.
A norm bound ‖q'⁻¹ * q‖ ≤ K transfers to an InverseNormLE bound on q⁻¹ * q' itself, by
cancelling the two grids and applying the operator-norm inequality to the inverse product.
The volume-ratio weights of the maximal adapted q-cells tiling a q'-cell W are
summable and sum to one: the maximal cells are pairwise disjoint and their union covers W up
to a null set.
If each fine row's weight below a cap is bounded by a geometrically decaying multiple D * 3 ^ (t - n) of a base scale, the row-weighted geometric sum over all indices below the cap is
summable and bounded by the total mass D times the geometric series constant, evaluated at the
cap.
A weighted finite sum ∑ w i * f i splits by whether the row index reaches the cap: the
at-cap terms are bounded using the total mass ≤ 1 and the cap bound a, and the below-cap
terms are bounded using the geometric weighted-sum bound T from fine_weight_bound, together
giving a + c * T * b.
The doubled quadratic form v. (1/2) A v is additive in the block matrix A.
The doubled quadratic form v. (1/2) A v is nonnegative when A is positive definite.
The doubled quadratic form v. (1/2) A v scales linearly under scalar multiplication of
A.
The block-matrix specialization of finite_cap_sum, via the quadratic form: a weighted sum
of blocks B i, each Loewner-bounded by A at the cap and by a geometrically decaying multiple
of E below the cap, is itself Loewner-bounded by A + (c * T) • E.
Annealed comparison from the actual capped maximal-cell partition. The parent and every child are open affine cubes with integrable entries.
If B ≤ A + c • E and E ≤ k • A, then B ≤ (1 + c * k) • A: substituting the second
bound into the first and collecting the A terms.
E1, with the unused unit-range assumption omitted from this support export.
The reverse companion of normalize_forward: if A is positive definite, B ≤ M + c • E,
E ≤ k • A, and c * k ≤ δ, then B - δ • A ≤ M.
E2 from the same capped partition, now with standard cells in the adapted parent. The source normalization is still taken at the original generation t.