High-contrast homogenization: Provider.Regularity.HarmonicAffineResidual

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

theorem HCPolySupport.WeakPoissonEquationOn.exists_sub_affine_harmonic {d : ℕ} (Q : TriadicCube d) (u : H1Function (openCubeSet Q)) (hu : WeakPoissonEquationOn (openCubeSet Q) u fun (x : Vec d) => 0) (c : ℝ) (e : Vec d) : ∃ (v : H1Function (openCubeSet Q)), (v.toFun = fun (x : Vec d) => u.toFun x - (c + vecDot e x)) ∧ (v.grad = fun (x : Vec d) => u.grad x - e) ∧ WeakPoissonEquationOn (openCubeSet Q) v fun (x : Vec d) => 0

Subtracting an affine function from a weakly harmonic function on an open cube preserves weak harmonicity, with the value and gradient representatives kept explicit for the later affine-error calculation.