Translation of weak derivatives

Weak differentiability is invariant under translations that stay inside the domain. If u has weak Fréchet derivative U on Ω, and x + h ∈ Ω for every x ∈ V, then x ↦ u (x + h) has weak derivative x ↦ U (x + h) on V. Consequently the difference quotient

x ↦ t⁻¹ • (u (x + t • w) - u x)

has weak derivative x ↦ t⁻¹ • (U (x + t • w) - U x) wherever both terms are defined. This is the local translation rule used by difference-quotient proofs of interior Sobolev regularity.

The proof translates each compactly supported test function in the opposite direction and uses translation invariance of the additive Haar measure. No regularity of the boundary of either domain is needed.

Main declarations

• TauCeti.HasWeakLineDerivOn.comp_add_right: translation of a weak directional derivative.
• TauCeti.HasWeakFDerivOn.comp_add_right: translation of a weak Fréchet derivative.
• TauCeti.HasWeakFDerivOn.translateLp: whole-space translation of an Lᵖ weak derivative.
• TauCeti.HasWeakFDerivOn.differenceQuotient: the weak derivative of a difference quotient.

References

• L. C. Evans, Partial Differential Equations, §5.8.2 and §6.3.1.
• D. Gilbarg, N. S. Trudinger, Elliptic Partial Differential Equations of Second Order, Lemma 7.23 and §8.8.

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

theorem TauCeti.HasWeakLineDerivOn.comp_add_right {E : Type u_1} {F : Type u_2} [MeasurableSpace E] [NormedAddCommGroup E] [NormedSpace ℝ E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {Omega V : TopologicalSpace.Opens E} {u u' : E → F} {v h : E} (hu : HasWeakLineDerivOn mu Omega u u' v) (hVO : Set.MapsTo (fun (x : E) => x + h) ↑V ↑Omega) : HasWeakLineDerivOn mu V (fun (x : E) => u (x + h)) (fun (x : E) => u' (x + h)) v

A translated function has the translated weak directional derivative on every open set whose translate lies in the original domain.

theorem TauCeti.HasWeakFDerivOn.comp_add_right {E : Type u_1} {F : Type u_2} [MeasurableSpace E] [NormedAddCommGroup E] [NormedSpace ℝ E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {Omega V : TopologicalSpace.Opens E} {u : E → F} {U : E → E →L[ℝ] F} {h : E} (hu : HasWeakFDerivOn mu Omega u U) (hVO : Set.MapsTo (fun (x : E) => x + h) ↑V ↑Omega) : HasWeakFDerivOn mu V (fun (x : E) => u (x + h)) fun (x : E) => U (x + h)

A translated function has the translated weak Fréchet derivative on every open set whose translate lies in the original domain.

theorem TauCeti.HasWeakFDerivOn.translateLp {E : Type u_1} {F : Type u_2} [MeasurableSpace E] [NormedAddCommGroup E] [NormedSpace ℝ E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {p : ENNReal} [Fact (1 ≤ p)] {f : ↥(MeasureTheory.Lp F p (mu.restrict ↑⊤))} {D : ↥(MeasureTheory.Lp (E →L[ℝ] F) p (mu.restrict ↑⊤))} (hf : HasWeakFDerivOn mu ⊤ ↑↑f ↑↑D) (h : E) : HasWeakFDerivOn mu ⊤ ↑↑(((mu.restrict ↑⊤).translateLp p h) f) ↑↑(((mu.restrict ↑⊤).translateLp p h) D)

On the whole space, translating an Lᵖ function and its weak Fréchet derivative by the same vector preserves the weak-derivative identity.

theorem TauCeti.HasWeakFDerivOn.differenceQuotient {E : Type u_1} {F : Type u_2} [MeasurableSpace E] [NormedAddCommGroup E] [NormedSpace ℝ E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {Omega V : TopologicalSpace.Opens E} {u : E → F} {U : E → E →L[ℝ] F} (hu : HasWeakFDerivOn mu Omega u U) (hV : V ≤ Omega) {w : E} {t : ℝ} (hVO : Set.MapsTo (fun (x : E) => x + t • w) ↑V ↑Omega) : HasWeakFDerivOn mu V (fun (x : E) => t⁻¹ • (u (x + t • w) - u x)) fun (x : E) => t⁻¹ • (U (x + t • w) - U x)

The weak derivative of the difference quotient of u in direction w with step t is the corresponding difference quotient of its weak derivative. Both V ⊆ Ω and V + t • w ⊆ Ω are explicit because both values occur in the quotient.