High-contrast homogenization: Geometry.DeterminantLoss #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
Comparison of canonical geometries under determinant loss #
This file proves e.global.selection.metric.loss: for positive doubled blocks
F ≤ E with determinant ratio r = det(E)^{1/d}/det(F)^{1/d}, the Loewner
comparison F ≤ E ≤ r^d F, the two-sided comparison
r^{-d/2} M(F) ≤ M(E) ≤ r^{d/2} M(F) of the canonical metric blocks, the two
imbalance bounds 𝔡(F) ≤ r^d 𝔡(E) and 𝔡(E) ≤ r^{2d} 𝔡(F), and the projective
bound d_pr([m(E)],[m(F)]) ≤ (d/2) log r.
The reference proof opens by saying that every eigenvalue of F^{-1/2}EF^{-1/2}
is at least one and their product is det(E)/det(F), so each of them is at most
that product. In the encoding used here no eigenvalue is ever named: the
largest one is the relative size Λ(F;E), the product is a determinant, and the
sentence is exactly relSize_le_det_div. Everything else is the geometric-mean
toolkit, the sharp rules, and the least-scalar-bound characterization of the
relative size.
The scalar r is carried as a hypothesis-bound real satisfying r^d = det(E)/det(F),
so that only the single power r^d — never a real exponent — occurs inside a
Loewner inequality, and r^{d/2} is the square root of that power. The printed
d-th root is canonDetRatio, and canonDeterminantLoss_canonDetRatio
instantiates the lemma at it.
The file also collects the three steps that e.global.selection.metric.comparison
shares with this lemma: the unconditional upper half E ≤ 𝔡(E)^{1/2} M(E) of the
balance chain, the passage from a scalar bound against M(F) to a bound on
𝔡(F) by squaring, and the step "take the lower-right principal blocks, then
invert" that turns a comparison of canonical metric blocks into a projective
bound on the canonical metrics.
Scalar bookkeeping for the Loewner order #
Square-root arithmetic #
These helpers speak only about abstract nonnegative reals; no later step lets a
linear-arithmetic call see Real.sqrt applied to a matrix expression.
Steps shared with the near-isometric comparison #
The imbalance is a square, hence nonnegative.
The upper half of the balance chain, unconditionally. The reference text
reads it off the definition of 𝔡(E): the positive matrix
C = M(E)^{-1/2} E M(E)^{-1/2} satisfies C ≤ |C| I = 𝔡(E)^{1/2} I. No
comparison between E and E^♯ is needed.
Squaring the largest generalized eigenvalue relative to M(F). A scalar
Loewner bound of F against its own canonical metric block bounds the
imbalance by the square of the scalar.
The lower-right principal blocks, followed by inversion. This is the
step that both e.global.selection.metric.loss and
e.global.selection.metric.comparison take to pass from a symmetric comparison of the
canonical metric blocks to a bound on the projective distance of the canonical
metrics; the passage to the blocks is e.scale.selection.canonical.metric, through
(M(E))₂₂ = m(E)^{-1}.
The comparison in terms of the determinant quotient #
The Loewner comparison produced by a determinant loss, with the
determinant quotient in place of r^d.
Sharp order reversal applied to the Loewner comparison: the reference
text's r^{-d} F^♯ ≤ E^♯. The companion inequality E^♯ ≤ F^♯ is order
reversal of the primal-adjoint involution applied to F ≤ E directly.
The upper comparison of the canonical metric blocks, the right-hand half of the comparison of the canonical metrics after a determinant loss.
The lower comparison of the canonical metric blocks, the left-hand half of the comparison of the canonical metrics after a determinant loss.
The first imbalance bound for the imbalances after a determinant loss,
with the determinant quotient in place of r^d.
The second imbalance bound for the imbalances after a determinant loss,
with the determinant quotient in place of r^d. This is the only place where
the sharp-pair identity e.response.canonical.imbalance is used.
The projective bound e.global.selection.metric.loss, with the
determinant quotient in place of r^d.
The printed form #
The determinant-loss ratio r = det(E)^{1/d}/det(F)^{1/d} of two ordered
blocks.
Equations
- HCPolySupport.HighContrast.canonDetRatio E F = (Matrix.det E / Matrix.det F) ^ (↑d)⁻¹
Instances For
The d-th power of the determinant-loss ratio is the determinant
quotient.
Comparison under determinant loss (e.global.selection.metric.loss).
The scalar r is any nonnegative real whose d-th power is the determinant
quotient; canonDetRatio is the printed choice.
e.global.selection.metric.loss at the printed ratio
r = det(E)^{1/d}/det(F)^{1/d}.