High-contrast homogenization: Provider.Regularity.IntrinsicSlopeGlobalGradientUniqueness #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
Intrinsic-slope uniqueness from a global full-gradient identity #
The intrinsic slope is the limit of centered-cube averages of the full gradient. This file identifies that sequence with the averages of the glued global representative and records the resulting uniqueness principle.
theorem
HCPolySupport.HighContrast.localGradientClassAverage_eq_globalFullGradientAverage
{d : ℕ}
(e : Vec d)
(z : NormalizedLocalH1Carrier d)
(n : ℕ)
:
localGradientClassAverage
((have this := ⋯.mp (finiteAffineBoundaryH1 (↑n) e).gradToHilbertVectorL2;
this) + z.gradientComponent n) = cubeAverageVec (originCube d ↑n) fun (x : Vec d) => e + z.globalGradientRepresentative x
The intrinsic local-class average is the centered-cube average of the glued global full-gradient representative.