High-contrast homogenization: Provider.Regularity.H1aOpenSubsetGradientRealization

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

Realizing an H1a gradient on an interior open carrier

The root MemH1a hypothesis is posed on the closed physical ellipsoid. A rounded physical cube used by the finite recurrence is an open bounded convex subset of that carrier. The global smooth approximation in MemH1a restricts to the cube, so its gradient slot has an actual local H1Function representative there. No membership statement on a widened or changed domain is introduced.

theorem HCPolySupport.HighContrast.isPotentialOn_grad_on_openSubset_of_memH1a {d : ℕ} {U V : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) (hUV : U ⊆ V) (hVb : Bornology.IsBounded V) {b : CoeffField d} {lam Lam : ℝ} (hlam : 0 < lam) (hell : ∀ᵐ (x : Vec d), IsEllipticMatrix lam Lam (b x)) {u : Vec d → ℝ} {Du : Vec d → Vec d} (hu : MemH1a b V u Du) : IsPotentialOn U Du

On an open bounded convex subset of a bounded MemH1a carrier, the gradient slot is the gradient of an actual local H1Function.