High-contrast homogenization: Provider.Regularity.FiniteLipschitzCoreBestFit

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

Finite centered-cube best-fit estimates

This module provides the terminal, integer-rate, one-step, and Caccioppoli best-fit interfaces.

theorem HCPolySupport.HighContrast.exists_scalarIdentityFiniteTerminalBestFitSlopeConstant (d : ℕ) [NeZero d] (s : ℝ) (hs : 0 < s) (hs_lt : s < 1 / 2) : ∃ (C : ℝ), 0 < C ∧ ∀ (a : Book.Ch02.TriadicCoeffFamily d) (k : ℤ) (u : Book.Ch03.CubeSolution (originCube d k) a), scalarIdentityWeakError a s k ≤ 1 → euclideanNorm (finiteCenteredCubeBestFitSlopeAt a k u k) ≤ C * Book.Ch03.h1EnergyNormOnCube (originCube d k) a u.toH1

At the outer scale, the canonical affine best-fit slope is controlled by the solution energy. This is the public slope estimate used when a ruled finite-affine flatness bound is applied to an arbitrary harmonic residual.

theorem HCPolySupport.HighContrast.exists_scalarIdentityFiniteTerminalBestFitErrorConstant (d : ℕ) [NeZero d] (s : ℝ) (hs : 0 < s) (hs_lt : s < 1 / 2) : ∃ (C : ℝ), 0 < C ∧ ∀ (a : Book.Ch02.TriadicCoeffFamily d) (k : ℤ) (u : Book.Ch03.CubeSolution (originCube d k) a), scalarIdentityWeakError a s k ≤ 1 → finiteCenteredCubeBestFitErrorAt a k u k ⋯ ≤ C * Book.Ch03.h1EnergyNormOnCube (originCube d k) a u.toH1

At the outer scale, the canonical best-affine error is controlled by the solution energy.

theorem HCPolySupport.HighContrast.exists_scalarIdentityFiniteBestFitIntegerRateStepConstants (d : ℕ) [NeZero d] (s : ℝ) (hs : 0 < s) (hs_lt : s < 1 / 2) (p : ℕ) (hp : 0 < p) : ∃ (depth : ℕ) (C₀ : ℝ), 0 < C₀ ∧ ∀ (t : ℕ), let N := depth + 2 * p * t + 2; ∃ (C : ℝ), 0 < C ∧ ∀ (a : Book.Ch02.TriadicCoeffFamily d) (m : ℤ) (u : Book.Ch03.CubeSolution (originCube d m) a) (k : ℤ) (hkm : k ≤ m), finiteCenteredCubeBestFitErrorAt a m u (k - ↑N) ⋯ ≤ C₀ * (1 / 3) ^ ((2 * p - 1) * t) * finiteCenteredCubeBestFitErrorAt a m u k hkm + C * scalarIdentityWeakError a s k * finiteCenteredCubeSolutionEnergy a m u k

Parameterized near-unit-rate improvement for the canonical best-affine error, with the replacement error kept explicit.

theorem HCPolySupport.HighContrast.exists_scalarIdentityFiniteBestFitOneStepConstant (d : ℕ) [NeZero d] (s : ℝ) (hs : 0 < s) (hs_lt : s < 1 / 2) : ∃ (N : ℕ), 0 < N ∧ ∃ (C : ℝ), 0 < C ∧ ∀ (a : Book.Ch02.TriadicCoeffFamily d) (m : ℤ) (u : Book.Ch03.CubeSolution (originCube d m) a) (k : ℤ) (hkm : k ≤ m), finiteCenteredCubeBestFitErrorAt a m u (k - ↑N) ⋯ ≤ 1 / 8 * finiteCenteredCubeBestFitErrorAt a m u k hkm + C * scalarIdentityWeakError a s k * finiteCenteredCubeSolutionEnergy a m u k

One fixed-step contraction for the canonical best-affine error. This is the public analytic interface consumed by finite affine flatness induction.

theorem HCPolySupport.HighContrast.exists_scalarIdentityFiniteCaccioppoliAffineConstant (d : ℕ) [NeZero d] (s : ℝ) (hs : 0 < s) (hs_lt : s < 1 / 2) : ∃ (C : ℝ), 0 < C ∧ ∀ (a : Book.Ch02.TriadicCoeffFamily d) (k : ℤ) (u : Book.Ch03.CubeSolution (originCube d k) a) (c : ℝ) (e : Vec d), scalarIdentityWeakError a s k ≤ 1 → finiteCenteredCubeSolutionEnergy a k u (k - 2) ≤ C * (normalizedAffineCandidateError (originCube d k) u.toH1.toFun c e + euclideanNorm e)

Affine Caccioppoli control two centered scales below a cube.