High-contrast homogenization: Entry.Multiscale.Initial.CanonicalMetric

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

Initialization: the canonical metric, the projective sandwich and the entry radius

The two deterministic kernels A17 and A18 of the initialization route and the entry-radius estimate they prove (p.initial.fixed.grid.scale, the printed "entry-radius estimate"; the geometric-mean monotonicity is p.global.selection). Block plumbing, the projective-distance sandwich, and the identification of the canonical metric of a block matrix with a matrix geometric mean are proved first.

Hermitian symmetry of skewCorrectedForm E h is proved here from block symmetry and the public posDef_lowerRight; HCPoly/Entry/Analysis/ReferenceComparison.lean has no public original for it (its corrected_pos proves the stronger PosDef privately). The two facts that file does export, swapConj_lowerRight and schurSigma_le_corrected, are used directly.

No probability law and no annealed premise enters any statement of this file.

Part 2. Block plumbing

Part 3. The projective-distance sandwich

Part 4. The canonical metric as a geometric mean

Hermitian symmetry of the skew-corrected form

HCPoly/Entry/Analysis/ReferenceComparison.lean exports swapConj_lowerRight and schurSigma_le_corrected; both are used below through those public originals. The one extra fact needed here, Hermitian symmetry of skewCorrectedForm E h, has no public original there (the private corrected_pos of that file proves the stronger PosDef), so it is proved below directly from block symmetry and the public posDef_lowerRight, as a private helper of this file.

theorem HCPolySupport.HighContrast.Multiscale.explicitCanonicalMetric_projectiveDistance_le_of_sandwich (d : ℕ) (hd : 2 ≤ d) (F G : BlockMat d) (hF : IsSymmetricBlockMat F) (hFpos : Book.Ch02.BlockPosDef F) (hG : IsSymmetricBlockMat G) (hGpos : Book.Ch02.BlockPosDef G) (c κ : ℝ) (hc : 0 < c) (hκ : 1 ≤ κ) (hlo : BlockMatLoewnerLE (blockScale c G) F) (hhi : BlockMatLoewnerLE F (blockScale (κ * c) G)) : projectiveDistance (explicitCanonicalMetric F) (explicitCanonicalMetric G) ≤ 1 / 2 * Real.log κ

A17 (kernel). Geometric-mean monotonicity and homogeneity (p.global.selection): cG ≤ F ≤ κcG gives d_pr([m(F)],[m(G)]) ≤ ½ log κ.

theorem HCPolySupport.HighContrast.Multiscale.explicitCanonicalMetric_refBlock_projectiveDistance_le (d : ℕ) (hd : 2 ≤ d) : ∃ (Cgeom : ℝ), 0 < Cgeom ∧ ∀ (E : BlockMat d), IsSymmetricBlockMat E → Book.Ch02.BlockPosDef E → BlockMatLoewnerLE (ofFullBlockMat (toFullBlockMat (blockSwap d) * (toFullBlockMat E)⁻¹ * toFullBlockMat (blockSwap d))) E → projectiveDistance 1 (explicitCanonicalMetric E) ≤ Cgeom * Real.log (2 + 4 * aspectRatio E)

A18 (kernel). The entry radius of the reference block itself : Cgeom depends on d alone.

theorem HCPolySupport.HighContrast.Multiscale.entry_radius (d : ℕ) (hd : 2 ≤ d) : ∃ (Cgeom : ℝ), 0 < Cgeom ∧ ∀ (E A : BlockMat d), IsSymmetricBlockMat E → Book.Ch02.BlockPosDef E → BlockMatLoewnerLE (ofFullBlockMat (toFullBlockMat (blockSwap d) * (toFullBlockMat E)⁻¹ * toFullBlockMat (blockSwap d))) E → Matrix.PosDef (toFullBlockMat A) → BlockMatLoewnerLE (blockScale (1 / 2) (ofFullBlockMat (toFullBlockMat (blockSwap d) * (toFullBlockMat E)⁻¹ * toFullBlockMat (blockSwap d)))) A → BlockMatLoewnerLE A (blockScale 2 E) → projectiveDistance 1 (explicitCanonicalMetric A) ≤ Cgeom * Real.log (2 + 4 * aspectRatio E)

A19. The entry-radius estimate (p.initial.fixed.grid.scale): a block sandwiched between ½𝐑𝐄⁻¹𝐑 and 2𝐄 has canonical metric within C(d) log(2+4Π) of Id.