High-contrast homogenization: Provider.Regularity.FiniteAffineBestFitEnergy

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

Finite affine best-fit energy comparison

This module proves the fixed-boundary, pre-inverse energy comparison between the finite affine solution on an inner centered cube and its canonical best-fit slope.

theorem HCPolySupport.HighContrast.exists_scalarIdentityFiniteAffineBestFitEnergyConstants (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), finiteCenteredCubeSolutionEnergy a m (finiteAffineCubeSolution a m b) k ≤ C * euclideanNorm ((finiteAffineBestFitSlope a k m ⋯) b) ∧ euclideanNorm ((finiteAffineBestFitSlope a k m ⋯) b) ≤ C * finiteCenteredCubeSolutionEnergy a m (finiteAffineCubeSolution a m b) k

On a sufficiently good finite row, the inner energy of a fixed-boundary affine solution is comparable in both directions to its current best-fit slope. This statement is deliberately prior to, and independent of, any inverse slope family.