High-contrast homogenization: Provider.Regularity.FiniteAffineBestFitEnergyGrowth

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

Fixed-boundary finite affine energy growth

This module composes same-boundary best-fit slope growth with the two-sided energy comparison. It is the valid-P replacement for the refuted inverse-map ratio in the energy-growth step of finite excess decay.

theorem HCPolySupport.HighContrast.exists_scalarIdentityFiniteAffineBestFitEnergyGrowthConstants (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 → ∀ j ∈ Finset.Icc n m, ∀ k ∈ Finset.Icc n m, j ≤ k → ∀ (b : Vec d), finiteCenteredCubeSolutionEnergy a m (finiteAffineCubeSolution a m b) k ≤ C ^ 2 * Real.rpow 3 (↑(k - j).toNat / 4) * finiteCenteredCubeSolutionEnergy a m (finiteAffineCubeSolution a m b) j

Under a sufficiently small GoodMax row, the energy of one fixed-boundary finite affine solution grows between two interval scales by at most the source factor 3^((k-j)/4).