High-contrast homogenization: #
Provider.Regularity.CorrectorGradientCubeIntegralTranslationStability
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
Translation stability for global corrector-gradient representatives #
The glued global gradient of every normalized local carrier belongs to
normalized L² on each exhaustion cube, as does every fixed translate. Thus
the general translated-cube integral theorem specializes with only the two
uniform quantitative bounds left to supply.
theorem
HCPolySupport.HighContrast.NormalizedLocalH1Carrier.memLp_globalGradientRepresentative_normalizedCubeMeasure
{d : ℕ}
(Phi : NormalizedLocalH1Carrier d)
(n : ℕ)
:
The glued global gradient representative belongs to normalized L² on
every centered exhaustion cube.
theorem
HCPolySupport.HighContrast.NormalizedLocalH1Carrier.memLp_globalGradientRepresentative_translate_normalizedCubeMeasure
{d : ℕ}
(Phi : NormalizedLocalH1Carrier d)
(t : Vec d)
(n : ℕ)
:
MeasureTheory.MemLp (fun (x : Vec d) => Phi.globalGradientRepresentative (x + t)) 2
(normalizedCubeMeasure (originCube d ↑n))
Every fixed translate of the glued global gradient representative also
belongs to normalized L² on every centered exhaustion cube.