Documentation

LeanPool.HighContrastHomogenization.Support.Sobolev.W1p.Translation

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

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

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

Translate a W^{1,p}(U) witness to W^{1,p}(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.W1pFunction.translate_toFun {d : ℕ} {U : Set (Vec d)} {p : ENNReal} (u : W1pFunction U p) (z x : Vec d) :
    (u.translate z).toFun x = u.toFun (x - z)
    source
    @[simp]
    theorem HCPolySupport.W1pFunction.translate_grad {d : ℕ} {U : Set (Vec d)} {p : ENNReal} (u : W1pFunction U p) (z x : Vec d) :
    (u.translate z).grad x = u.grad (x - z)
    source
    noncomputable def HCPolySupport.W10pFunction.translate {d : ℕ} {U : Set (Vec d)} {p : ENNReal} (u : W10pFunction U p) (z : Vec d) :
    W10pFunction (translateSet z U) p

    Translate a W^{1,p}_0(U) witness to W^{1,p}_0(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.W10pFunction.translate_toW1pFunction {d : ℕ} {U : Set (Vec d)} {p : ENNReal} (u : W10pFunction U p) (z : Vec d) :
      (u.translate z).toW1pFunction = u.translate z