High-contrast homogenization: Entry.Response.Core.AnnealedMeanDrift #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
The annealed mean under drift #
This file compares the annealed block mean of the recentred coefficients with the adapted mean,
bounding the drift between them, and shows the annealed block of respCoeffMinus (respectively
respCoeffPlus) agrees with the adapted block once evaluated on the adapted cell. It proves the
monotonicity of the block congruence and of the block scaling under the Loewner order, the positive
definiteness and symmetry of the block mean respM0, the scalewise bound on the response source
load from a Loewner hypothesis, and the two-regime evaluation of a tail sum split at the cutoff
between recent and older scales. It serves p.response.transfer.
The general-cell annealed shear identity, minus sign
(p.response.transfer at an arbitrary adapted cell):
E[A(V; a - g)] = G^t E[A(V; a)] G. At V = respCell jStar F t the right-hand side is
respEhatMinus P jStar F t; the point of this form is that it holds at every subcell
adaptedCellAtCenter (respGrid jStar F) k z, which is what respSourceLoad sums over.
The general-cell annealed shear identity, plus sign
(p.response.transfer): E[A(V; a^t + g)] = D G^t E[A(V; a)] G D. At
V = respCell jStar F t the right-hand side is respEhatPlus P jStar F t.
Round 1c: the k ≥ j_* branch — the determinant-drift Loewner comparison. #
The k ≥ j_* Loewner comparison (p.response.transfer): for j_* ≤ k ≤ t the
generation-k annealed block is dominated by (1 + 3^{ρ(t-k)} D_{q,j_*}(t)) E_t. This is the
"telescope the mean increments and use 3/2 > (1-γ)/8" step, in Loewner form.
Round 1c: the two-regime geometric summation of L_s. #
The printed split of L_s at k = j_* (p.response.transfer): a family that
is geometric with ratio r₁ below the crossover N and geometric with ratio r₂ in the
excess n - N above it is summable, with the two regimes contributing separately.
Round 1c: the k < j_* branch — the annealed source estimate in the E_s scale. #
Adapted cells are nested in the generation (p.response.transfer).
The k < j_* per-cell bound (p.response.transfer): the annealed block of any
aligned adapted cell is dominated by C Π e(m)^2 3^{γ(j_*-k)_+} E_s. This is the printed
"the source estimate... bound the remaining sum by C E_s", before the summation: the source
estimate Adapter.aligned_source_bound lands on the reference block E, and the reference
normalization Annealed.adaptedMean_refBlock_normalization converts E into E_s at the
cost Π e(m), which is exactly the factor the second inequality of
e.response.source.smallness is designed to absorb.
Scale-wise form of h7_respSourceLoad_le_of_loewner: the Loewner bound on the annealed
block is allowed to depend on the generation, which is what the printed split at k = j_*
(p.response.transfer) needs. It also records the summability of the generation
summands of L_s, which the same hypotheses give and without which the tsum defining L_s is
the junk value of a divergent series.
Nonnegativity of the profile at a single generation pair, extracted from the
inline argument (HCPoly/Entry/OneGridPropagation.lean).