High-contrast homogenization: Provider.ShortHop.Eccentricity

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

The witness eccentricity is the exponential of the projective distance

The hop-index bootstrap e.global.selection.eccentricity reads the identity

d_pr([I],[μ]) = ½ log(|μ| |μ^{-1}|) = log 𝔢_q

and turns the prefix bound d_pr([I],[μ_i]) ≤ i c_hop into the eccentricity bound 𝔢_{q_i} ≤ e^{i c_hop}, hence into a bound on the boundary constant B_q = C_d 𝔢_q ζ_g.

The identity is immediate in the encoding used here. The projective distance is half the sum of the logarithms of the two relative sizes, the relative size of a positive witness against the identity is its spectral size, the relative size of the identity against it is the spectral size of its inverse, and the witness eccentricity is the square root of the product of the two. The square root halves the logarithm, which is exactly the factor the projective distance carries.

Nothing in this file mentions a grid: the eccentricity is a function of the witness alone, as the carrier layer records.

The relative size against the identity

theorem HCPolySupport.HighContrast.ShortHop.relSize_one_right {d : ℕ} (X : Mat d) : relSize X 1 = ‖X‖

Measuring a matrix against the identity reads off its spectral size.

The eccentricity identity

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

The logarithm of the witness eccentricity is the projective distance to the identity (the display of e.global.selection.eccentricity).

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

The witness eccentricity is the exponential of the projective distance to the identity.

theorem HCPolySupport.HighContrast.ShortHop.witnessEccentricity_le_exp {d : ℕ} [NeZero d] {m : Mat d} (hm : Matrix.PosDef m) {t : ℝ} (h : projDist 1 m ≤ t) : witnessEccentricity m ≤ Real.exp t

The prefix bound on the eccentricity. A witness within projective distance t of the identity has eccentricity at most e^t.

theorem HCPolySupport.HighContrast.ShortHop.boundaryConst_le_exp {d : ℕ} [NeZero d] {Cd g : ℝ} (hCd : 0 ≤ Cd) (hg : g < 1) {m : Mat d} (hm : Matrix.PosDef m) {t : ℝ} (h : projDist 1 m ≤ t) : boundaryConst Cd g m ≤ Cd * Real.exp t * zetaG g

The prefix bound on the boundary constant. Since B_q = C_d 𝔢_q ζ_g, the eccentricity bound is a bound on the boundary constant.