Documentation

LeanPool.HighContrastHomogenization.Provider.PolynomialHomogenization.Root.Corrector.EquivariantPhysicalCorrectorFamilyWrapper

High-contrast homogenization: #

Provider.PolynomialHomogenization.Root.Corrector.EquivariantPhysicalCorrectorFamilyWrapper

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

Global representatives of equivariant corrector families #

Projective local-gradient covariance determines covariance of the canonical global representatives. This module combines that passage with the exact slope algebra of normalized local carriers and the zero extension away from an invariant construction event.

source
theorem HCPolySupport.HighContrast.Root.NormalizedLocalH1Carrier.globalGradientRepresentative_addCarrier {d : ℕ} (z w : NormalizedLocalH1Carrier d) :
(z.addCarrier w).globalGradientRepresentative =ᵐ[MeasureTheory.volume] fun (x : Vec d) => z.globalGradientRepresentative x + w.globalGradientRepresentative x

Addition of normalized carriers is addition of their canonical global gradient representatives, almost everywhere.

source
theorem HCPolySupport.HighContrast.Root.NormalizedLocalH1Carrier.globalGradientRepresentative_smulCarrier {d : ℕ} (c : ℝ) (z : NormalizedLocalH1Carrier d) :
(NormalizedLocalH1Carrier.smulCarrier c z).globalGradientRepresentative =ᵐ[MeasureTheory.volume] fun (x : Vec d) => c • z.globalGradientRepresentative x

Scalar multiplication of a normalized carrier is scalar multiplication of its canonical global gradient representative, almost everywhere.