High-contrast homogenization: Entry.Response.Core.ResponseImbalanceComparison #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
The response-imbalance comparison #
This file proves the response-imbalance comparison and the matrix facts behind the
calibrated-blocks estimate e.response.calibrated.blocks: the calibration bundle RespCalibrated
bounds the canonical mean, the geometric mean, and the two centred energies Ehat^∓ of the
recentred coefficients above and below, in terms of the determinant ratio and the canonical
imbalance. It shows the calibration bundle is preserved under congruence of the canonical mean,
that the response correction g is skew, and that the swapped conjugate block is positive
definite, and combines these facts into the comparison between the response imbalance and the
calibration bounds. It also records that the source load L_s^± is a sum of squares against
nonnegative weights, hence nonnegative, and the error-row arithmetic of the cutoff estimate
e.response.cutoff.estimate.
The imbalance comparison #
The imbalance comparison e.response.imbalance.comparison:
1 <= kappa_t <= kappa_s <= r^2 kappa_t with 1 <= r = det E_s / det E_t < e^{d sigma}.
(1 <= r is det E_t <= det E_s, which follows from E_t <= E_s; it is the implicit
side condition of the printed display.)
The first inequality is Analysis.one_le_det_adaptedMean together with the primal-adjoint
order Analysis.adaptedMean_swapConj_le (e.matrix.annealed.sharp.order,
e.matrix.annealed.sharp.order); the middle
one is subadditivity Annealed.adaptedMean_antitone and the eigenvalue-product argument of
e.response.imbalance.comparison; the last is raw.det, since
detIncrement P q s t = log det E_s - log det E_t by definition.
Premises hε, hσ: without them 1 ≤ B and jStar ≤ s are unavailable.
Helpers for the calibrated-blocks estimate #
New private lemmas proved for e.response.calibrated.blocks.
They are inserted here, immediately above response_calibrated_blocks, so that its body can
cite them.
The route they implement: the Riccati sandwich M(E) ≤ E ≤ 𝔡(E)^{1/2}M(E) (p.response.transfer),
the self-duality 𝐑M(F)⁻¹𝐑 = M(F) and the congruence G^t M(F) G = M_0 , and
the two-sided comparison of canonical means that carries the cost √(r(1+ξ)/(1-ξ)).
The swap conjugate of a positive definite full block is positive definite.
A # B ≤ A whenever B ≤ A: the left half of the Riccati sandwich
M(E) ≤ E ≤ 𝔡(E)^{1/2}M(E) (p.response.transfer), applied with B = E^♯ ≤ E.
A ≤ c • B implies A ≤ √c • (A # B): the right half of the Riccati sandwich
(p.response.transfer). Indeed A = A # A ≤ A # (c • B) = √c • (A # B).
Two-sided comparison of canonical means: A ≤ a • F and F ≤ b • A give
M(A) ≤ √(ab) • M(F). This is the congruence cost √(r(1+ξ)/(1-ξ)) of
p.response.transfer: the first argument of the geometric mean is monotone and
the second, 𝐑·⁻¹𝐑, is antitone, so a two-sided comparison is what the mean consumes.
If A ≤ B are positive definite then B ≤ (det B / det A) • A. With A = E_t and
B = E_s this is the comparison E_s ≤ r E_t of e.response.calibrated.blocks, r being the
determinant ratio of p.response.transfer: conjugating by E_t^{-1/2} turns E_t ≤ E_s into 1 ≤ X with
det X = r, and every eigenvalue of such an X is at most det X.
Block-algebra helpers. #
The canonical mean is the geometric mean of F and F# = 𝐑F⁻¹𝐑 in the full carrier.
g = k(M(F)) is skew (p.response.transfer): self-duality of M(F) forces
M_{22}M_{12} + M_{21}M_{22} = 0, which is exactly gᵀ = -g.
G^t M(F) G = M_0 (p.response.transfer).
D commutes with M_0 (p.response.transfer).
Ehat_u^- = G^t E_u G in the full carrier (p.response.transfer).
Ehat_u^+ = D Ehat_u^- D in the full carrier (p.response.transfer).
Upper half of e.response.calibrated.blocks in abstract form: A ≤ k • N, N ≤ c • N_F
and G^t N_F G = M_0 give G^t A G ≤ (C k) • M_0 for any c ≤ C
(e.response.calibrated.blocks).
Lower half of e.response.calibrated.blocks in abstract form: N_F ≤ c • N, N ≤ A
and G^t N_F G = M_0 give C⁻¹ • M_0 ≤ G^t A G for any c ≤ C
(e.response.calibrated.blocks).
The calibrated-blocks estimate #
Nonnegativity of the source load and the cutoff error-row arithmetic #
The source load L_s^± of p.response.transfer is a weighted sum of squares against
nonnegative weights, hence nonnegative. The cutoff estimate e.response.cutoff.estimate
collects its three error rows and the cutoff pairing term under one constant by elementary
arithmetic, using only that every scalar in sight is nonnegative.
The source load L_s is nonnegative: it is a sum over scales of a nonnegative weight
3 ^ (-(3/2) n) times a cell average of a squared sum of square roots.
L_s^- is nonnegative, being the source load of the recentred coefficient a_-.
L_s^+ is nonnegative, being the source load of the adjoint recentred coefficient a_+.