High-contrast homogenization: Provider.Regularity.PrintOrderRoundedAnalyticGeometry

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

Analytic geometry of a selected rounded generation

This carrier exposes the same constant-matrix and harmonic-replacement API used by the finite regularity proof, with the rounded generation explicit.

structure HCPolySupport.HighContrast.RoundedGenerationAnalyticGeometry (d : ℕ) [NeZero d] : Type

Uniform deterministic geometry attached to one admissible rounded generation.

• generation : ℤ

  Admissible generation at which the reference matrices and deterministic geometry are rounded.

• admissible : ↑(kZero d) ≤ self.generation
• reference_posDef (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) : Matrix.PosDef (roundedReferenceMatrixAtGeneration self.generation abar hS)
• reference_elliptic (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) : IsEllipticMatrix (99 / 100) (101 / 100) (roundedReferenceMatrixAtGeneration self.generation abar hS)
• reference_lower (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) : (99 / 100) • 1 ≤ roundedReferenceMatrixAtGeneration self.generation abar hS
• reference_upper (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) : roundedReferenceMatrixAtGeneration self.generation abar hS ≤ (101 / 100) • 1

noncomputable def HCPolySupport.HighContrast.RoundedGenerationAnalyticGeometry.grid {d : ℕ} [NeZero d] (geom : RoundedGenerationAnalyticGeometry d) (m : Mat d) : Mat d

The selected rounded coordinate matrix.

Equations

• geom.grid m = HCPolySupport.HighContrast.roundedGrid geom.generation m

theorem HCPolySupport.HighContrast.RoundedGenerationAnalyticGeometry.grid_posDef {d : ℕ} [NeZero d] (geom : RoundedGenerationAnalyticGeometry d) {m : Mat d} (hm : Matrix.PosDef m) : Matrix.PosDef (geom.grid m)

theorem HCPolySupport.HighContrast.RoundedGenerationAnalyticGeometry.grid_transpose {d : ℕ} [NeZero d] (geom : RoundedGenerationAnalyticGeometry d) {m : Mat d} (hm : Matrix.PosDef m) : matTranspose (geom.grid m) = geom.grid m

theorem HCPolySupport.HighContrast.RoundedGenerationAnalyticGeometry.grid_det_isUnit {d : ℕ} [NeZero d] (geom : RoundedGenerationAnalyticGeometry d) {m : Mat d} (hm : Matrix.PosDef m) : IsUnit (Matrix.det (geom.grid m))

noncomputable def HCPolySupport.HighContrast.RoundedGenerationAnalyticGeometry.referenceMatrix {d : ℕ} [NeZero d] (geom : RoundedGenerationAnalyticGeometry d) (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) : Mat d

The constant selected-generation reference matrix.

Equations

• geom.referenceMatrix abar hS = HCPolySupport.HighContrast.roundedReferenceMatrixAtGeneration geom.generation abar hS

noncomputable def HCPolySupport.HighContrast.RoundedGenerationAnalyticGeometry.centeredCoeffSpace {d : ℕ} [NeZero d] (geom : RoundedGenerationAnalyticGeometry d) (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) (a : CoeffSpace d) : CoeffSpace d

The selected normalized coefficient carrier.

Equations

• geom.centeredCoeffSpace abar hS a = HCPolySupport.HighContrast.roundedCenteredCoeffSpaceAtGeneration geom.generation ⋯ abar hS a

noncomputable def HCPolySupport.HighContrast.RoundedGenerationAnalyticGeometry.responseMax {d : ℕ} [NeZero d] (geom : RoundedGenerationAnalyticGeometry d) (a : CoeffSpace d) (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) (k : ℤ) (w : Fin d → ℤ) : ℝ

The selected physical response maximum.

Equations

• geom.responseMax a abar hS k w = HCPolySupport.HighContrast.roundedNormalizedDoubledResponseMaxAtGeneration geom.generation a abar hS k w

noncomputable def HCPolySupport.HighContrast.RoundedGenerationAnalyticGeometry.spatialWeakError {d : ℕ} [NeZero d] (geom : RoundedGenerationAnalyticGeometry d) (a : CoeffSpace d) (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) (s : ℝ) (m : ℤ) : ℝ

The selected full weak-error row.

Equations

• geom.spatialWeakError a abar hS s m = HCPolySupport.HighContrast.roundedGenerationSpatialWeakError geom.generation a abar hS s m

theorem HCPolySupport.HighContrast.RoundedGenerationAnalyticGeometry.spatialWeakError_nonneg {d : ℕ} [NeZero d] (geom : RoundedGenerationAnalyticGeometry d) (a : CoeffSpace d) (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) (s : ℝ) (m : ℤ) : 0 ≤ geom.spatialWeakError a abar hS s m

theorem HCPolySupport.HighContrast.RoundedGenerationAnalyticGeometry.reference_coarse_elliptic {d : ℕ} [NeZero d] (geom : RoundedGenerationAnalyticGeometry d) (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) : IsEllipticMatrix (1 / 2) 2 (geom.referenceMatrix abar hS)

noncomputable def HCPolySupport.HighContrast.RoundedGenerationAnalyticGeometry.referenceConstantCoeffMatrix {d : ℕ} [NeZero d] (geom : RoundedGenerationAnalyticGeometry d) (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) : Book.Ch03.ConstantCoeffMatrix d

The selected reference in the Chapter 3 constant-matrix carrier.

Equations

• geom.referenceConstantCoeffMatrix abar hS = HCPolySupport.HighContrast.roundedReferenceConstantCoeffMatrixAtGeneration geom.generation abar hS ⋯ ⋯

@[simp]

theorem HCPolySupport.HighContrast.RoundedGenerationAnalyticGeometry.referenceConstantCoeffMatrix_matrix {d : ℕ} [NeZero d] (geom : RoundedGenerationAnalyticGeometry d) (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) : (geom.referenceConstantCoeffMatrix abar hS).matrix = geom.referenceMatrix abar hS

noncomputable def HCPolySupport.HighContrast.RoundedGenerationAnalyticGeometry.harmonicReplacementDatum {d : ℕ} [NeZero d] (geom : RoundedGenerationAnalyticGeometry d) (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) (a : Book.Ch03.CoeffFamily d) (m : ℤ) (u : H1Function (Book.Ch02.cubeDomain (originCube d m)).carrier) (hu : IsWeakSolutionOn (a.coeffOn (originCube d m)).toCoeffField (Book.Ch02.cubeDomain (originCube d m)).carrier u.grad) : Book.Ch03.CoarseGrainingComparisonDatum (originCube d m) a (roundedReferenceConstantCoeffMatrixAtGeneration geom.generation abar hS ⋯ ⋯) 0

The same-trace harmonic replacement for the selected reference.

Equations

• geom.harmonicReplacementDatum abar hS a m u hu = HCPolySupport.HighContrast.roundedHarmonicReplacementDatumAtGeneration geom.generation abar hS ⋯ ⋯ a m u hu

@[simp]

theorem HCPolySupport.HighContrast.RoundedGenerationAnalyticGeometry.harmonicReplacementDatum_u {d : ℕ} [NeZero d] (geom : RoundedGenerationAnalyticGeometry d) (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) (a : Book.Ch03.CoeffFamily d) (m : ℤ) (u : H1Function (Book.Ch02.cubeDomain (originCube d m)).carrier) (hu : IsWeakSolutionOn (a.coeffOn (originCube d m)).toCoeffField (Book.Ch02.cubeDomain (originCube d m)).carrier u.grad) : (geom.harmonicReplacementDatum abar hS a m u hu).u = u

def HCPolySupport.HighContrast.RoundedGenerationAnalyticGeometry.ofApplication {d : ℕ} [NeZero d] {g : ℝ} {a : CoeffSpace d} {abar : Mat d} {sourceAmplitude target kappa Cid : ℝ} {X : CoeffSpace d → ℝ} (application : PrintOrderParametricRoundedCoefficientApplication d g a abar sourceAmplitude target kappa Cid X) : RoundedGenerationAnalyticGeometry d

The geometry extracted from a parametric rounded application.

Equations

• One or more equations did not get rendered due to their size.