High-contrast homogenization: Provider.Regularity.FiniteAffineSlopeBijective

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

Bijectivity of finite affine best-fit slope maps

This module derives interval-scale bijectivity from the valid same-boundary forward-slope bounds and terminal closeness. No inverse map is used in the argument.

theorem HCPolySupport.HighContrast.exists_scalarIdentityFiniteAffineSlopeBijectiveConstants (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), Function.Bijective ⇑(finiteAffineBestFitSlope a k m ⋯) ∧ IsUnit (Matrix.det (finiteAffineBestFitSlopeMatrix a k m ⋯))

On a sufficiently small GoodMax row, every finite affine best-fit slope map in the interval is bijective and its matrix has unit determinant.