Local translations of W^{1,p} functions

This file packages translation by a vector as an element of W^{1,p} on any smaller open set whose translate stays inside the original domain. Translation commutes with the weak gradient.

Main declarations

• TauCeti.W1p.translate: local translation from W^{1,p}(Ω) to W^{1,p}(V) when V + h ⊆ Ω.
• TauCeti.W1p.value_translate_ae: the value of a local translation.
• TauCeti.W1p.gradient_translate_ae: the weak gradient of a local translation.

noncomputable def TauCeti.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)] {Omega V : TopologicalSpace.Opens E} {h : E} (hVO : Set.MapsTo (fun (x : E) => x + h) ↑V ↑Omega) (u : ↥(W1p mu Omega p)) : ↥(W1p mu V p)

Local translation of a Sobolev function. If x + h ∈ Ω for every x ∈ V, this is the element of W^{1,p}(V) represented by x ↦ u (x + h). Its weak gradient is represented by x ↦ ∇u (x + h); see W1p.value_translate_ae and W1p.gradient_translate_ae.

Unlike extension by zero, local translation needs no boundary condition: the explicit inclusion V + h ⊆ Ω ensures that only values inside the original domain are used.

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.W1p.value_translate_ae {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)] {Omega V : TopologicalSpace.Opens E} {h : E} (hVO : Set.MapsTo (fun (x : E) => x + h) ↑V ↑Omega) (u : ↥(W1p mu Omega p)) : ↑↑(value (translate hVO u)) =ᵐ[mu.restrict ↑V] fun (x : E) => ↑↑(value u) (x + h)

Local translation is represented almost everywhere by precomposition with x ↦ x + h.

theorem TauCeti.W1p.gradient_translate_ae {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)] {Omega V : TopologicalSpace.Opens E} {h : E} (hVO : Set.MapsTo (fun (x : E) => x + h) ↑V ↑Omega) (u : ↥(W1p mu Omega p)) : ↑↑(gradient (translate hVO u)) =ᵐ[mu.restrict ↑V] fun (x : E) => ↑↑(gradient u) (x + h)

The weak gradient of a local translation is represented almost everywhere by the translated weak gradient.