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.foldExtensionFiniteP
{m : ℕ}
(lo hi : Vec (m + 1))
(hlt : ∀ (k : Fin (m + 1)), lo k < hi k)
(p : FiniteLpExponent)
(u : W1pFunction (Box lo hi) p.exponent)
:
FoldExtensionFiniteP lo hi p u
The finite-p even-fold extension of a Sobolev function on an open axis
box.
Equations
- One or more equations did not get rendered due to their size.