High-contrast homogenization: Provider.Regularity.WeakGradientTranslation #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
Translation of weak-gradient pairs #
The upstream H1Function translation API contains this change of variables
for bundled square-integrable functions. Corrector representatives are used
globally and locally, so this file proves the underlying predicate-level
transport without adding an H1Function witness.
theorem
HCPolySupport.HighContrast.HasWeakGradientOn.untranslate
{d : ℕ}
{U : Set (Vec d)}
{u : Vec d → ℝ}
{Du : Vec d → Vec d}
(z : Vec d)
(h : HasWeakGradientOn (translateSet z U) u Du)
:
HasWeakGradientOn U (fun (x : Vec d) => u (x + z)) fun (x : Vec d) => Du (x + z)
Pulling a weak-gradient pair on U + z back by x ↦ x + z gives a
weak-gradient pair on U.