High-contrast homogenization: Provider.ShortHop.PathStep

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

The candidate of the short test

The candidate witness of p.successful.short.bridge is the next point on the fixed constant-speed projective path from the current witness to the canonical metric of the old grid's terminal block: the path point at parameter min{c_hop/d_pr, 1}, and the endpoint itself when the two projective classes already agree. Two of the three candidate clauses of the proposition are proved here — the candidate is a positive witness, and the projective jump to it is at most the hop length. The third, the bound on the cross-grid factor, is the hop distortion read at those two facts.

The path point m(θ) = m₀^{1/2}(m₀^{-1/2}m₁m₀^{-1/2})^θm₀^{1/2} is a congruence of the real power of the normalized pair, so normalizing it by m₀^{-1/2} gives back that real power exactly. Positive definiteness is then the positive definiteness of the real power carried across the congruence, and the printed form of the projective distance — half the sum of the logarithms of the sizes of the normalized pair and of its inverse — turns the constant-speed bound into the two size bounds of the real power. This is where the path is constant speed: each of the two logarithms is multiplied by θ, so the distance is at most θ times the distance to the endpoint.

The zero branch costs nothing: the candidate is the endpoint, and the distance to it is the vanishing distance itself.

The path point as a congruence

theorem HCPolySupport.HighContrast.ShortHop.normalize_projPath {d : ℕ} {m0 m1 : Mat d} (h0 : Matrix.PosDef m0) (theta : ℝ) : matSqrt m0⁻¹ * projPath m0 m1 theta * matSqrt m0⁻¹ = matPow theta (matSqrt m0⁻¹ * m1 * matSqrt m0⁻¹)

Normalizing the path point returns the real power. The path point is the congruence of (m₀^{-1/2}m₁m₀^{-1/2})^θ by m₀^{1/2}, and conjugating back by m₀^{-1/2} undoes it.

The constant-speed bound

The candidate

theorem HCPolySupport.HighContrast.ShortHop.posDef_canonicalMetric {d : ℕ} {E : BlockMat d} (hE : Matrix.PosDef (toFullBlockMat E)) : Matrix.PosDef (canonicalMetric E)

The canonical metric of a positive definite doubled block is a positive witness.