Documentation

LeanPool.HighContrastHomogenization.Provider.Regularity.PrintOrderRoundedGenerationData

High-contrast homogenization: Provider.Regularity.PrintOrderRoundedGenerationData #

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

Coefficient data at a selected rounded generation #

The affine coefficient, its constant symmetric reference, and the Chapter 3 coefficient family are packaged using one common admissible generation.

source
noncomputable def HCPolySupport.HighContrast.roundedCenteredCoefficientAtGeneration {d : ℕ} (l : ℤ) (hl : ↑(kZero d) ≤ l) (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) (a : CoeffField d) :
CoeffField d

The centered physical coefficient pulled back by a selected rounded grid.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem HCPolySupport.HighContrast.roundedCenteredCoefficientAtGeneration_apply {d : ℕ} (l : ℤ) (hl : ↑(kZero d) ≤ l) (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) (a : CoeffField d) (y : Vec d) :
    roundedCenteredCoefficientAtGeneration l hl abar hS a y = (roundedGrid l (symmPart abar))⁻¹ * specBound (symmPart abar)⁻¹ • (a (matVecMul (roundedGrid l (symmPart abar)) y) - skewPart abar) * matTranspose (roundedGrid l (symmPart abar))⁻¹
    source
    noncomputable def HCPolySupport.HighContrast.roundedCenteredCoeffSpaceAtGeneration {d : ℕ} [NeZero d] (l : ℤ) (hl : ↑(kZero d) ≤ l) (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) (a : CoeffSpace d) :
    CoeffSpace d

    The selected-grid pullback on the qualitative coefficient carrier.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem HCPolySupport.HighContrast.roundedCenteredCoeffSpaceAtGeneration_ae {d : ℕ} [NeZero d] (l : ℤ) (hl : ↑(kZero d) ≤ l) (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) (a : CoeffSpace d) :
      ↑↑(roundedCenteredCoeffSpaceAtGeneration l hl abar hS a) =ᵐ[MeasureTheory.volume] roundedCenteredCoefficientAtGeneration l hl abar hS ↑↑a

      The selected-grid pullback has the literal transformed representative almost everywhere.

      source
      theorem HCPolySupport.HighContrast.exists_roundedCenteredCoeffFamilyAtGeneration {d : ℕ} [NeZero d] (l : ℤ) (hl : ↑(kZero d) ≤ l) (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) (a : CoeffSpace d) :
      ∃ (aRounded : Book.Ch03.CoeffFamily d), (∀ (Q : TriadicCube d), (aRounded.coeffOn Q).toCoeffField = ↑↑(roundedCenteredCoeffSpaceAtGeneration l hl abar hS a)) ∧ ∀ (Q : TriadicCube d), (aRounded.coeffOn Q).toCoeffField =ᵐ[MeasureTheory.volume] roundedCenteredCoefficientAtGeneration l hl abar hS ↑↑a

      The selected rounded sample admits a compatible Chapter 3 family.

      source
      noncomputable def HCPolySupport.HighContrast.roundedReferenceConstantCoeffMatrixAtGeneration {d : ℕ} (l : ℤ) (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) (hPos : Matrix.PosDef (roundedReferenceMatrixAtGeneration l abar hS)) (hEll : IsEllipticMatrix (1 / 2) 2 (roundedReferenceMatrixAtGeneration l abar hS)) :
      Book.Ch03.ConstantCoeffMatrix d

      A selected near-identity matrix in the Chapter 3 constant-coefficient carrier, using the uniform one-half/two ellipticity window.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        noncomputable def HCPolySupport.HighContrast.roundedHarmonicReplacementDatumAtGeneration {d : ℕ} (l : ℤ) (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) (hPos : Matrix.PosDef (roundedReferenceMatrixAtGeneration l abar hS)) (hEll : IsEllipticMatrix (1 / 2) 2 (roundedReferenceMatrixAtGeneration l abar hS)) (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 l abar hS hPos hEll) 0

        The chosen same-trace comparison for any selected rounded reference.

        Equations
        Instances For
          source
          @[simp]
          theorem HCPolySupport.HighContrast.roundedHarmonicReplacementDatumAtGeneration_u {d : ℕ} (l : ℤ) (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) (hPos : Matrix.PosDef (roundedReferenceMatrixAtGeneration l abar hS)) (hEll : IsEllipticMatrix (1 / 2) 2 (roundedReferenceMatrixAtGeneration l abar hS)) (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) :
          (roundedHarmonicReplacementDatumAtGeneration l abar hS hPos hEll a m u hu).u = u