High-contrast homogenization: Provider.Regularity.FiniteAffineBestFitEnergyENNReal

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

ENNReal finite affine best-fit energy comparison

This module transports the real-valued fixed-boundary energy comparison to the exact weighted-gradient ENNReal carrier used by the finite slope family.

theorem HCPolySupport.HighContrast.exists_scalarIdentityFiniteAffineBestFitEnergyENNRealConstants (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), 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 ∧ 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))

On a sufficiently good finite row, the weighted-gradient norm of a fixed-boundary affine solution is bounded above and below by the ENNReal realization of its current canonical best-fit slope norm.