Coarse-graining support: Support.Sobolev.PotentialSolenoidalTranslation #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
theorem
HCPolySupport.isPotentialOn_translateSet
{d : ℕ}
{U : Set (Vec d)}
{f : Vec d → Vec d}
(hf : IsPotentialOn U f)
(z : Vec d)
:
IsPotentialOn (translateSet z U) fun (x : Vec d) => f (x - z)
theorem
HCPolySupport.isPotentialZeroTraceOn_translateSet
{d : ℕ}
{U : Set (Vec d)}
{f : Vec d → Vec d}
(hf : IsPotentialZeroTraceOn U f)
(z : Vec d)
:
IsPotentialZeroTraceOn (translateSet z U) fun (x : Vec d) => f (x - z)
theorem
HCPolySupport.isSolenoidalOn_translateSet
{d : ℕ}
{U : Set (Vec d)}
{g : Vec d → Vec d}
(hg : IsSolenoidalOn U g)
(z : Vec d)
:
IsSolenoidalOn (translateSet z U) fun (x : Vec d) => g (x - z)
theorem
HCPolySupport.isSolenoidalZeroNormalTraceOn_translateSet
{d : ℕ}
{U : Set (Vec d)}
{g : Vec d → Vec d}
(hg : IsSolenoidalZeroNormalTraceOn U g)
(z : Vec d)
:
IsSolenoidalZeroNormalTraceOn (translateSet z U) fun (x : Vec d) => g (x - z)