Documentation

LeanPool.HighContrastHomogenization.Provider.PolynomialHomogenization.Root.Corrector.C1JointTargetRestriction

High-contrast homogenization: #

Provider.PolynomialHomogenization.Root.Corrector.C1JointTargetRestriction

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

Restriction of the joint affine-corrector target #

The projective joint limit has one compatible full-gradient class on every centered cube. Consequently the harmonic target on an inner cube is the restriction of the joint cube solution on any larger centered cube.

source
theorem HCPolySupport.HighContrast.Root.jointTargetHarmonicGradient_eq_restricted_outer {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) (hCauchy : FiniteAffineCorrectionLocalCauchy a) (e : Vec d) {q m : ℕ} (hqm : q ≤ m) :
↑((jointTargetHarmonicGradientLinearMap a hCauchy q) e) = (finiteCubeSolutionRestriction a ⋯ (finiteAffineCorrectionJointLocalCubeSolution a hCauchy e m)).toH1.gradToHilbertVectorL2

The joint harmonic target is the restriction of its outer cube-solution representative.