High-contrast homogenization: Entry.ProjectiveStep

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

The projective step

This proves the exact type of HCPoly/Entry/Statements/ProjectiveStep.lean (near l.projective.step). The source-scale premise is retained; its standing sentence is near e.source.lower.scale. The explicit positive source family is chosen before the geometric constant, and the geometric constant before γ, K, the grid scale, the matrices and the step size. The geometric proof does not use the source-scale premise. Choosing the source family to be one makes no claim about the separate source estimate.

theorem HCPolySupport.HighContrast.Entry.projective_step (d : ℕ) (hd : 2 ≤ d) : ∃ (Csrc : ℝ → ℝ), (∀ γ ∈ Set.Ico 0 1, 0 < Csrc γ) ∧ ∃ (C : ℝ), 0 < C ∧ ∀ γ ∈ Set.Ico 0 1, ∀ (K : ℝ), 1 < K → ∀ (jStar : ℕ), 2 * d ≤ 3 ^ jStar → ⌈Csrc γ * Real.logb 3 (2 * K)⌉ ≤ ↑jStar → ∀ (m mStar : Mat d), Matrix.PosDef m → Matrix.PosDef mStar → ∀ (ε : ℝ), 0 < ε → projectiveDistance m (geometryUpdate ε m mStar) ≤ ε ∧ 1 / 2 * Real.log (‖geometryUpdate ε m mStar‖ * ‖(geometryUpdate ε m mStar)⁻¹‖) ≤ 1 / 2 * Real.log (‖m‖ * ‖m⁻¹‖) + ε ∧ (ε ≤ 1 → gridRatio (Geometry.explicitRoundedGrid jStar m) (Geometry.explicitRoundedGrid jStar (geometryUpdate ε m mStar)) ≤ C)

The three printed projective-step conclusions, with the constant and premise order and arbitrary positive target matrix.