High-contrast homogenization: Provider.Selection.RoundedHops

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

Rounded projective hops

This file proves the any-pair form of l.projective.step. The normalized square roots have least singular value one, entrywise rounding is a uniformly small perturbation, and projective distance controls the two normalized cross maps. No absolute eccentricity is assumed.

noncomputable def HCPolySupport.HighContrast.Selection.normalizedRoot {d : ℕ} (m : Mat d) : Mat d

The normalized square root 𝒛(m)=|m⁻¹|¹⁄²m¹⁄², the matrix the rounding of s.scale.selection rounds.

Equations

• HCPolySupport.HighContrast.Selection.normalizedRoot m = √(HCPolySupport.HighContrast.specBound m⁻¹) • HCPolySupport.HighContrast.matSqrt m

theorem HCPolySupport.HighContrast.Selection.normalizedRoot_eq {d : ℕ} (m : Mat d) : normalizedRoot m = √(specBound m⁻¹) • matSqrt m

The defining equation for the normalized square root.

theorem HCPolySupport.HighContrast.Selection.norm_inv_roundedGrid_le {d : ℕ} [NeZero d] {l : ℤ} (hl : ↑(kZero d) ≤ l) {m : Mat d} (hm : Matrix.PosDef m) : ‖(roundedGrid l m)⁻¹‖ ≤ 101 / 100

The absolute inverse bound in e.rounded.grid.bounds.

theorem HCPolySupport.HighContrast.Selection.norm_roundedGrid_le {d : ℕ} [NeZero d] {l : ℤ} (hl : ↑(kZero d) ≤ l) {m : Mat d} (hm : Matrix.PosDef m) : ‖roundedGrid l m‖ ≤ 100 / 99 * witnessEccentricity m

The absolute grid bound in e.rounded.grid.bounds.

noncomputable def HCPolySupport.HighContrast.Selection.hopConstant (d : ℕ) (chop : ℝ) : ℝ

The explicit rounded-hop constant used below.

Equations

• HCPolySupport.HighContrast.Selection.hopConstant d chop = (1 + 2 * (51 / 50 * Real.exp chop)) ^ (2 * d)

theorem HCPolySupport.HighContrast.Selection.rounded_projective_hop {d : ℕ} (hd : 2 ≤ d) {chop : ℝ} {l : ℤ} (hl : ↑(kZero d) ≤ l) {m₀ m₁ : Mat d} (h₀ : Matrix.PosDef m₀) (h₁ : Matrix.PosDef m₁) (hdist : projDist m₀ m₁ ≤ chop) : gridRatio (roundedGrid l m₀) (roundedGrid l m₁) ≤ hopConstant d chop

The general any-pair rounded-hop bound.

theorem HCPolySupport.HighContrast.Selection.exists_hopConstant {d : ℕ} (hd : 2 ≤ d) (chop : ℝ) : ∃ (Khop : ℝ), 1 ≤ Khop ∧ ∀ (l : ℤ), ↑(kZero d) ≤ l → ∀ (m₀ m₁ : Mat d), Matrix.PosDef m₀ → Matrix.PosDef m₁ → projDist m₀ m₁ ≤ chop → gridRatio (roundedGrid l m₀) (roundedGrid l m₁) ≤ Khop

Existence of a single rounded-hop constant, in the exact any-pair form consumed by the frozen short-hop theorem.

theorem HCPolySupport.HighContrast.Selection.rounded_witnessEccentricity_eq_exp {d : ℕ} [NeZero d] {m : Mat d} (hm : Matrix.PosDef m) : witnessEccentricity m = Real.exp (projDist 1 m)

The witness identity for the eccentricity of a rounded geometry.

def HCPolySupport.HighContrast.Selection.witnessGridConstant (d : ℕ) : ℝ

A dimension-only constant for the identity-grid witness bound.

Equations

• HCPolySupport.HighContrast.Selection.witnessGridConstant d = 2 ^ (2 * d)

theorem HCPolySupport.HighContrast.Selection.witnessGridConstant_eq (d : ℕ) : witnessGridConstant d = 2 ^ (2 * d)

The defining equation for the identity-grid constant.

theorem HCPolySupport.HighContrast.Selection.gridRatio_roundedGrid_one_le {d : ℕ} (hd : 2 ≤ d) {l : ℤ} (hl : ↑(kZero d) ≤ l) {m : Mat d} (hm : Matrix.PosDef m) : gridRatio (roundedGrid l m) 1 ≤ witnessGridConstant d * (1 + witnessEccentricity m) ^ (2 * d)

The comparison constant between a rounded geometry and the Euclidean grid.