High-contrast homogenization: Provider.Regularity.FiniteAffineGradientExcessStep

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

One-step finite affine gradient excess

This module assembles the ruled best-fit normalization with harmonic residuals. It first records the exact value-error bridge consumed by the two-scale Caccioppoli estimate.

theorem HCPolySupport.HighContrast.finiteCenteredCubeBestFitErrorAt_restriction_eq {d : ℕ} (a : Book.Ch02.TriadicCoeffFamily d) (m : ℤ) (u : Book.Ch03.CubeSolution (originCube d m) a) (k : ℤ) (hkm : k ≤ m) : have uk := finiteCubeSolutionRestriction a hkm u; finiteCenteredCubeBestFitErrorAt a k uk k ⋯ = finiteCenteredCubeBestFitErrorAt a m u k hkm

Restricting a solution and then taking its outer-scale best-fit error is the same as taking the original solution's best-fit error on that inner cube.

theorem HCPolySupport.HighContrast.finiteAffineGradientUpdatedResidual_candidateError_le {d : ℕ} [NeZero d] {a : Book.Ch02.TriadicCoeffFamily d} {delta C : ℝ} {n m : ℤ} {Q : ℤ → Mat d} (hfamily : IsFiniteAffineSlopeFamily a delta C n m Q) {r k : ℤ} (hr : r ∈ Finset.Icc n m) (hrk : r ≤ k) (hkm : k ≤ m) (u : Book.Ch03.CubeSolution (originCube d m) a) (e : Vec d) : have v := finiteAffineGradientResidual a hkm u e; have vR := finiteCubeSolutionRestriction a hrk v; have c := finiteCenteredCubeBestFitInterceptAt a r vR r; have p := finiteCenteredCubeBestFitSlopeAt a r vR r; have q := matVecMul (Q r) p; have cQ := (finiteAffineBestFitIntercept a r m ⋯) q; normalizedAffineCandidateError (originCube d r) (finiteAffineGradientUpdatedResidual a ⋯ u e q).toH1.toFun (c - cQ) 0 ≤ finiteCenteredCubeBestFitErrorAt a r vR r ⋯ + C * delta * euclideanNorm p

The ruled finite-affine comparison turns the canonical affine best fit of an arbitrary harmonic residual into a zero-slope affine candidate for the updated residual.

theorem HCPolySupport.HighContrast.exists_scalarIdentityFiniteAffineGradientExcessIntegerRateStepConstants (d : ℕ) [NeZero d] (s : ℝ) (hs : 0 < s) (hs_lt : s < 1 / 2) (p : ℕ) (hp : 0 < p) : ∃ (depth : ℕ) (C₀ : ℝ) (Cc : ℝ) (Ce : ℝ) (Ct : ℝ), 0 < C₀ ∧ 0 < Cc ∧ 0 < Ce ∧ 0 < Ct ∧ ∀ (t : ℕ), have N := depth + 2 * p * t + 2; ∃ (Cs : ℝ), 0 < Cs ∧ ∀ (a : Book.Ch02.TriadicCoeffFamily d) (delta C : ℝ) (n m : ℤ) (Q : ℤ → Mat d), 0 ≤ delta → 1 ≤ C → ScalarIdentityGoodMaxOnInterval a s delta n m → IsFiniteAffineSlopeFamily a delta C n m Q → ∀ k ∈ Finset.Icc n m, k - ↑N ∈ Finset.Icc n m → ∀ (u : Book.Ch03.CubeSolution (originCube d m) a), finiteAffineGradientExcess a (k - ↑N - 2) m u ≤ ENNReal.ofReal (Cc * (C₀ * (1 / 3) ^ ((2 * p - 1) * t) * Ce + Cs * delta + C * delta * Ct * ↑((3 ^ d) ^ N))) * finiteAffineGradientExcess a k m u

Integer-rate Step 1 for the canonical gradient excess. The deterministic coefficient has effective per-scale exponent 1 - 1 / (2p); the two coefficient-error terms remain explicit for the later smallness choice.