High-contrast homogenization: Provider.Regularity.PrintOrderRoundedGenerationFiniteEllipticity

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

Analytic bounds for the rounded finite energy recurrence

This file derives the Poincare and coarse-Caccioppoli inputs used in the printed finite energy-row recurrence directly from the genuinely rounded comparison matrix and its fixed near-unity ellipticity window.

theorem HCPolySupport.HighContrast.RoundedFiniteEnergyInternal.coarseBMatrixNorm_le_printOrderRoundedReferenceResponse {d : ℕ} [NeZero d] {geom : RoundedGenerationAnalyticGeometry d} (Q : TriadicCube d) (a : Book.Ch02.TriadicCoeffFamily d) (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) : Book.Ch02.coarseBMatrixNorm Q a ≤ ↑d * (2 * (101 / 100)) * (Book.Ch02.normalizedBlockResponseMax Q a (geom.referenceMatrix abar hS) + 1)

The one-cube upper coarse ellipticity norm is controlled directly by the rounded-reference response.

theorem HCPolySupport.HighContrast.RoundedFiniteEnergyInternal.coarseSigmaStarInvMatrixNorm_le_printOrderRoundedReferenceResponse {d : ℕ} [NeZero d] {geom : RoundedGenerationAnalyticGeometry d} (Q : TriadicCube d) (a : Book.Ch02.TriadicCoeffFamily d) (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) : Book.Ch02.coarseSigmaStarInvMatrixNorm Q a ≤ ↑d * (2 * (100 / 99)) * (Book.Ch02.normalizedBlockResponseMax Q a (geom.referenceMatrix abar hS) + 1)

The one-cube lower coarse ellipticity inverse norm is controlled directly by the rounded-reference response.

theorem HCPolySupport.HighContrast.RoundedFiniteEnergyInternal.LambdaSq_finite_two_le_printOrderRoundedReferenceError {d : ℕ} [NeZero d] {geom : RoundedGenerationAnalyticGeometry d} (Q : TriadicCube d) (a : Book.Ch02.TriadicCoeffFamily d) (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) {s : ℝ} (hs : 0 < s) : Book.Ch02.LambdaSq Q s (Book.Ch02.MultiscaleExponent.finite 2) a ≤ ↑d * (2 * (100 / 99)) * (Book.Ch02.HomogenizationErrorOnCube Q s Book.Ch02.MultiscaleExponent.infinity (Book.Ch02.MultiscaleExponent.finite 2) a (geom.referenceMatrix abar hS) ^ 2 + 1)

The finite q = 2 upper ellipticity row is controlled directly by the homogenization error normalized against the rounded reference matrix.

theorem HCPolySupport.HighContrast.RoundedFiniteEnergyInternal.lambdaSq_finite_two_inv_le_printOrderRoundedReferenceError {d : ℕ} [NeZero d] {geom : RoundedGenerationAnalyticGeometry d} (Q : TriadicCube d) (a : Book.Ch02.TriadicCoeffFamily d) (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) {s : ℝ} (hs : 0 < s) : (Book.Ch02.lambdaSq Q s (Book.Ch02.MultiscaleExponent.finite 2) a)⁻¹ ≤ ↑d * (2 * (100 / 99)) * (Book.Ch02.HomogenizationErrorOnCube Q s Book.Ch02.MultiscaleExponent.infinity (Book.Ch02.MultiscaleExponent.finite 2) a (geom.referenceMatrix abar hS) ^ 2 + 1)

The inverse finite q = 2 lower ellipticity row is controlled directly by the homogenization error normalized against the rounded reference matrix.

theorem HCPolySupport.HighContrast.RoundedFiniteEnergyInternal.roundedGenerationWeakError_le_one_finiteTwoEllipticity {d : ℕ} [NeZero d] {geom : RoundedGenerationAnalyticGeometry d} (a : CoeffSpace d) (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) (aRounded : Book.Ch03.CoeffFamily d) (hRounded : ∀ (Q : TriadicCube d), (aRounded.coeffOn Q).toCoeffField = ↑↑(geom.centeredCoeffSpace abar hS a)) {s : ℝ} (hs : 0 < s) {k : ℤ} (herror : geom.spatialWeakError a abar hS s k ≤ 1) : Book.Ch02.LambdaSq (originCube d k) s (Book.Ch02.MultiscaleExponent.finite 2) aRounded ≤ 5 * ↑d ∧ (Book.Ch02.lambdaSq (originCube d k) s (Book.Ch02.MultiscaleExponent.finite 2) aRounded)⁻¹ ≤ 5 * ↑d

A rounded weak-error bound by one gives a dimension-only finite q = 2 ellipticity window.