Documentation

LeanPool.HighContrastHomogenization.Support.Sobolev.H1.OriginCubeSymmetry.H10Actions

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.

source
noncomputable def HCPolySupport.H10Function.signFlipOnOpenCubeSetOriginCube {d : ℕ} {n : ℤ} (u : H10Function (openCubeSet (originCube d n))) (i : Fin d) :
H10Function (openCubeSet (originCube d n))

Precompose an H¹₀ witness on the open centered cube with a coordinate sign flip.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem HCPolySupport.H10Function.signFlipOnOpenCubeSetOriginCube_toH1Function {d : ℕ} {n : ℤ} (u : H10Function (openCubeSet (originCube d n))) (i : Fin d) :
    (u.signFlipOnOpenCubeSetOriginCube i).toH1Function = u.signFlipOnOpenCubeSetOriginCube i
    source
    noncomputable def HCPolySupport.H10Function.swapOnOpenCubeSetOriginCube {d : ℕ} {n : ℤ} (u : H10Function (openCubeSet (originCube d n))) (i j : Fin d) :
    H10Function (openCubeSet (originCube d n))

    Precompose an H¹₀ witness on the open centered cube with a coordinate swap.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem HCPolySupport.H10Function.swapOnOpenCubeSetOriginCube_toH1Function {d : ℕ} {n : ℤ} (u : H10Function (openCubeSet (originCube d n))) (i j : Fin d) :
      (u.swapOnOpenCubeSetOriginCube i j).toH1Function = u.swapOnOpenCubeSetOriginCube i j