Documentation

LeanPool.HighContrastHomogenization.Support.Sobolev.Foundations.CubeDirichletH2.PoissonTranslation

Coarse-graining support: Support.Sobolev.Foundations.CubeDirichletH2.PoissonTranslation #

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

source
noncomputable def HCPolySupport.CubeDirichletWeakPoissonProblem.untranslateToOriginFunction {d : ℕ} (Q : TriadicCube d) (u : H10Function (openCubeSet Q)) :
H10Function (openCubeSet (originCube d Q.scale))

Pull an arbitrary-cube zero-trace function back to the centered cube of the same scale.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem HCPolySupport.CubeDirichletWeakPoissonProblem.untranslateToOriginFunction_toFun {d : ℕ} (Q : TriadicCube d) (u : H10Function (openCubeSet Q)) (x : Vec d) :
    (untranslateToOriginFunction Q u).toFun x = u.toFun (x + triadicCubeShift Q)
    source
    @[simp]
    theorem HCPolySupport.CubeDirichletWeakPoissonProblem.untranslateToOriginFunction_grad {d : ℕ} (Q : TriadicCube d) (u : H10Function (openCubeSet Q)) (x : Vec d) :
    (untranslateToOriginFunction Q u).grad x = u.grad (x + triadicCubeShift Q)
    source
    theorem HCPolySupport.CubeDirichletWeakPoissonProblem.untranslateToOrigin {d : ℕ} {Q : TriadicCube d} {u : H10Function (openCubeSet Q)} {F : Vec d → ℝ} (hweak : CubeDirichletWeakPoissonProblem Q u F) :
    CubeDirichletWeakPoissonProblem (originCube d Q.scale) (untranslateToOriginFunction Q u) fun (x : Vec d) => F (x + triadicCubeShift Q)

    Pull a cube Dirichlet weak Poisson equation back to the centered cube of the same scale.

    source
    theorem HCPolySupport.CubeDirichletWeakPoissonProblem.untranslateToOriginFunction_translate_grad {d : ℕ} (Q : TriadicCube d) (u : H10Function (openCubeSet Q)) (x : Vec d) :
    ((untranslateToOriginFunction Q u).translate (triadicCubeShift Q)).grad x = u.grad x

    Translating the centered pullback recovers the original arbitrary-cube gradient.