High-contrast homogenization: Provider.Regularity.FiniteAffineBestFitInduction

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

Finite affine best-fit induction

This module develops the pre-inverse best-fit error and forward-slope estimates used in the finite flatness argument.

noncomputable def HCPolySupport.HighContrast.finiteAffineBestFitError {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) (k m : ℤ) (hkm : k ≤ m) (b : Vec d) : ℝ

Normalized error of the canonical best affine fit to the finite solution posed on Q_m, measured on the inner cube Q_k.

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.HighContrast.finiteAffineBestFitError_nonneg {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) (k m : ℤ) (hkm : k ≤ m) (b : Vec d) : 0 ≤ finiteAffineBestFitError a k m hkm b

Canonical finite affine best-fit errors are nonnegative.

theorem HCPolySupport.HighContrast.finiteAffineBestFitError_congr_index {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) {k l m : ℤ} (hkl : k = l) (hk : k ≤ m) (hl : l ≤ m) (b : Vec d) : finiteAffineBestFitError a k m hk b = finiteAffineBestFitError a l m hl b

theorem HCPolySupport.HighContrast.finiteAffineBestFitSlope_congr_index {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) {k l m : ℤ} (hkl : k = l) (hk : k ≤ m) (hl : l ≤ m) (b : Vec d) : (finiteAffineBestFitSlope a k m hk) b = (finiteAffineBestFitSlope a l m hl) b

theorem HCPolySupport.HighContrast.finiteAffineBestFitError_le {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) (k m : ℤ) (hkm : k ≤ m) (b : Vec d) (c : ℝ) (e : Vec d) : finiteAffineBestFitError a k m hkm b ≤ normalizedAffineCandidateError (originCube d k) (finiteAffineSolution a m b).toH1.toFun c e

The canonical best-fit error is no larger than the error of any affine candidate on the same cube.

theorem HCPolySupport.HighContrast.finiteCenteredCubeBestFitError_finiteAffineCubeSolution_of_le {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) (k m : ℤ) (hkm : k ≤ m) (b : Vec d) : finiteCenteredCubeBestFitErrorAt a m (finiteAffineCubeSolution a m b) k hkm = finiteAffineBestFitError a k m hkm b

The generic centered-cube best-fit row agrees with the canonical finite affine best fit when the cube solution carries affine boundary slope b.

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

The canonical finite-affine best-fit errors satisfy the fixed-step contraction supplied by the finite Lipschitz core.

theorem HCPolySupport.HighContrast.exists_originCubeAffineSlopeErrorConstant (d : ℕ) : ∃ (C : ℝ), 0 < C ∧ ∀ (k : ℤ) (c : ℝ) (e : Vec d), euclideanNorm e ≤ C * normalizedAffineCandidateError (originCube d k) (fun (x : Vec d) => 0) c e

theorem HCPolySupport.HighContrast.exists_finiteAffineBestFitAdjacentSlopeConstant (d : ℕ) [NeZero d] : ∃ (C : ℝ), 0 < C ∧ ∀ (a : Book.Ch02.TriadicCoeffFamily d) (k m : ℤ) (hkm : k + 1 ≤ m) (b : Vec d), euclideanNorm ((finiteAffineBestFitSlope a k m ⋯) b - (finiteAffineBestFitSlope a (k + 1) m hkm) b) ≤ C * finiteAffineBestFitError a (k + 1) m hkm b

Best-fit slopes on adjacent centered cubes differ by at most a dimension-only multiple of the outer best-fit error.

theorem HCPolySupport.HighContrast.exists_finiteAffineBestFitTerminalSlopeConstant (d : ℕ) [NeZero d] (s : ℝ) (hs : 0 < s) (hs_lt : s < 1 / 2) : ∃ (C : ℝ), 0 < C ∧ ∀ (a : Book.Ch02.TriadicCoeffFamily d) (m : ℤ) (b : Vec d) (delta : ℝ), 0 ≤ delta → delta ≤ 1 → scalarIdentityWeakError a s m ≤ delta → euclideanNorm ((finiteAffineBestFitSlope a m m ⋯) b - b) ≤ C * delta * euclideanNorm b

At the terminal scale, the best-fit slope is close to the prescribed boundary slope at response-error order.

theorem HCPolySupport.HighContrast.exists_finiteAffineBestFitCaccioppoliConstant (d : ℕ) [NeZero d] (s : ℝ) (hs : 0 < s) (hs_lt : s < 1 / 2) : ∃ (C : ℝ), 0 < C ∧ ∀ (a : Book.Ch02.TriadicCoeffFamily d) (m : ℤ) (b : Vec d) (k : ℤ) (hkm : k + 2 ≤ m), scalarIdentityWeakError a s (k + 2) ≤ 1 → finiteCenteredCubeSolutionEnergy a m (finiteAffineCubeSolution a m b) k ≤ C * (finiteAffineBestFitError a (k + 2) m hkm b + euclideanNorm ((finiteAffineBestFitSlope a (k + 2) m hkm) b))

Two-scale Caccioppoli control specialized to the canonical best affine fit of a finite affine-boundary solution.

theorem HCPolySupport.HighContrast.exists_finiteAffineBestFitTerminalBandConstant (d : ℕ) [NeZero d] (s : ℝ) (hs : 0 < s) (hs_lt : s < 1 / 2) (N : ℕ) : ∃ (C : ℝ), 0 < C ∧ ∀ (a : Book.Ch02.TriadicCoeffFamily d) (m : ℤ) (b : Vec d) (delta : ℝ) (k : ℤ), 0 ≤ delta → delta ≤ 1 → m - ↑N ≤ k → ∀ (hkm : k ≤ m), scalarIdentityWeakError a s m ≤ delta → finiteAffineBestFitError a k m hkm b ≤ C * delta * euclideanNorm b ∧ euclideanNorm ((finiteAffineBestFitSlope a k m hkm) b - b) ≤ C * delta * euclideanNorm b

Uniform initialization of the best-fit error and slope throughout a fixed terminal band.

theorem HCPolySupport.HighContrast.exists_scalarIdentityFiniteAffineBestFitErrorInductionConstants (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), finiteAffineBestFitError a k m ⋯ b ≤ C * delta * euclideanNorm ((finiteAffineBestFitSlope a k m ⋯) b)

A sufficiently small good-max row forces the canonical best-affine error to be proportional to the current best-fit slope at every scale.