High-contrast homogenization: #

Provider.PolynomialHomogenization.Root.CorrectorComposition.JointCarrierAEEq

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

The joint local limit depends only on the a.e. coefficient family #

HCPoly.Provider.PolynomialHomogenization.Root.CorrectorDecay.JointAEEqTransfer proves that two joint finite-corrector limits for a.e.-equal coefficient families have identical projective gradient components, and says explicitly that "no equality of value representatives or of the bundled families is asserted".

This module supplies the value half and therefore the equality of the bundled carriers. The analytic content is one line of Poincaré: the two finite affine corrections at a given generation are H¹₀ functions on the same cube whose weak gradients agree almost everywhere, so their difference is an H¹₀ function with vanishing gradient class, hence vanishes.

The consequence used downstream is jointLocalLimit_eq_of_aeeq: the canonical joint local limit is literally the same carrier family for a.e.-equal coefficient families. That is what lets the root's corrector-family hypotheses be discharged with the certificate's own exact-gauge reference family in place of the (arbitrarily selected) datum family.

The value half #

source

theorem HCPolySupport.HighContrast.CorrectorComposition.finiteAffineCorrection_toScalarL2_eq_of_aeeq {d : ℕ} [NeZero d] {a b : Book.Ch02.TriadicCoeffFamily d} (hab : a.AEEq b) (m : ℤ) (e : Vec d) :

(finiteAffineCorrection a m e).toScalarL2 = (finiteAffineCorrection b m e).toScalarL2

Zero-trace corrections with a.e.-equal gradients have equal L² classes. The difference is an H¹₀ function on the cube whose gradient class vanishes; the zero-trace Poincaré inequality kills it.

source