High-contrast homogenization: Provider.Regularity.FiniteAffineBestFitBounds

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

Finite affine best-fit slope bounds

This module packages the adjacent, all-pair, and terminal slope consequences of the finite best-fit error induction.

theorem HCPolySupport.HighContrast.exists_scalarIdentityFiniteAffineBestFitInductionConstants (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 → ∀ (k : ℤ) (hk : k ∈ Finset.Icc n m) (b : Vec d), finiteAffineBestFitError a k m ⋯ b ≤ C * delta * euclideanNorm ((finiteAffineBestFitSlope a k m ⋯) b) ∧ (∀ (hkm : k < m), euclideanNorm ((finiteAffineBestFitSlope a (k + 1) m ⋯) b - (finiteAffineBestFitSlope a k m ⋯) b) ≤ C * delta * euclideanNorm ((finiteAffineBestFitSlope a k m ⋯) b)) ∧ (∀ (j : ℤ) (hj : j ∈ Finset.Icc n m), j ≤ k → (1 - C * delta) ^ (k - j).toNat * euclideanNorm ((finiteAffineBestFitSlope a j m ⋯) b) ≤ euclideanNorm ((finiteAffineBestFitSlope a k m ⋯) b) ∧ euclideanNorm ((finiteAffineBestFitSlope a k m ⋯) b) ≤ (1 + C * delta) ^ (k - j).toNat * euclideanNorm ((finiteAffineBestFitSlope a j m ⋯) b)) ∧ (k = m → euclideanNorm ((finiteAffineBestFitSlope a m m ⋯) b - b) ≤ C * delta * euclideanNorm b)

Shared constants for finite best-fit error, adjacent slope control, all-pair multiplicative slope bounds, and terminal slope closeness.