Even-fold Sobolev extension construction #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
The construction uses the geometry, approximation and transport estimates from the companion basic module.
noncomputable def
HCPolySupport.foldExtension
{m : ℕ}
(lo hi : Vec (m + 1))
(hlt : ∀ (k : Fin (m + 1)), lo k < hi k)
(u : H1Function (Box lo hi))
:
FoldExtension lo hi u
Even-fold extension of an H¹(box) function.
Equations
- One or more equations did not get rendered due to their size.