High-contrast homogenization: Provider.Regularity.PrintOrderParametricRoundedApplication

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

Printed-order application at a tolerance-selected rounded generation

The rounded generation is chosen after the identity regularity constant. The same generation is then used for the near-identity reference, the physical coefficient family, and every response row.

noncomputable def HCPolySupport.HighContrast.printOrderSpineRoundingTolerance (d : ℕ) (Cid : ℝ) : ℝ

The private spine keeps the original one-percent geometric window and, when necessary, refines it further to the absorption tolerance.

Equations

• HCPolySupport.HighContrast.printOrderSpineRoundingTolerance d Cid = min (1 / 100) (HCPolySupport.HighContrast.printOrderAbsorptionTolerance d Cid)

theorem HCPolySupport.HighContrast.printOrderSpineRoundingTolerance_pos (d : ℕ) (Cid : ℝ) : 0 < printOrderSpineRoundingTolerance d Cid

theorem HCPolySupport.HighContrast.printOrderSpineRoundingTolerance_le_absorption (d : ℕ) (Cid : ℝ) : printOrderSpineRoundingTolerance d Cid ≤ printOrderAbsorptionTolerance d Cid

theorem HCPolySupport.HighContrast.printOrderSpineRoundingTolerance_le_one_percent (d : ℕ) (Cid : ℝ) : printOrderSpineRoundingTolerance d Cid ≤ 1 / 100

theorem HCPolySupport.HighContrast.printOrderSpineRoundingTolerance_le_half (d : ℕ) (Cid : ℝ) : printOrderSpineRoundingTolerance d Cid ≤ 1 / 2

theorem HCPolySupport.HighContrast.printOrderRoundedReferenceDualRegularityAtGeneration_of_absorption (d : ℕ) (g Cid : ℝ) (hg : g ∈ Set.Ico 0 1) (hidentity : PrintOrderIdentityCubeDualRegularityWithConstant d g Cid) {generation : ℤ} (hmatrix : ∀ (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)), Matrix.PosDef (roundedReferenceMatrixAtGeneration generation abar hS) ∧ IsEllipticMatrix (1 - printOrderAbsorptionTolerance d Cid) (1 + printOrderAbsorptionTolerance d Cid) (roundedReferenceMatrixAtGeneration generation abar hS) ∧ ‖roundedReferenceMatrixAtGeneration generation abar hS - 1‖ ≤ printOrderAbsorptionTolerance d Cid) : PrintOrderRoundedReferenceDualRegularityAtGeneration d g generation

structure HCPolySupport.HighContrast.PrintOrderParametricRoundedCoefficientApplication (d : ℕ) [NeZero d] (g : ℝ) (a : CoeffSpace d) (abar : Mat d) (sourceAmplitude target kappa Cid : ℝ) (X : CoeffSpace d → ℝ) : Type

The complete rounded application at the generation selected by the absorption tolerance.

• generation : ℤ

  Admissible rounding generation selected for the prescribed absorption tolerance.

• generation_admissible : ↑(kZero d) ≤ self.generation
• hS : Matrix.PosDef (symmPart abar)
• reference_posDef : Matrix.PosDef (roundedReferenceMatrixAtGeneration self.generation abar ⋯)
• reference_posDef_all (abar' : Mat d) (hS' : Matrix.PosDef (symmPart abar')) : Matrix.PosDef (roundedReferenceMatrixAtGeneration self.generation abar' hS')
• reference_sharp_elliptic_all (abar' : Mat d) (hS' : Matrix.PosDef (symmPart abar')) : IsEllipticMatrix (99 / 100) (101 / 100) (roundedReferenceMatrixAtGeneration self.generation abar' hS')
• reference_lower_all (abar' : Mat d) (hS' : Matrix.PosDef (symmPart abar')) : (99 / 100) • 1 ≤ roundedReferenceMatrixAtGeneration self.generation abar' hS'
• reference_upper_all (abar' : Mat d) (hS' : Matrix.PosDef (symmPart abar')) : roundedReferenceMatrixAtGeneration self.generation abar' hS' ≤ (101 / 100) • 1
• reference_elliptic : IsEllipticMatrix (1 / 2) 2 (roundedReferenceMatrixAtGeneration self.generation abar ⋯)
• reference_defect : ‖roundedReferenceMatrixAtGeneration self.generation abar ⋯ - 1‖ ≤ printOrderAbsorptionTolerance d Cid
• dualRegularity : PrintOrderRoundedReferenceDualRegularityAtGeneration d g self.generation
• commonCertificate : PrintOrderQuantitativeNormalizedReferenceCertificate abar g target kappa (printOrderCommonQuantitativeAffineScale d g sourceAmplitude target kappa abar X a) a
• goodMax (m : ℤ) : ↑(Quenched.triadicCeilingIndex (printOrderCommonQuantitativeAffineScale d g sourceAmplitude target kappa abar X a)) ≤ m → RoundedGenerationSpatialGoodMaxOnInterval self.generation a abar ⋯ (printCertificateOrder g) (target / (1 - 3 ^ (-kappa))) (↑(Quenched.triadicCeilingIndex (printOrderCommonQuantitativeAffineScale d g sourceAmplitude target kappa abar X a))) m
• goodTail : RoundedGenerationSpatialGoodTail self.generation a abar ⋯ (printCertificateOrder g) (target / (1 - 3 ^ (-kappa))) ↑(Quenched.triadicCeilingIndex (printOrderCommonQuantitativeAffineScale d g sourceAmplitude target kappa abar X a))
• aRounded : Book.Ch03.CoeffFamily d

  Triadic coefficient family realizing the centered coefficient rounded at generation.

• aRounded_eq (Q : TriadicCube d) : (self.aRounded.coeffOn Q).toCoeffField = ↑↑(roundedCenteredCoeffSpaceAtGeneration self.generation ⋯ abar ⋯ a)
• aRounded_ae (Q : TriadicCube d) : (self.aRounded.coeffOn Q).toCoeffField =ᵐ[MeasureTheory.volume] roundedCenteredCoefficientAtGeneration self.generation ⋯ abar ⋯ ↑↑a