High-contrast homogenization: Entry.Geometry.GeometryUpdateBounds

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

Bounds for the geometry update

For positive definite m and mStar, the update geometryUpdate ε m mStar is again positive definite. On the branch where m and mStar are not projectively equal, its normalized form is the real CFC power matPow θ (normalizedMat m mStar) with θ = min (ε / projectiveDistance m mStar) 1 ∈ (0, 1], and projectiveDistance m (geometryUpdate ε m mStar) = min ε (projectiveDistance m mStar), so the update advances the projective class of m by exactly the requested step, capped at the distance to mStar. The spectral thresholds specBound and specMin, and their ratio, of a positive CFC power are the corresponding scalar powers of the originals. These are the update-side estimates that do not require the projective-distance separation theorem of HCPoly.Entry.Geometry.ProjectiveMetric; they serve l.projective.step and the step advance of the finite run in p.global.selection.

theorem HCPolySupport.HighContrast.Geometry.matPow_posDef {d : ℕ} {M : Mat d} (hM : Matrix.PosDef M) (θ : ℝ) : Matrix.PosDef (matPow θ M)

A positive matrix has positive real CFC powers for every real exponent.

theorem HCPolySupport.HighContrast.Geometry.specBound_matPow {d : ℕ} {M : Mat d} [NeZero d] (hM : Matrix.PosDef M) {θ : ℝ} (hθ : 0 ≤ θ) : specBound (matPow θ M) = specBound M ^ θ

Positive CFC powers raise the upper spectral threshold to the same scalar power.

theorem HCPolySupport.HighContrast.Geometry.specMin_matPow {d : ℕ} {M : Mat d} [NeZero d] (hM : Matrix.PosDef M) {θ : ℝ} (hθ : 0 ≤ θ) : specMin (matPow θ M) = specMin M ^ θ

Positive CFC powers raise the lower spectral threshold to the same scalar power.

theorem HCPolySupport.HighContrast.Geometry.specSpread_matPow {d : ℕ} {M : Mat d} [NeZero d] (hM : Matrix.PosDef M) {θ : ℝ} (hθ : 0 ≤ θ) : specBound (matPow θ M) / specMin (matPow θ M) = (specBound M / specMin M) ^ θ

The spectral spread of a positive CFC power is the scalar power of the original spread.

theorem HCPolySupport.HighContrast.Geometry.geometryUpdate_of_projectiveEq {d : ℕ} {m mStar : Mat d} (h : ProjectiveEq m mStar) (ε : ℝ) : geometryUpdate ε m mStar = mStar

In the projectively equal branch, the geometry update returns mStar.

theorem HCPolySupport.HighContrast.Geometry.projectiveDistance_pos_of_not_projectiveEq {d : ℕ} {m mStar : Mat d} [NeZero d] (hm : Matrix.PosDef m) (hStar : Matrix.PosDef mStar) (hne : ¬ProjectiveEq m mStar) : 0 < projectiveDistance m mStar

Away from the projectively equal branch, the projective distance is strictly positive.

theorem HCPolySupport.HighContrast.Geometry.geometryUpdate_exponent_mem_Ioc {d : ℕ} {m mStar : Mat d} [NeZero d] (hm : Matrix.PosDef m) (hStar : Matrix.PosDef mStar) (hne : ¬ProjectiveEq m mStar) {ε : ℝ} (hε : 0 < ε) : min (ε / projectiveDistance m mStar) 1 ∈ Set.Ioc 0 1

On the nonequal branch and for positive step size, the printed update exponent lies in (0, 1].

theorem HCPolySupport.HighContrast.Geometry.normalizedMat_geometryUpdate_of_not_projectiveEq {d : ℕ} {m mStar : Mat d} (hm : Matrix.PosDef m) (hne : ¬ProjectiveEq m mStar) (ε : ℝ) : normalizedMat m (geometryUpdate ε m mStar) = matPow (min (ε / projectiveDistance m mStar) 1) (normalizedMat m mStar)

On the nonequal branch, normalizing the update cancels the endpoint square roots and leaves the powered relative matrix.

theorem HCPolySupport.HighContrast.Geometry.geometryUpdate_posDef {d : ℕ} {m mStar : Mat d} (hm : Matrix.PosDef m) (hStar : Matrix.PosDef mStar) (ε : ℝ) : Matrix.PosDef (geometryUpdate ε m mStar)

The geometry update is positive definite for positive endpoints and every real step.

theorem HCPolySupport.HighContrast.Geometry.projectiveDistance_geometryUpdate_eq_min {d : ℕ} {m mStar : Mat d} [NeZero d] (hm : Matrix.PosDef m) (hStar : Matrix.PosDef mStar) {ε : ℝ} (hε : 0 < ε) : projectiveDistance m (geometryUpdate ε m mStar) = min ε (projectiveDistance m mStar)

The positive-step geometry update moves by the smaller of the requested step and the endpoint projective distance.

theorem HCPolySupport.HighContrast.Geometry.projectiveDistance_geometryUpdate_le {d : ℕ} {m mStar : Mat d} [NeZero d] (hm : Matrix.PosDef m) (hStar : Matrix.PosDef mStar) {ε : ℝ} (hε : 0 < ε) : projectiveDistance m (geometryUpdate ε m mStar) ≤ ε

A positive geometry update stays within the prescribed projective distance step.