Coarse-graining support: Support.Sobolev.Foundations.PoincareW1p.Translation

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

theorem HCPolySupport.W1pFunction.valueLpSeminorm_translate_eq {d : ℕ} {U : Set (Vec d)} {p : ENNReal} (u : W1pFunction U p) (z : Vec d) : (u.translate z).valueLpSeminorm = u.valueLpSeminorm

Translation preserves the scalar L^p seminorm of a W^{1,p} witness.

theorem HCPolySupport.W1pFunction.integralAverage_translate_eq {d : ℕ} {U : Set (Vec d)} {p : ENNReal} (u : W1pFunction U p) (z : Vec d) : integralAverage (translateSet z U) (u.translate z).toFun = integralAverage U u.toFun

Translation commutes with the integral average.

theorem HCPolySupport.W1pFunction.subAverageLpSeminorm_translate_eq {d : ℕ} {U : Set (Vec d)} {p : ENNReal} (u : W1pFunction U p) (z : Vec d) : (u.translate z).subAverageLpSeminorm = u.subAverageLpSeminorm

Translation preserves the scalar L^p seminorm after subtracting the average.

theorem HCPolySupport.W1pFunction.gradCoordLpSeminorm_translate_eq {d : ℕ} {U : Set (Vec d)} {p : ENNReal} (u : W1pFunction U p) (z : Vec d) (i : Fin d) : (u.translate z).gradCoordLpSeminorm i = u.gradCoordLpSeminorm i

Translation preserves every coordinate gradient L^p seminorm.

theorem HCPolySupport.W1pFunction.gradientCoordLpSeminormSum_translate_eq {d : ℕ} {U : Set (Vec d)} {p : ENNReal} (u : W1pFunction U p) (z : Vec d) : (u.translate z).gradientCoordLpSeminormSum = u.gradientCoordLpSeminormSum

Translation preserves the coordinate-sum gradient L^p seminorm.

noncomputable def HCPolySupport.W1pFunction.castDomain {d : ℕ} {U : Set (Vec d)} {p : ENNReal} {V : Set (Vec d)} (hUV : U = V) (u : W1pFunction U p) : W1pFunction V p

Transport of a W^{1,p} function along an equality of its domains, retaining its value and weak gradient.

Equations

• HCPolySupport.W1pFunction.castDomain hUV u = hUV ▸ u

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

The W^{1,p} function on U given by x ↦ u(x + z) for a function on the translated domain U + z.

Equations

• HCPolySupport.W1pFunction.untranslateForPoincare z u = HCPolySupport.W1pFunction.castDomain ⋯ (u.translate (-z))

theorem HCPolySupport.W1pFunction.valueLpSeminorm_untranslateForPoincare_eq {d : ℕ} {U : Set (Vec d)} {p : ENNReal} (z : Vec d) (u : W1pFunction (translateSet z U) p) : (untranslateForPoincare z u).valueLpSeminorm = u.valueLpSeminorm

theorem HCPolySupport.W1pFunction.gradientCoordLpSeminormSum_untranslateForPoincare_eq {d : ℕ} {U : Set (Vec d)} {p : ENNReal} (z : Vec d) (u : W1pFunction (translateSet z U) p) : (untranslateForPoincare z u).gradientCoordLpSeminormSum = u.gradientCoordLpSeminormSum

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

Translate a mean-zero W^{1,p}(U) witness to W^{1,p}(U + z).

Equations

• u.translate z = { toW1pFunction := u.toW1pFunction.translate z, meanZero := ⋯ }

@[simp]

theorem HCPolySupport.W1pMeanZeroFunction.translate_toW1pFunction {d : ℕ} {U : Set (Vec d)} {p : ENNReal} (u : W1pMeanZeroFunction U p) (z : Vec d) : (u.translate z).toW1pFunction = u.toW1pFunction.translate z

noncomputable def HCPolySupport.W1pMeanZeroFunction.untranslateForPoincare {d : ℕ} {U : Set (Vec d)} {p : ENNReal} (z : Vec d) (u : W1pMeanZeroFunction (translateSet z U) p) : W1pMeanZeroFunction U p

The mean-zero W^{1,p} function on U given by x ↦ u(x + z) for a mean-zero function on `U

• z`.

Equations

• HCPolySupport.W1pMeanZeroFunction.untranslateForPoincare z u = { toW1pFunction := HCPolySupport.W1pFunction.untranslateForPoincare z u.toW1pFunction, meanZero := ⋯ }

noncomputable def HCPolySupport.W1pPoincareEstimate.translate {d : ℕ} {U : Set (Vec d)} {p : ENNReal} (hC : W1pPoincareEstimate U p) (z : Vec d) : W1pPoincareEstimate (translateSet z U) p

Translate a finite-p Poincare estimate from U to U + z unchanged.

Equations

• hC.translate z = { constantValue := hC.constantValue, constant_nonneg := ⋯, bound := ⋯ }

@[simp]

theorem HCPolySupport.W1pPoincareEstimate.translate_constant {d : ℕ} {U : Set (Vec d)} {p : ENNReal} (hC : W1pPoincareEstimate U p) (z : Vec d) : (hC.translate z).constantValue = hC.constantValue