Documentation

LeanPool.HighContrastHomogenization.Support.Sobolev.H1.Translation

Coarse-graining support: Support.Sobolev.H1.Translation #

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

source
noncomputable def HCPolySupport.H1Function.translate {d : ℕ} {U : Set (Vec d)} (u : H1Function U) (z : Vec d) :
H1Function (translateSet z U)

Translate an H¹(U) witness to H¹(U + z) by precomposing with x ↦ x - z.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem HCPolySupport.H1Function.translate_toFun {d : ℕ} {U : Set (Vec d)} (u : H1Function U) (z x : Vec d) :
    (u.translate z).toFun x = u.toFun (x - z)
    source
    @[simp]
    theorem HCPolySupport.H1Function.translate_grad {d : ℕ} {U : Set (Vec d)} (u : H1Function U) (z x : Vec d) :
    (u.translate z).grad x = u.grad (x - z)
    source
    noncomputable def HCPolySupport.H1Function.untranslate {d : ℕ} {U : Set (Vec d)} (z : Vec d) (u : H1Function (translateSet z U)) :
    H1Function U

    Pull an H¹(U + z) witness back to H¹(U) by precomposing with x ↦ x + z.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem HCPolySupport.H1Function.untranslate_toFun {d : ℕ} {U : Set (Vec d)} (z : Vec d) (u : H1Function (translateSet z U)) (x : Vec d) :
      (untranslate z u).toFun x = u.toFun (x + z)
      source
      @[simp]
      theorem HCPolySupport.H1Function.untranslate_grad {d : ℕ} {U : Set (Vec d)} (z : Vec d) (u : H1Function (translateSet z U)) (x : Vec d) :
      (untranslate z u).grad x = u.grad (x + z)
      source
      noncomputable def HCPolySupport.H10Function.translate {d : ℕ} {U : Set (Vec d)} (u : H10Function U) (z : Vec d) :
      H10Function (translateSet z U)

      Translate an H¹₀(U) witness to H¹₀(U + z) by precomposing with x ↦ x - z.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem HCPolySupport.H10Function.translate_toH1Function {d : ℕ} {U : Set (Vec d)} (u : H10Function U) (z : Vec d) :
        (u.translate z).toH1Function = u.translate z
        source
        noncomputable def HCPolySupport.H10Function.untranslate {d : ℕ} {U : Set (Vec d)} (z : Vec d) (u : H10Function (translateSet z U)) :
        H10Function U

        Pull an H¹₀(U + z) witness back to H¹₀(U) by precomposing with x ↦ x + z.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[simp]
          theorem HCPolySupport.H10Function.untranslate_toH1Function {d : ℕ} {U : Set (Vec d)} (z : Vec d) (u : H10Function (translateSet z U)) :
          (untranslate z u).toH1Function = H1Function.untranslate z u.toH1Function