High-contrast homogenization: Provider.Regularity.FiniteAffineSlopeFamily #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
Valid finite affine slope families #
This module records the source-proved forward best-fit slope bounds and a joint family of proof-gated inverse matrices. It deliberately contains no same-vector comparison between inverse matrices at different scales.
structure
HCPolySupport.HighContrast.IsFiniteAffineSlopeFamily
{d : ℕ}
[NeZero d]
(a : Book.Ch02.TriadicCoeffFamily d)
(delta C : ℝ)
(n m : ℤ)
(Q : ℤ → Mat d)
:
One finite family of inverse best-fit slope matrices, characterized by two-sided inverse identities and the source-proved forward-slope estimates.
- slopeMatrix_mul_inverse (k : ℤ) (hk : k ∈ Finset.Icc n m) : finiteAffineBestFitSlopeMatrix a k m ⋯ * Q k = 1
- inverse_mul_slopeMatrix (k : ℤ) (hk : k ∈ Finset.Icc n m) : Q k * finiteAffineBestFitSlopeMatrix a k m ⋯ = 1
- flatness_at (k : ℤ) (hk : k ∈ Finset.Icc n m) (e : Vec d) : normalizedAffineCandidateError (originCube d k) (finiteAffineSolution a m (matVecMul (Q k) e)).toH1.toFun ((finiteAffineBestFitIntercept a k m ⋯) (matVecMul (Q k) e)) e ≤ C * delta * euclideanNorm e
- bestFitEnergy_lower (k : ℤ) (hk : k ∈ Finset.Icc n m) (b : Vec d) : ENNReal.ofReal (C⁻¹ * euclideanNorm ((finiteAffineBestFitSlope a k m ⋯) b)) ≤ weightedGradNorm (a.coeffOn (originCube d k)).toCoeffField (openCubeSet (originCube d k)) (finiteAffineSolution a m b).toH1.grad
- bestFitEnergy_upper (k : ℤ) (hk : k ∈ Finset.Icc n m) (b : Vec d) : weightedGradNorm (a.coeffOn (originCube d k)).toCoeffField (openCubeSet (originCube d k)) (finiteAffineSolution a m b).toH1.grad ≤ ENNReal.ofReal (C * euclideanNorm ((finiteAffineBestFitSlope a k m ⋯) b))
- bestFitSlope_lower (j : ℤ) (hj : j ∈ Finset.Icc n m) (k : ℤ) (hk : k ∈ Finset.Icc n m) : j ≤ k → ∀ (b : Vec d), (1 - C * delta) ^ (k - j).toNat * euclideanNorm ((finiteAffineBestFitSlope a j m ⋯) b) ≤ euclideanNorm ((finiteAffineBestFitSlope a k m ⋯) b)
- bestFitSlope_upper (j : ℤ) (hj : j ∈ Finset.Icc n m) (k : ℤ) (hk : k ∈ Finset.Icc n m) : j ≤ k → ∀ (b : Vec d), euclideanNorm ((finiteAffineBestFitSlope a k m ⋯) b) ≤ (1 + C * delta) ^ (k - j).toNat * euclideanNorm ((finiteAffineBestFitSlope a j m ⋯) b)