High-contrast homogenization: Entry.Geometry.RoundedGridComparison

Imported from the Apache-2.0 HighContrastHomogenization development at commit 7a13dbcd8d6609264a713373f5c69ceeac870472.

Rounded-grid comparison for bounded projective hops

This module contains the supporting geometric estimates for the rounded-grid comparison used in l.projective.step (near e.rounded.grid.bounds, s.geometry.transport, l.projective.step). The standing source-scale condition near e.source.lower.scale belongs to the main statement, not to these geometric estimates.

theorem HCPolySupport.HighContrast.Geometry.opNorm_roundingError_le_half {d : ℕ} (jStar : ℕ) (m : Mat d) (hj : 2 * d ≤ 3 ^ jStar) : ‖explicitRoundedGrid jStar m - unroundedGrid m‖ ≤ 1 / 2

The exact standing threshold 2*d ≤ 3^jStar gives the printed half-size operator-norm rounding error.

theorem HCPolySupport.HighContrast.Geometry.unroundedGrid_posDef {d : ℕ} [NeZero d] {m : Mat d} (hm : Matrix.PosDef m) : Matrix.PosDef (unroundedGrid m)

The unrounded grid |m⁻¹|^{1/2} m^{1/2} is positive definite on positive matrices.

theorem HCPolySupport.HighContrast.Geometry.opNorm_matSqrt_inv_mul_sqrt_sq {d : ℕ} [NeZero d] {m m' : Mat d} (hm : Matrix.PosDef m) (hm' : Matrix.PosDef m') : ‖matSqrt m⁻¹ * CFC.sqrt m'‖ ^ 2 = specBound (normalizedMat m m')

The squared norm of the noncommuting cross root is the upper relative spectral threshold: multiply by the adjoint, preserving every factor's order.

theorem HCPolySupport.HighContrast.Geometry.opNorm_le_opNorm_of_matLoewnerLE {d : ℕ} {A B : Mat d} (hA : Matrix.PosSemidef A) (hAB : MatLoewnerLE A B) : ‖A‖ ≤ ‖B‖

Loewner comparison of a positive semidefinite real matrix controls its Euclidean operator norm.

theorem HCPolySupport.HighContrast.Geometry.opNorm_inv_le_of_relative_lower {d : ℕ} {m m' : Mat d} (hm : Matrix.PosDef m) (hm' : Matrix.PosDef m') {L : ℝ} (hL : 0 < L) (hlow : MatLoewnerLE (L • m) m') : ‖m'⁻¹‖ ≤ L⁻¹ * ‖m⁻¹‖

Inverse order controls the scalar normalization ratio of the unrounded grids.

theorem HCPolySupport.HighContrast.Geometry.inv_sqrt_eq_matSqrt_inv {d : ℕ} {m : Mat d} (hm : Matrix.PosDef m) : (CFC.sqrt m)⁻¹ = matSqrt m⁻¹

The inverse of the positive CFC square root is the matrix square root of the inverse. This identity involves a single matrix.

theorem HCPolySupport.HighContrast.Geometry.opNorm_unroundedGrid_cross_le {d : ℕ} [NeZero d] {m m' : Mat d} (hm : Matrix.PosDef m) (hm' : Matrix.PosDef m') : ‖(unroundedGrid m)⁻¹ * unroundedGrid m'‖ ≤ Real.exp (projectiveDistance m m')

The unrounded cross map is controlled by the projective distance, without any commutativity assumption on the two positive matrices.

theorem HCPolySupport.HighContrast.Geometry.projectiveDistance_reverse_le {d : ℕ} [NeZero d] {m m' : Mat d} (hm : Matrix.PosDef m) (hm' : Matrix.PosDef m') : projectiveDistance m' m ≤ projectiveDistance m m'

Reversing a positive pair reverses the relative comparison constants, so the projective distance cannot increase.

theorem HCPolySupport.HighContrast.Geometry.projectiveDistance_symm {d : ℕ} [NeZero d] {m m' : Mat d} (hm : Matrix.PosDef m) (hm' : Matrix.PosDef m') : projectiveDistance m m' = projectiveDistance m' m

The projective distance is symmetric on positive matrices.

theorem HCPolySupport.HighContrast.Geometry.opNorm_roundedGrid_cross_le {d : ℕ} [NeZero d] (jStar : ℕ) (hj : 2 * d ≤ 3 ^ jStar) {m m' : Mat d} (hm : Matrix.PosDef m) (hm' : Matrix.PosDef m') : ‖(explicitRoundedGrid jStar m)⁻¹ * explicitRoundedGrid jStar m'‖ ≤ 2 * Real.exp (projectiveDistance m m') + 1

The half-size rounding errors and the existing rounded inverse bound transfer the unrounded cross comparison at the exact standing grid threshold.

theorem HCPolySupport.HighContrast.Geometry.gridRatio_roundedGrid_le_of_projectiveDistance_le (d : ℕ) (hd : 2 ≤ d) : ∃ (C : ℝ), 0 < C ∧ ∀ (jStar : ℕ), 2 * d ≤ 3 ^ jStar → ∀ (m m' : Mat d), Matrix.PosDef m → Matrix.PosDef m' → projectiveDistance m m' ≤ 1 → gridRatio (explicitRoundedGrid jStar m) (explicitRoundedGrid jStar m') ≤ C

One positive constant depending only on the dimension controls both orientations of every rounded hop of projective length at most one.