High-contrast homogenization: Provider.Regularity.FiniteAffineSlopeTerminalInverse #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
Terminal inverse slope-matrix closeness #
This module constructs the terminal inverse only from proved bijectivity and transfers terminal forward-map closeness to operator-norm inverse closeness.
theorem
HCPolySupport.HighContrast.exists_scalarIdentityFiniteAffineSlopeTerminalInverseConstants
(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 →
∃ (hbij : Function.Bijective ⇑(finiteAffineBestFitSlope a m m ⋯)),
Book.Ch02.matrixNorm (finiteAffineBestFitSlopeInverseMatrix a m m ⋯ hbij - 1) ≤ C * delta
On a sufficiently small GoodMax row, the proof-gated terminal inverse
best-fit slope matrix differs from the identity by O(delta) in the source
operator norm.