High-contrast homogenization: Provider.Regularity.FiniteLipschitzCoreRecurrence

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

Finite centered-cube energy recurrence

This module proves the finite energy recurrence from the shared analytic and terminal estimates.

theorem HCPolySupport.HighContrast.FiniteLipschitzCoreInternal.finiteLipschitzTopAffineErrorSum_le {d : ℕ} (a : Book.Ch02.TriadicCoeffFamily d) (m : ℤ) (u : Book.Ch03.CubeSolution (originCube d m) a) (N : ℕ) : ∑ j ∈ Finset.Ioc (m - ↑N) m, finiteLipschitzAffineErrorRow a m u j ≤ ↑N * (3 ^ N * ↑((3 ^ d) ^ N)) * finiteLipschitzAffineErrorRow a m u m

theorem HCPolySupport.HighContrast.FiniteLipschitzCoreInternal.exists_finiteLipschitzEnergyRecurrenceConstant (d : ℕ) [NeZero d] (s : ℝ) (hs : 0 < s) (hs_lt : s < 1 / 2) : ∃ (C : ℝ), 1 ≤ C ∧ ∀ (a : Book.Ch02.TriadicCoeffFamily d) (n m : ℤ) (u : Book.Ch03.CubeSolution (originCube d m) a), n ≤ m → ScalarIdentityGoodMaxOnInterval a s 1 n m → ∀ h ∈ Finset.Icc n m, finiteLipschitzEnergyRow a m u h ≤ C * finiteLipschitzEnergyRow a m u m + C * ∑ j ∈ Finset.Ioc h m, scalarIdentityWeakError a s j * finiteLipschitzEnergyRow a m u j

theorem HCPolySupport.HighContrast.exists_scalarIdentityFiniteEnergyRecurrenceConstant (d : ℕ) [NeZero d] (s : ℝ) (hs : 0 < s) (hs_lt : s < 1 / 2) : ∃ (C : ℝ), 1 ≤ C ∧ ∀ (a : Book.Ch02.TriadicCoeffFamily d) (n m : ℤ) (u : Book.Ch03.CubeSolution (originCube d m) a), n ≤ m → ScalarIdentityGoodMaxOnInterval a s 1 n m → ∀ h ∈ Finset.Icc n m, finiteCenteredCubeSolutionEnergy a m u h ≤ C * finiteCenteredCubeSolutionEnergy a m u m + C * ∑ j ∈ Finset.Ioc h m, scalarIdentityWeakError a s j * finiteCenteredCubeSolutionEnergy a m u j

Unit pointwise identity-comparison errors give the finite energy recurrence used by the small-tail closure.