From Bessel-potential regularity to first-order weak derivatives

This file proves one direction of the agreement between the Fourier-theoretic and weak-derivative definitions of first-order Sobolev regularity on the whole space. If the tempered distribution associated to a real L² function belongs to Mathlib's Bessel-potential space H^{1,2}, then the function is the value component of an element of W^{1,2}.

Real representatives of the directional distributional derivatives connect Mathlib's complex Bessel-potential interface to the real weak-gradient interface. Their values along a finite basis determine an E-valued weak gradient.

Main declarations

• MeasureTheory.Lp.exists_real_lp_lineDeriv_of_memSobolev_zero: an order-zero Bessel-potential representative of a derivative of a real Lᵖ function may be chosen real.
• MeasureTheory.Lp.exists_real_l2_lineDeriv_of_memSobolev_one: every directional derivative of a real H^{1,2} function has a real L² representative.
• MeasureTheory.Lp.exists_w1p_value_eq_of_memSobolev_one: a real L² function whose associated tempered distribution lies in H^{1,2} belongs to weak-derivative W^{1,2}.

References

• L. C. Evans, Partial Differential Equations, Chapter 5, §5.8.
• M. Taylor, Partial Differential Equations I, Chapter 4.

theorem MeasureTheory.Lp.exists_real_lp_lineDeriv_of_memSobolev_zero {E : Type u_1} [MeasurableSpace E] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E] {p : ENNReal} [Fact (1 ≤ p)] (u : ↥(Lp ℝ p volume)) (v : E) (h : TemperedDistribution.MemSobolev 0 p (LineDeriv.lineDerivOp v (toTemperedDistribution (Complex.ofRealCLM.compLp u)))) : ∃ (u' : ↥(Lp ℝ p volume)), LineDeriv.lineDerivOp v (toTemperedDistribution (Complex.ofRealCLM.compLp u)) = toTemperedDistribution (Complex.ofRealCLM.compLp u')

If the derivative in direction v of the tempered distribution associated to a real Lᵖ function has Bessel-potential order zero, then it is represented by a real Lᵖ function.

This real representative makes the derivative available to the real weak-gradient interface.

theorem MeasureTheory.Lp.exists_real_l2_lineDeriv_of_memSobolev_one {E : Type u_1} [MeasurableSpace E] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E] (u : ↥(Lp ℝ 2 volume)) (h : TemperedDistribution.MemSobolev 1 2 (toTemperedDistribution (Complex.ofRealCLM.compLp u))) (v : E) : ∃ (u' : ↥(Lp ℝ 2 volume)), LineDeriv.lineDerivOp v (toTemperedDistribution (Complex.ofRealCLM.compLp u)) = toTemperedDistribution (Complex.ofRealCLM.compLp u')

Every directional derivative of a real H^{1,2} function has a real L² representative. This is the directional weak-derivative half of the inclusion H^{1,2} ⊆ W^{1,2}.

theorem MeasureTheory.Lp.exists_w1p_value_eq_of_memSobolev_one {E : Type u_1} [MeasurableSpace E] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E] (u : ↥(Lp ℝ 2 volume)) (h : TemperedDistribution.MemSobolev 1 2 (toTemperedDistribution (Complex.ofRealCLM.compLp u))) : ∃ (w : ↥(TauCeti.W1p volume ⊤ 2)), ↑↑(TauCeti.W1p.value w) =ᵐ[volume] ↑↑u

A real L² function whose associated tempered distribution belongs to the Bessel-potential space H^{1,2} is the value component of a weak-derivative Sobolev function in W^{1,2}(ℝⁿ).