Documentation

LeanPool.HighContrastHomogenization.Provider.PolynomialHomogenization.Root.RowSupply.LocalHomogenizationErrorTranslation

High-contrast homogenization: #

Provider.PolynomialHomogenization.Root.RowSupply.LocalHomogenizationErrorTranslation

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

Local translation of the cube homogenization error #

Root-cube identifications with one physical coefficient determine all descendant responses. The resulting theorem is the local, a.e. version of the upstream translation API needed for independently constructed coefficient families.

source
noncomputable def HCPolySupport.HighContrast.RowSupply.cubeTranslationVector {d : ℕ} (z : Fin d → ℤ) (Q : TriadicCube d) :
Vec d

The physical translation represented by a lattice shift of a triadic cube.

Equations
Instances For
    source
    theorem HCPolySupport.HighContrast.RowSupply.homogenizationErrorOnCube_translate_of_physical_ae {d : ℕ} (z : Fin d → ℤ) (Q : TriadicCube d) (aPhysical aCentered : Book.Ch02.TriadicCoeffFamily d) (f : CoeffField d) (hPhysical : (aPhysical.coeffOn (translateCube z Q)).toCoeffField =ᵐ[volumeMeasureOn (openCubeSet (translateCube z Q))] f) (hCentered : (aCentered.coeffOn Q).toCoeffField =ᵐ[volumeMeasureOn (openCubeSet Q)] translateCoeffField (cubeTranslationVector z Q) f) (s : ℝ) (p q : Book.Ch02.MultiscaleExponent) (a0 : Mat d) :
    Book.Ch02.HomogenizationErrorOnCube (translateCube z Q) s p q aPhysical a0 = Book.Ch02.HomogenizationErrorOnCube Q s p q aCentered a0

    Two independently constructed coefficient families have identical on-cube homogenization errors when their root representatives are the same physical coefficient before and after the cube translation.