High-contrast homogenization: Provider.Regularity.WeakSolutionTranslation

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

Translation of global weak solutions

Integer covariance of correctors requires the deterministic fact that a global weak solution remains a global weak solution after translating both its coefficient and flux fields. This file proves that raw PDE transport without assuming any corrector-family covariance.

theorem HCPolySupport.HighContrast.smoothGrad_comp_subRight {d : ℕ} (phi : Vec d → ℝ) (z x : Vec d) : smoothGrad (fun (y : Vec d) => phi (y - z)) x = smoothGrad phi (x - z)

The coordinate gradient commutes with precomposition by a translation.

theorem HCPolySupport.HighContrast.IsWeakSolutionOn.translateCoeffField_univ {d : ℕ} {b : CoeffField d} {F : Vec d → Vec d} (h : IsWeakSolutionOn b Set.univ F) (z : Vec d) : IsWeakSolutionOn (translateCoeffField z b) Set.univ fun (x : Vec d) => F (x + z)

A global weak solution translates with its coefficient field: if F is b-harmonic, then F(· + z) is b(· + z)-harmonic.