High-contrast homogenization: Provider.PolynomialHomogenization.PhysicalH1Realization

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

Physical Sobolev realization

The coefficient-weighted zero-trace pair is first realized as an exact H10Function. Adding a boundary datum gives a physical H1Function; subtracting the comparison function's zero-trace witness gives the final affine boundary relation.

On the bounded domain the coefficient agrees almost everywhere with a field uniformly elliptic almost everywhere on all of ℝ^d, and MemH1a0 reads the field only there, so the realization is read at that companion field.

theorem HCPolySupport.HighContrast.exists_h1Function_memAffineH10_of_memH1a0 {d : ℕ} [NeZero d] {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) {a : Source.AKL.Field d} (ha : AEUniformlyEllipticField a) {aPhysical : CoeffField d} (hae : ↑a =ᵐ[MeasureTheory.volume] aPhysical) (g₀ h : H1Function U) (hgh : MemAffineH10 U g₀ h) (uFun : Vec d → ℝ) (uGrad : Vec d → Vec d) (hu0 : MemH1a0 aPhysical U (fun (x : Vec d) => uFun x - g₀.toFun x) fun (x : Vec d) => uGrad x - g₀.grad x) : ∃ (u : H1Function U), u.toFun = uFun ∧ u.grad = uGrad ∧ MemAffineH10 U h u

A coefficient-weighted zero-trace pair with boundary datum g₀ has an exact Sobolev representative in the affine boundary class of h.