High-contrast homogenization: Entry.Geometry.ProjectiveStep

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

Geometric consequences for the projective step

The two lemmas here assemble the already-proved projective metric triangle inequality and exact geometry-update displacement. They correspond to the eccentricity conclusion of l.projective.step (near l.projective.step).

theorem HCPolySupport.HighContrast.Geometry.log_eccentricity_le_add_projectiveDistance {d : ℕ} [NeZero d] {m m' : Mat d} (hm : Matrix.PosDef m) (hm' : Matrix.PosDef m') : 1 / 2 * Real.log (‖m'‖ * ‖m'⁻¹‖) ≤ 1 / 2 * Real.log (‖m‖ * ‖m⁻¹‖) + projectiveDistance m m'

Half-log eccentricity is 1-Lipschitz for the projective distance from the identity.

theorem HCPolySupport.HighContrast.Geometry.log_eccentricity_geometryUpdate_le {d : ℕ} [NeZero d] {m mStar : Mat d} (hm : Matrix.PosDef m) (hStar : Matrix.PosDef mStar) {ε : ℝ} (hε : 0 < ε) : 1 / 2 * Real.log (‖geometryUpdate ε m mStar‖ * ‖(geometryUpdate ε m mStar)⁻¹‖) ≤ 1 / 2 * Real.log (‖m‖ * ‖m⁻¹‖) + ε

The geometry update increases half-log eccentricity by at most the requested step, for every positive ε.