High-contrast homogenization: Entry.Multiscale.Global.FiniteRun

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

The generic finite run and the projective metric

The generic stopping and telescoping facts for a potential with a per-step charge (p.global.selection, e.global.selection.count), the elementary identities of detIncrement and synchCharge, and the projective-metric layer (e.scale.selection.canonical.metric, e.global.selection.metric.loss, e.global.selection.metric.comparison): positive definiteness of the canonical metric, symmetry and the triangle inequality, and the two canonical-metric comparisons (log-determinant and Loewner sandwich).

§B Generic finite run (p.global.selection)

theorem HCPolySupport.HighContrast.Multiscale.exists_stop_of_potential (Φ charge : ℕ → ℝ) (stop : ℕ → Prop) (c Bud : ℝ) (hc : 0 < c) (hΦ : ∀ (i : ℕ), 0 ≤ Φ i) (hstep : ∀ (i : ℕ), (∀ j ≤ i, ¬stop j) → Φ (i + 1) - Φ i ≤ -c + charge i) (hbud : ∀ (M : ℕ), (∀ j < M, ¬stop j) → ∑ i ∈ Finset.range M, charge i ≤ Bud) : ∃ i ≤ ⌈(Φ 0 + Bud) / c⌉₊, stop i

e.global.selection.count-p.global.selection, abstract: a nonnegative potential decreasing by c per continuing step up to a charge whose running sum is bounded by Bud stops within ⌈(Φ 0 + Bud)/c⌉₊ steps.

§C Matrix geometry (p.global.selection)

theorem HCPolySupport.HighContrast.Multiscale.explicitCanonicalMetric_posDef {d : ℕ} (F : BlockMat d) (hFs : IsSymmetricBlockMat F) (hF : Book.Ch02.BlockPosDef F) : Matrix.PosDef (explicitCanonicalMetric F)

explicitCanonicalMetric F is positive definite for a symmetric positive block F (e.scale.selection.canonical.metric); specialises Geometry.explicitCanonicalMetric_posDef, trivial for d = 0.

theorem HCPolySupport.HighContrast.Multiscale.projectiveDistance_triangle {d : ℕ} (m₀ m₁ m₂ : Mat d) (h₀ : Matrix.PosDef m₀) (h₁ : Matrix.PosDef m₁) (h₂ : Matrix.PosDef m₂) : projectiveDistance m₀ m₂ ≤ projectiveDistance m₀ m₁ + projectiveDistance m₁ m₂

Triangle inequality for projectiveDistance on positive definite matrices (p.global.selection).

theorem HCPolySupport.HighContrast.Multiscale.explicitCanonicalMetric_projectiveDistance_le_logDet {d : ℕ} (F G : BlockMat d) (hFs : IsSymmetricBlockMat F) (hF : Book.Ch02.BlockPosDef F) (hGs : IsSymmetricBlockMat G) (hG : Book.Ch02.BlockPosDef G) (hGF : BlockMatLoewnerLE G F) : projectiveDistance (explicitCanonicalMetric F) (explicitCanonicalMetric G) ≤ 1 / 2 * (blockLogDet F - blockLogDet G)

e.global.selection.metric.loss: for positive blocks G ≤ F, d_pr([m(F)],[m(G)]) ≤ ½ log (det F / det G). Monotonicity and homogeneity of the matrix geometric mean in explicitCanonicalMetric, and the 2d eigenvalues of G^{-1/2} F G^{-1/2}.

theorem HCPolySupport.HighContrast.Multiscale.explicitCanonicalMetric_projectiveDistance_le_of_deltaSandwich {d : ℕ} (F G : BlockMat d) (δ : ℝ) (hδ : δ ∈ Set.Ico 0 1) (hFs : IsSymmetricBlockMat F) (hF : Book.Ch02.BlockPosDef F) (hGs : IsSymmetricBlockMat G) (hG : Book.Ch02.BlockPosDef G) (h₁ : BlockMatLoewnerLE (blockScale (1 - δ) F) G) (h₂ : BlockMatLoewnerLE G (blockScale (1 + δ) F)) : projectiveDistance (explicitCanonicalMetric F) (explicitCanonicalMetric G) ≤ 1 / 2 * Real.log ((1 + δ) / (1 - δ))

e.global.selection.metric.comparison: a δ-sandwich moves the canonical metric by at most ½ log((1+δ)/(1-δ)); same statement as explicitCanonicalMetric_projectiveDistance_le_of_sandwich in HCPoly/Entry/InitialFixedGridScale.lean, proved here from BlockGeometricMean.sandwich.

theorem HCPolySupport.HighContrast.Multiscale.blockLogDet_le_of_sandwich {d : ℕ} (F G : BlockMat d) (δ : ℝ) (hδ : 0 ≤ δ) (hFs : IsSymmetricBlockMat F) (hF : Book.Ch02.BlockPosDef F) (hGs : IsSymmetricBlockMat G) (hG : Book.Ch02.BlockPosDef G) (h₂ : BlockMatLoewnerLE G (blockScale (1 + δ) F)) : blockLogDet G ≤ blockLogDet F + 2 * ↑d * Real.log (1 + δ)

p.global.selection: G ≤ (1+δ) F raises the log-determinant by at most 2d log(1+δ).