Translation of a weak gradient

The global approximation theorem shifts a function into the domain before mollifying it, so that the mollification of the shift is defined on a neighbourhood of the piece of boundary in view. The shift has to move the weak gradient with it, which is what this file records.

Translation is the second of the two rigid motions the extension operator runs on, beside the reflection of EllipticPdes.Extension.Reflect. It is measure preserving and its derivative is the identity, so it moves a weak gradient with no sign and no Jacobian.

Main declarations

• EllipticPdes.Extension.partialD_comp_translate: the partial derivatives of a translate.
• EllipticPdes.Extension.hasWeakGradOn_comp_translate: the weak gradient of a translate.
• EllipticPdes.Extension.eLpNorm_comp_translate: translation preserves every Lᵖ seminorm.

References

L. C. Evans, Partial Differential Equations (2nd ed.), §5.3.3, Theorem 3.

The translation

theorem EllipticPdes.Extension.measurePreserving_translate {d : ℕ} (h : EuclideanSpace ℝ (Fin d)) : MeasureTheory.MeasurePreserving (fun (y : EuclideanSpace ℝ (Fin d)) => y + h) MeasureTheory.volume MeasureTheory.volume

theorem EllipticPdes.Extension.measurableEmbedding_translate {d : ℕ} (h : EuclideanSpace ℝ (Fin d)) : MeasurableEmbedding fun (y : EuclideanSpace ℝ (Fin d)) => y + h

Derivatives and supports

theorem EllipticPdes.Extension.partialD_comp_translate {d : ℕ} {φ : EuclideanSpace ℝ (Fin d) → ℝ} (hφ : Differentiable ℝ φ) (h : EuclideanSpace ℝ (Fin d)) (k : Fin d) (x : EuclideanSpace ℝ (Fin d)) : Sobolev.partialD k (fun (y : EuclideanSpace ℝ (Fin d)) => φ (y + h)) x = Sobolev.partialD k φ (x + h)

Partial derivatives of a translate. Translation has derivative the identity, so a partial derivative translates with no factor.

theorem EllipticPdes.Extension.contDiff_comp_translate {d : ℕ} {φ : EuclideanSpace ℝ (Fin d) → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (h : EuclideanSpace ℝ (Fin d)) : ContDiff ℝ ↑⊤ fun (y : EuclideanSpace ℝ (Fin d)) => φ (y + h)

theorem EllipticPdes.Extension.hasCompactSupport_comp_translate {d : ℕ} {φ : EuclideanSpace ℝ (Fin d) → ℝ} (hφ : HasCompactSupport φ) (h : EuclideanSpace ℝ (Fin d)) : HasCompactSupport fun (y : EuclideanSpace ℝ (Fin d)) => φ (y + h)

theorem EllipticPdes.Extension.tsupport_comp_translate_subset {d : ℕ} {φ : EuclideanSpace ℝ (Fin d) → ℝ} {B : Set (EuclideanSpace ℝ (Fin d))} (h : EuclideanSpace ℝ (Fin d)) (hs : tsupport φ ⊆ (fun (y : EuclideanSpace ℝ (Fin d)) => y + h) ⁻¹' B) : (tsupport fun (y : EuclideanSpace ℝ (Fin d)) => φ (y - h)) ⊆ B

The weak gradient of a translate

theorem EllipticPdes.Extension.hasWeakGradOn_comp_translate {d : ℕ} {B : Set (EuclideanSpace ℝ (Fin d))} {u : EuclideanSpace ℝ (Fin d) → ℝ} {g : Fin d → EuclideanSpace ℝ (Fin d) → ℝ} (hw : Embedding.HasWeakGradOn B u g) (h : EuclideanSpace ℝ (Fin d)) : Embedding.HasWeakGradOn ((fun (y : EuclideanSpace ℝ (Fin d)) => y + h) ⁻¹' B) (fun (y : EuclideanSpace ℝ (Fin d)) => u (y + h)) fun (k : Fin d) (y : EuclideanSpace ℝ (Fin d)) => g k (y + h)

Translation of a weak gradient. If u has weak gradient g on B, then u(· + h) has weak gradient k ↦ gₖ(· + h) on the preimage of B under the translation.

The proof is the change of variables under a measure-preserving translation, twice: once to move the test function onto B, where the hypothesis applies, and once to move the conclusion back.

theorem EllipticPdes.Extension.eLpNorm_comp_translate {d : ℕ} {f : EuclideanSpace ℝ (Fin d) → ℝ} (hf : MeasureTheory.AEStronglyMeasurable f MeasureTheory.volume) (h : EuclideanSpace ℝ (Fin d)) (p : ENNReal) : MeasureTheory.eLpNorm (fun (y : EuclideanSpace ℝ (Fin d)) => f (y + h)) p MeasureTheory.volume = MeasureTheory.eLpNorm f p MeasureTheory.volume

Translation preserves every Lᵖ seminorm.