High-contrast homogenization: Provider.Regularity.FiniteAffineSlopeFamilyExistence

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

Existence of finite affine slope families

This module assembles the proof-gated inverse matrices, best-fit flatness, fixed-boundary energy comparison, and same-boundary forward-slope bounds into one finite affine slope family. The flatness intercept is the attained best-fit intercept of the outer finite solution.

theorem HCPolySupport.HighContrast.exists_scalarIdentityFiniteAffineSlopeFamilyConstants (d : ℕ) [NeZero d] (s : ℝ) (hs : 0 < s) (hs_lt : s < 1 / 2) : ∃ (C : ℝ) (c : ℝ), 1 ≤ C ∧ c ∈ Set.Ioc 0 (2 * C)⁻¹ ∧ ∀ (a : Book.Ch02.TriadicCoeffFamily d) (delta : ℝ) (n m : ℤ), n < m → delta ∈ Set.Ioc 0 c → ScalarIdentityGoodMaxOnInterval a s delta n m → ∃ (Q : ℤ → Mat d), IsFiniteAffineSlopeFamily a delta C n m Q

A sufficiently small good-max row admits a finite affine slope family whose flatness normalization is the attained outer best-fit intercept.