High-contrast homogenization: Entry.Response.Core.EnergyDefectBound #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
The response energy-and-defect estimate #
This file proves the response energy-and-defect estimate response_energy_and_defect
(e.response.energy.and.defect) and the all-scale spectral bound of the recentred block
(p.response.transfer) it rests on, the latter by splitting the bound across scales and comparing
each piece to the Loewner order. It proves the block spectral bound is nonnegative and controlled
by the Loewner order and by the block trace, bounds the mean part of the estimate by the
determinant drift, telescopes the resulting bound over an interval of scales, and shows the
maximal scale ratio rhoMax stays below the response's own scale ratio respRho.
The response energy and defect estimate #
The response energy and defect estimate e.response.energy.and.defect:
0 <= E[J_t^±] = (L^±)^2/2 - 1 <= C kappa_s^{1/2} and
0 <= tau^± <= C(r-1) kappa_s^{1/2}.
Route: Annealed.responseJ_eq_coarseBlock_adapted is AK.HC (2.15) at an adapted cell, so
E[J_t^±] = (L^±)^2/2 - p.q^± = (L^±)^2/2 - 1 (the loads satisfy p.q^± = 1,
p.response.transfer);
(L^-)^2 + (L^+)^2 = 4 e.m_t^{1/2}S_*^{-1}m_t^{1/2}e <= 4 sqrt(theta) (p.response.transfer) and
the
calibrated blocks give the upper bound. The defect bound is 0 <= E_s - E_t <= (r-1)E_t
applied to the same loads, with Annealed.adaptedMean_antitone for E_t <= E_s.
The premises _hε, _hσ are carried: without them 1 ≤ B and jStar ≤ s
are unavailable. The binder names are underscore-prefixed because they do not occur in
the statement's own type; the hypotheses are unchanged and the proof uses them, with no
linter suppression.
Helpers for the Step 5 split #
Eleven lemmas used in the Step 5 split, kept private so that later steps can cite
them without re-deriving them.
The flat representation of a scalar multiple of I_{2d}
(p.response.transfer, the definition of the spectral positive part).
Quadratic forms add along an additive decomposition of the flat representations. This is
the form in which the Step 5 split is fed to BlockMatLoewnerLE
(p.response.transfer).
|H_+| >= 0 (p.response.transfer). The defining set of blockSpecBound
consists of nonnegative reals, so its sInf is nonnegative -- including the junk value 0
on the empty set, i.e. on a block with no Loewner upper bound of the form c I_{2d}.
The attained-infimum lemma for blockSpecBound (p.response.transfer): any
nonnegative c with H <= c I_{2d} bounds |H_+|. The defining set is bounded below by 0,
so csInf_le applies with no further hypothesis.
The subadditive Step 5 bound (p.response.transfer): if the fluctuation part
V^q_{k,t}(z) = E_t^{-1/2}(A_k(z) - Ak)E_t^{-1/2} is at most cv I_{2d} and the mean part
P^q_{k,t} - I_{2d} is at most cm I_{2d}, then the spectral positive part of the
normalized difference is at most cv + cm. This is the only place the two parts are
recombined.
The bounded-supremum lemma for the all-scale maximum
(p.response.transfer). respAllScaleMax is a real sSup over the pairs
(n, z) with n : ℕ -- the scale k = t - n -- and z in the finite index box
triadicIndexBox d n of the scale-k cells inside U_t. The scale index is not
bounded, so the family need not be bounded above; Real.sSup_le covers both cases, since on
an unbounded family the real sSup takes the junk value 0. Consequently a single
nonnegative bound valid at every scale and index bounds M pathwise.
The response window lies above j_* (p.response.transfer): the raw
output places s at least B log_3(2 + Pi) generations above j_*, and B >= B_0 >= 1
while 2 + Pi >= 3, so j_* < s < t.
This is the premise every OneGrid history/profile lemma needs ((j_* : Z) <= n), and it
is not derivable from RawOutput alone: SelectionData.one_le_B0 is stated only for
eps in (0, eps_0] and sigma in (0, eps], so the two range hypotheses hε, hσ must be
carried.
Further helpers for the Step 5 split #
Eleven additional lemmas used in the Step 5 split. They close the mean-part estimate
(mean_part_le_determinantDrift) and supply the two ingredients needed for the fluctuation half
(the
index-box inclusion triadicIndexBox_center_mem and the weight trade
rhoMax_lt_respRho).
Every lemma cited by name is either from Mathlib, an exported declaration of this library,
or one of the
private helpers above.
The operator-norm Loewner envelope of a positive semidefinite doubled block
(p.response.transfer). For N >= 0 the quadratic form is dominated by |N| times the
Euclidean square, so N <= |N| I_{2d} in the Loewner order. This is the step that turns a norm
bound into the blockScale c I witness that blockSpecBound is an infimum over.
blockTrace is additive on blockSub. Auxiliary to the telescoping of
determinantDrift (p.response.transfer).
Congruence preserves the Loewner gap (p.response.transfer): if B <= A and
R > 0, then R^{-1/2} A R^{-1/2} - R^{-1/2} B R^{-1/2} >= 0. This is the pathwise sign that
makes every increment of determinantDrift nonnegative and makes P^q_{k,t} - I_{2d} positive
semidefinite.
The mean part of the all-scale maximum
(p.response.transfer): "The mean part telescopes into the nonnegative increments in
D_{q,j_*}(t); its weight is bounded by the drift weight because rho > (1-gamma)/8."
For j_* <= k <= t,
3^{-rho(t-k)} |(P^q_{k,t} - I_{2d})_+| <= D_{q,j_*}(t).
Route, in order: Annealed.adaptedMean_antitone gives A_t <= A_k, hence P^q_{k,t} >= I_{2d}
(normalizedBlock_gap_posSemidef); blockSpecBound_le_blockTrace replaces the spectral
bound by tr(P^q_{k,t} - I_{2d}); Annealed.normalizedMean_self gives P^q_{t,t} = I_{2d}, so
telescope_Icc writes that trace as sum_{j=k+1}^{t} tr(P^q_{j-1,t} - P^q_{j,t}); every
summand is nonnegative, so the range extends from Icc (k+1) t to Icc (j_*+1) t; and the
weight comparison is rho_gamma = (1+gamma)/2 >= 1/2 > 1/8 >= (1-gamma)/8 together with
0 <= t - j <= t - k.
Geometry and exponents for the fluctuation half #
rho_max < rho (p.response.transfer, "because rho > rho_max"): with
rho_gamma = (1+gamma)/2 and rho_max = gamma + Q^{-1}(d + (1-gamma)/4), the selection bound
4(d+1) <= Q(1-gamma) gives Q^{-1}(d + (1-gamma)/4) < (1-gamma)/2. This is the weight trade
of the fluctuation half of the all-scale maximum.
Helpers for the fluctuation half #
Four further lemmas for the fluctuation half of the all-scale maximum
(p.response.transfer). They are stated against the OneGrid history layer, so they require
the import HCPoly.Entry.Multiscale.OneGrid.HistoryMajorization.
They cite the private helpers triadicIndexBox_center_mem and
rhoMax_lt_respRho.
The fluctuation half of the all-scale maximum #
Auxiliary to the fluctuation half: the summand of respAllScaleMax's fluctuation part at one
scale index
n' and one triadic index z is dominated by the integrand of fluctuationHistory
(p.response.transfer, "the fluctuation part is bounded by the maximum defining
ℋ^fluc_q(t), because rho > rho_max").
The scale j = t - n' lies in [j_*, t] because n' ≤ (t - j_*)⁺; the centre
3^j q z lies in 3^j q Z^d ∩ U_t by triadicIndexBox_center_mem; and the weight is traded
by rhoMax_lt_respRho.