High-contrast homogenization: Entry.Geometry.BridgeEccentricity

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

Eccentricities in the successful short bridge

Ordinary support for p.successful.short.bridge. The logarithmic eccentricity comparison follows from the existing projective triangle inequality, with the identity as its first endpoint. The spectral positivity receipts are discharged inside that metric API on positive matrices.

The scalar bracket lemmas make the positive length explicit. The final bridge must supply it from its choice of L₀ ≥ 1; it is not a new source hypothesis. The dimension instance excludes the empty matrix, whose norm product is zero. All constants in the grid-ratio conclusion precede the coarse exponent and law.

theorem HCPolySupport.HighContrast.Geometry.one_le_norm_mul_norm_inv {d : ℕ} [NeZero d] {m : Mat d} (hm : Matrix.PosDef m) : 1 ≤ ‖m‖ * ‖m⁻¹‖

The condition-number expression has positive base on the source domain.

theorem HCPolySupport.HighContrast.Geometry.log_norm_mul_norm_inv_nonneg {d : ℕ} [NeZero d] {m : Mat d} (hm : Matrix.PosDef m) : 0 ≤ Real.log (‖m‖ * ‖m⁻¹‖)

The logarithm in the bridge hypothesis is nonnegative, with positive argument.

theorem HCPolySupport.HighContrast.Geometry.eccentricity_eq_exp_half_log {d : ℕ} [NeZero d] {m : Mat d} (hm : Matrix.PosDef m) : √(‖m‖ * ‖m⁻¹‖) = Real.exp (1 / 2 * Real.log (‖m‖ * ‖m⁻¹‖))

The square root is the exponential of half the logarithm on the positive domain.

theorem HCPolySupport.HighContrast.Geometry.bracket_nonneg_of_eccentricity {d : ℕ} [NeZero d] {m : Mat d} (hm : Matrix.PosDef m) {c₀ : ℝ} (hc₀ : 0 < c₀) {L : ℕ} (hL : 1 ≤ L) {k jStar : ℤ} {B₀ Pi : ℝ} (hecc : Real.log (‖m‖ * ‖m⁻¹‖) ≤ c₀ / ↑L * (↑k - ↑jStar - ↑⌈B₀ * Real.logb 3 (2 + Pi)⌉)) : 0 ≤ ↑k - ↑jStar - ↑⌈B₀ * Real.logb 3 (2 + Pi)⌉

The eccentricity assumption forces the source-separation bracket to be nonnegative. The coefficient is positive because the length is positive.

theorem HCPolySupport.HighContrast.Geometry.eccentricity_le_exp_of_log_le {d : ℕ} [NeZero d] {m : Mat d} (hm : Matrix.PosDef m) {t : ℝ} (hecc : Real.log (‖m‖ * ‖m⁻¹‖) ≤ t) : √(‖m‖ * ‖m⁻¹‖) ≤ Real.exp t

The first printed eccentricity bound. Dropping the factor one half is legitimate because the exponent is nonnegative.

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

Eccentricity changes by at most the exponential of the projective distance. The positive-definiteness hypotheses feed the attained spectral extrema used by projectiveDistance_triangle and projectiveDistance_one_eq_log_eccentricity.

theorem HCPolySupport.HighContrast.Geometry.eccentricity_le_of_projectiveDistance_le {d : ℕ} [NeZero d] {m mPlus : Mat d} (hm : Matrix.PosDef m) (hmPlus : Matrix.PosDef mPlus) (hpr : projectiveDistance m mPlus ≤ 1) : √(‖mPlus‖ * ‖mPlus⁻¹‖) ≤ Real.exp 1 * √(‖m‖ * ‖m⁻¹‖)

The second eccentricity bound of p.successful.short.bridge.

theorem HCPolySupport.HighContrast.Geometry.exists_gridRatio_bound (d : ℕ) (hd : 2 ≤ d) : ∃ (K₀ : ℝ), 1 ≤ K₀ ∧ ∀ (jStar : ℕ), 2 * d ≤ 3 ^ jStar → ∀ (m mPlus : Mat d), Matrix.PosDef m → Matrix.PosDef mPlus → projectiveDistance m mPlus ≤ 1 → gridRatio (explicitRoundedGrid jStar m) (explicitRoundedGrid jStar mPlus) ≤ K₀

Choose the Whitney distortion constant using dimension alone, before every law and geometry parameter. Enlarging it to at least one preserves the bound.