High-contrast homogenization: Provider.Regularity.PrintOrderRoundedGenerationFinitePoincareRows

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

Printed-order Poincare rows for the finite recurrence

The fluctuation estimate uses the weak-error row at the same fractional order. Its proof only requires that half of this order lie below one half; the stronger small-order binder in the archived wrapper is not used.

theorem HCPolySupport.HighContrast.exists_roundedGenerationFiniteLipschitzPoincareConstant (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), geom.spatialWeakError a abar hS s k ≤ 1 → cubeBesovScaleWeight 1 (originCube d k) * cubeLpNorm (originCube d k) 2 (cubeFluctuation (originCube d k) u.toH1.toFun) ≤ C * Book.Ch03.h1EnergyNormOnCube (originCube d k) aRounded u.toH1

Poincare's fluctuation estimate at any positive order below one half.

theorem HCPolySupport.HighContrast.exists_roundedGenerationFiniteLipschitzAffineErrorEnergyConstant (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)) → ∀ (m : ℤ) (u : Book.Ch03.CubeSolution (originCube d m) aRounded), ∀ k ≤ m, geom.spatialWeakError a abar hS s k ≤ 1 → FiniteLipschitzCoreInternal.finiteLipschitzAffineErrorRow aRounded m u k ≤ C * FiniteLipschitzCoreInternal.finiteLipschitzEnergyRow aRounded m u k

The best affine error is controlled by the energy row at a printed-order good scale.

theorem HCPolySupport.HighContrast.exists_roundedGenerationFiniteLipschitzTerminalSlopeConstant (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)) → ∀ (m : ℤ) (u : Book.Ch03.CubeSolution (originCube d m) aRounded), geom.spatialWeakError a abar hS s m ≤ 1 → euclideanNorm (FiniteLipschitzCoreInternal.finiteLipschitzBestSlope aRounded m u m) ≤ C * FiniteLipschitzCoreInternal.finiteLipschitzEnergyRow aRounded m u m

The top-scale best affine slope is controlled by the top energy row at a printed-order good scale.