High-contrast homogenization: Provider.Regularity.FiniteLipschitzCoreTerminal

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

Terminal affine estimates for finite large-scale regularity

This module contains the terminal error and slope estimates shared by the energy-recurrence and best-fit branches.

theorem HCPolySupport.HighContrast.FiniteLipschitzCoreInternal.exists_finiteLipschitzAffineErrorEnergyConstant (d : ℕ) [NeZero d] (s : ℝ) (hs : 0 < s) (hs_lt : s < 1 / 2) : ∃ (C : ℝ), 0 < C ∧ ∀ (a : Book.Ch02.TriadicCoeffFamily d) (m : ℤ) (u : Book.Ch03.CubeSolution (originCube d m) a), ∀ k ≤ m, scalarIdentityWeakError a s k ≤ 1 → finiteLipschitzAffineErrorRow a m u k ≤ C * finiteLipschitzEnergyRow a m u k

theorem HCPolySupport.HighContrast.FiniteLipschitzCoreInternal.exists_finiteLipschitzTerminalSlopeConstant (d : ℕ) [NeZero d] (s : ℝ) (hs : 0 < s) (hs_lt : s < 1 / 2) : ∃ (C : ℝ), 0 < C ∧ ∀ (a : Book.Ch02.TriadicCoeffFamily d) (m : ℤ) (u : Book.Ch03.CubeSolution (originCube d m) a), scalarIdentityWeakError a s m ≤ 1 → euclideanNorm (finiteLipschitzBestSlope a m u m) ≤ C * finiteLipschitzEnergyRow a m u m