Translation of arbitrary-order Sobolev functions

Translation on the whole space preserves every weak derivative. Thus translating an element of W^{k,p} translates its value and each field in its iterated weak-gradient chain. The resulting operator is a linear isometry. This is the whole-space symmetry needed to average translated Sobolev functions against smooth kernels in the density argument.

The construction follows the weak-derivative graph defining W^{k,p}. The first stage uses TauCeti.W1p.translate; later stages use TauCeti.HasWeakFDerivOn.translateLp to translate the preceding stage and its highest weak derivative together. See Evans, Partial Differential Equations, §5.3.1.

theorem TauCeti.Wkp.instIsAddHaarMeasureRestrictCoeOpensTop {E : Type u_1} [MeasurableSpace E] [NormedAddCommGroup E] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] : (mu.restrict ↑⊤).IsAddHaarMeasure

noncomputable def TauCeti.Wkp.translate {E : Type u_1} [MeasurableSpace E] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {p : ENNReal} [Fact (1 ≤ p)] (h : E) (k : ℕ) : Wkp mu ⊤ p k → Wkp mu ⊤ p k

Translation of a whole-space Sobolev function. At every order it translates the value and all recorded weak derivatives by the same vector.

Equations

• TauCeti.Wkp.translate h 0 = ⇑((mu.restrict ↑⊤).translateLp p h)
• TauCeti.Wkp.translate h k.succ = fun (u : TauCeti.Wkp mu ⊤ p (k + 1)) => TauCeti.Wkp.Translated.element✝ (TauCeti.Wkp.translated✝ h k u)

@[simp]

theorem TauCeti.Wkp.value_translate {E : Type u_1} [MeasurableSpace E] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {p : ENNReal} [Fact (1 ≤ p)] (h : E) (k : ℕ) (u : Wkp mu ⊤ p k) : value k (translate h k u) = ((mu.restrict ↑⊤).translateLp p h) (value k u)

The value of a translated Sobolev function is the translated value.

theorem TauCeti.Wkp.translate_one_eq_W1p_translate {E : Type u_1} [MeasurableSpace E] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {p : ENNReal} [Fact (1 ≤ p)] (h : E) (u : Wkp mu ⊤ p 1) : translate h 1 u = W1p.translate ⋯ u

At order one, whole-space translation agrees with the existing local translation when the source and target domains are both the whole space.

@[simp]

theorem TauCeti.Wkp.iteratedGradient_translate {E : Type u_1} [MeasurableSpace E] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {p : ENNReal} [Fact (1 ≤ p)] (h : E) (k : ℕ) (u : Wkp mu ⊤ p (k + 1)) : iteratedGradient k (translate h (k + 1) u) = ((mu.restrict ↑⊤).translateLp p h) (iteratedGradient k u)

The highest weak derivative of a translated Sobolev function is the translated highest weak derivative.

@[simp]

theorem TauCeti.Wkp.lowerOrder_translate {E : Type u_1} [MeasurableSpace E] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {p : ENNReal} [Fact (1 ≤ p)] (h : E) (k : ℕ) (u : Wkp mu ⊤ p (k + 1)) : lowerOrder k (translate h (k + 1) u) = translate h k (lowerOrder k u)

Translation commutes with forgetting the highest weak derivative.

@[simp]

theorem TauCeti.Wkp.translate_zero {E : Type u_1} [MeasurableSpace E] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {p : ENNReal} [Fact (1 ≤ p)] (k : ℕ) (u : Wkp mu ⊤ p k) : translate 0 k u = u

Translation by zero fixes every whole-space Sobolev function.

theorem TauCeti.Wkp.translate_add {E : Type u_1} [MeasurableSpace E] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {p : ENNReal} [Fact (1 ≤ p)] (h₁ h₂ : E) (k : ℕ) (u : Wkp mu ⊤ p k) : translate (h₁ + h₂) k u = translate h₂ k (translate h₁ k u)

Two successive Sobolev translations compose by addition of their vectors.

theorem TauCeti.Wkp.continuous_translate {E : Type u_1} [MeasurableSpace E] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {p : ENNReal} [Fact (1 ≤ p)] (hp : p ≠ ⊤) (k : ℕ) (u : Wkp mu ⊤ p k) : Continuous fun (h : E) => translate h k u

For finite p, translation of a fixed whole-space Sobolev function varies continuously with the translation vector.

@[simp]

theorem TauCeti.Wkp.norm_translate {E : Type u_1} [MeasurableSpace E] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {p : ENNReal} [Fact (1 ≤ p)] (h : E) (k : ℕ) (u : Wkp mu ⊤ p k) : ‖translate h k u‖ = ‖u‖

Translation preserves the iterated graph norm at every Sobolev order.

noncomputable def TauCeti.Wkp.translateLIE {E : Type u_1} [MeasurableSpace E] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {p : ENNReal} [Fact (1 ≤ p)] (h : E) (k : ℕ) : Wkp mu ⊤ p k ≃ₗᵢ[ℝ] Wkp mu ⊤ p k

Whole-space translation is a linear isometric equivalence on W^{k,p}. Its inverse is translation by -h; it acts on the value and every weak derivative by Lᵖ translation.

Equations

• TauCeti.Wkp.translateLIE h k = LinearIsometryEquiv.ofSurjective (TauCeti.Wkp.translateLI✝ h k) ⋯

@[simp]

theorem TauCeti.Wkp.translateLIE_apply {E : Type u_1} [MeasurableSpace E] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {p : ENNReal} [Fact (1 ≤ p)] (h : E) (k : ℕ) (u : Wkp mu ⊤ p k) : (translateLIE h k) u = translate h k u

@[simp]

theorem TauCeti.Wkp.translateLIE_symm {E : Type u_1} [MeasurableSpace E] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {p : ENNReal} [Fact (1 ≤ p)] (h : E) (k : ℕ) : (translateLIE h k).symm = translateLIE (-h) k

The inverse of Sobolev translation is translation by the negative vector.

@[simp]

theorem TauCeti.Wkp.translateLIE_zero {E : Type u_1} [MeasurableSpace E] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {p : ENNReal} [Fact (1 ≤ p)] (k : ℕ) : translateLIE 0 k = LinearIsometryEquiv.refl ℝ (Wkp mu ⊤ p k)

Translation by zero is the identity equivalence.

theorem TauCeti.Wkp.translateLIE_add {E : Type u_1} [MeasurableSpace E] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {p : ENNReal} [Fact (1 ≤ p)] (h₁ h₂ : E) (k : ℕ) : translateLIE (h₁ + h₂) k = (translateLIE h₁ k).trans (translateLIE h₂ k)

Sobolev translation equivalences compose by addition of their vectors.