Coarse-graining support: Support.Sobolev.PotentialSolenoidalOriginCubeSymmetry #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
theorem
HCPolySupport.isPotentialOn_signFlip_openCubeSet_originCube
{d : ℕ}
{n : ℤ}
{f : Vec d → Vec d}
(hf : IsPotentialOn (openCubeSet (originCube d n)) f)
(i : Fin d)
:
IsPotentialOn (openCubeSet (originCube d n)) fun (x : Vec d) =>
(signFlipVecContinuousLinearEquiv i) (f ((signFlipVecContinuousLinearEquiv i) x))
theorem
HCPolySupport.isPotentialOn_swap_openCubeSet_originCube
{d : ℕ}
{n : ℤ}
{f : Vec d → Vec d}
(hf : IsPotentialOn (openCubeSet (originCube d n)) f)
(i j : Fin d)
:
IsPotentialOn (openCubeSet (originCube d n)) fun (x : Vec d) =>
(swapVecContinuousLinearEquiv i j) (f ((swapVecContinuousLinearEquiv i j) x))
theorem
HCPolySupport.isPotentialZeroTraceOn_signFlip_openCubeSet_originCube
{d : ℕ}
{n : ℤ}
{f : Vec d → Vec d}
(hf : IsPotentialZeroTraceOn (openCubeSet (originCube d n)) f)
(i : Fin d)
:
IsPotentialZeroTraceOn (openCubeSet (originCube d n)) fun (x : Vec d) =>
(signFlipVecContinuousLinearEquiv i) (f ((signFlipVecContinuousLinearEquiv i) x))
theorem
HCPolySupport.isPotentialZeroTraceOn_swap_openCubeSet_originCube
{d : ℕ}
{n : ℤ}
{f : Vec d → Vec d}
(hf : IsPotentialZeroTraceOn (openCubeSet (originCube d n)) f)
(i j : Fin d)
:
IsPotentialZeroTraceOn (openCubeSet (originCube d n)) fun (x : Vec d) =>
(swapVecContinuousLinearEquiv i j) (f ((swapVecContinuousLinearEquiv i j) x))
theorem
HCPolySupport.isSolenoidalZeroNormalTraceOn_signFlip_openCubeSet_originCube
{d : ℕ}
{n : ℤ}
{g : Vec d → Vec d}
(hg : IsSolenoidalZeroNormalTraceOn (openCubeSet (originCube d n)) g)
(i : Fin d)
:
IsSolenoidalZeroNormalTraceOn (openCubeSet (originCube d n)) fun (x : Vec d) =>
(signFlipVecContinuousLinearEquiv i) (g ((signFlipVecContinuousLinearEquiv i) x))
theorem
HCPolySupport.isSolenoidalZeroNormalTraceOn_swap_openCubeSet_originCube
{d : ℕ}
{n : ℤ}
{g : Vec d → Vec d}
(hg : IsSolenoidalZeroNormalTraceOn (openCubeSet (originCube d n)) g)
(i j : Fin d)
:
IsSolenoidalZeroNormalTraceOn (openCubeSet (originCube d n)) fun (x : Vec d) =>
(swapVecContinuousLinearEquiv i j) (g ((swapVecContinuousLinearEquiv i j) x))