High-contrast homogenization:

Provider.PolynomialHomogenization.Root.CorrectorDecay.JointAEEqTransfer

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

theorem HCPolySupport.HighContrast.finiteAffineSolution_grad_ae_of_aeeq {d : ℕ} [NeZero d] {a b : Book.Ch02.TriadicCoeffFamily d} (hab : a.AEEq b) (m : ℤ) (e : Vec d) : (finiteAffineSolution a m e).toH1.grad =ᵐ[volumeMeasureOn (Book.Ch02.cubeDomain (originCube d m)).carrier] (finiteAffineSolution b m e).toH1.grad

Finite affine Dirichlet gradients depend only on the a.e. coefficient family.

theorem HCPolySupport.HighContrast.finiteAffineCorrection_grad_ae_of_aeeq {d : ℕ} [NeZero d] {a b : Book.Ch02.TriadicCoeffFamily d} (hab : a.AEEq b) (m : ℤ) (e : Vec d) : (finiteAffineCorrection a m e).grad =ᵐ[volumeMeasureOn (Book.Ch02.cubeDomain (originCube d m)).carrier] (finiteAffineCorrection b m e).grad

The zero-trace correction gradients inherit the preceding a.e. invariance after cancelling the common affine boundary slope.

theorem HCPolySupport.HighContrast.finiteAffineCorrectionLocalSequence_gradient_eq_of_aeeq {d : ℕ} [NeZero d] {a b : Book.Ch02.TriadicCoeffFamily d} (hab : a.AEEq b) (e : Vec d) (q : ℕ) : (finiteAffineCorrectionLocalSequence a e q).gradToHilbertVectorL2 = (finiteAffineCorrectionLocalSequence b e q).gradToHilbertVectorL2

The Hilbert-vector class of a finite correction gradient is a.e. invariant in the coefficient family.

theorem HCPolySupport.HighContrast.normalizedLocalPair_gradient_eq_of_aeeq {d : ℕ} [NeZero d] {a b : Book.Ch02.TriadicCoeffFamily d} (hab : a.AEEq b) (e : Vec d) (n k : ℕ) : (normalizedLocalPair (finiteAffineCorrectionLocalSequence a e) n k).2 = (normalizedLocalPair (finiteAffineCorrectionLocalSequence b e) n k).2

The gradient component of every normalized local pair is invariant under a.e. replacement of the coefficient family.

theorem HCPolySupport.HighContrast.jointGradientComponent_eq_of_aeeq {d : ℕ} [NeZero d] {a b : Book.Ch02.TriadicCoeffFamily d} (hab : a.AEEq b) (PhiA PhiB : Vec d → NormalizedLocalH1Carrier d) (hA : IsFiniteAffineCorrectionJointLocalEquation a PhiA) (hB : IsFiniteAffineCorrectionJointLocalEquation b PhiB) (e : Vec d) (n : ℕ) : (PhiA e).gradientComponent n = (PhiB e).gradientComponent n

Two joint finite-corrector limits for a.e.-equal families have identical projective gradient components. No equality of value representatives or of the bundled families is asserted.

theorem HCPolySupport.HighContrast.jointGlobalGradient_ae_of_aeeq {d : ℕ} [NeZero d] {a b : Book.Ch02.TriadicCoeffFamily d} (hab : a.AEEq b) (PhiA PhiB : Vec d → NormalizedLocalH1Carrier d) (hA : IsFiniteAffineCorrectionJointLocalEquation a PhiA) (hB : IsFiniteAffineCorrectionJointLocalEquation b PhiB) (e : Vec d) : (PhiA e).globalGradientRepresentative =ᵐ[MeasureTheory.volume] (PhiB e).globalGradientRepresentative

Canonical global gradient representatives of a.e.-equal coefficient families agree almost everywhere.