Coordinate symmetry of centered-cube H¹ functions #
Constructor transport from the Apache-2.0 CoarseGraining development, pinned at
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
The original namespaces, definitions, theorem statements, and proofs are retained.
noncomputable def
HCPolySupport.H1Function.signFlipOnOpenCubeSetOriginCube
{d : ℕ}
{n : ℤ}
(u : H1Function (openCubeSet (originCube d n)))
(i : Fin d)
:
H1Function (openCubeSet (originCube d n))
Precompose an H¹ witness on the open centered cube with a coordinate sign
flip, transporting the weak gradient by the same sign flip.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
HCPolySupport.H1Function.swapOnOpenCubeSetOriginCube
{d : ℕ}
{n : ℤ}
(u : H1Function (openCubeSet (originCube d n)))
(i j : Fin d)
:
H1Function (openCubeSet (originCube d n))
Precompose an H¹ witness on the open centered cube with a coordinate swap,
transporting the weak gradient by the same swap.
Equations
- One or more equations did not get rendered due to their size.