High-contrast homogenization: Provider.Regularity.PrintOrderRoundedGenerationFiniteCaccioppoli

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

Printed-order Caccioppoli row for the finite recurrence

The Caccioppoli parameters are chosen strictly between the response order and one half. The exponent-gap ellipticity bridge then supplies both q = 1 rows from the printed q = 2 weak-error row.

theorem HCPolySupport.HighContrast.exists_roundedGenerationFiniteLipschitzCaccioppoliAffineConstant (d : ℕ) [NeZero d] (geom : RoundedGenerationAnalyticGeometry d) (s : ℝ) (hs : 0 < s) (hs_lt : s < 1 / 2) : ∃ (C : ℝ), 0 < C ∧ ∀ (a : CoeffSpace d) (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) (aRounded : Book.Ch03.CoeffFamily d), (∀ (Q : TriadicCube d), (aRounded.coeffOn Q).toCoeffField = ↑↑(geom.centeredCoeffSpace abar hS a)) → ∀ (k : ℤ) (u : Book.Ch03.CubeSolution (originCube d k) aRounded) (c : ℝ) (e : Vec d), geom.spatialWeakError a abar hS s k ≤ 1 → Book.Ch03.h1EnergyNormOnCube (originCube d (k - 2)) aRounded (finiteCubeSolutionRestriction aRounded ⋯ u).toH1 ≤ C * (normalizedAffineCandidateError (originCube d k) u.toH1.toFun c e + euclideanNorm e)

The coarse Caccioppoli row at every positive printed order below one half.