Bessel-potential and weak-derivative Sobolev spaces agree

This file proves that the Fourier-theoretic and weak-derivative definitions of integer-order Lᵖ Sobolev regularity on the whole space agree for 1 < p < ∞ (Calderón's theorem): for every natural number k, a real Lᵖ function lies in Mathlib's Bessel-potential space H^{k,p}(ℝⁿ) exactly when it is the value of an element of the weak-derivative Sobolev space W^{k,p}(ℝⁿ). The two scales differ at p = 1 and p = ∞.

Both scales are described by first derivatives. A tempered distribution lies in H^{k+1,p} when it lies in Lᵖ and its directional derivatives lie in H^{k,p} (TemperedDistribution.memSobolev_natCast_add_one_iff, which rests on the Mihlin–Hörmander multiplier theorem when p ≠ 2), and a function lies in W^{k+1,p} when its directional weak derivatives lie in W^{k,p} (TauCeti.Wkp.exists_value_eq_iff_forall_exists_hasWeakLineDerivOn). On the whole space, weak derivatives are tempered-distributional derivatives (TauCeti.hasWeakLineDerivOn_iff_lineDerivOp_toTemperedDistribution_ofReal_eq), and an Lᵖ derivative of a real function has a real representative. Induction on k then matches the two descriptions.

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.memSobolev_natCast_iff_exists_wkp_value_eq: H^{k,p}(ℝⁿ) = W^{k,p}(ℝⁿ) for every natural k and 1 < p < ∞.
• TemperedDistribution.fderiv_apply_mem_realSobolevFunctions: the classical directional derivatives of a real C¹ function in H^{s+1,p}, s ≥ 0, lie in H^{s,p}.
• TemperedDistribution.mem_realSobolevFunctions_add_one_of_fderiv_apply: conversely, a real C¹ function in H^{s,p} whose classical directional derivatives lie in H^{s,p} lies in H^{s+1,p}.

References

• A.-P. Calderón, Lebesgue spaces of differentiable functions and distributions, Proc. Sympos. Pure Math. 4 (1961), 33–49.
• E. M. Stein, Singular Integrals and Differentiability Properties of Functions, Chapter V, §3.
• 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.memSobolev_natCast_iff_exists_wkp_value_eq {E : Type u_1} [MeasurableSpace E] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E] {p : ENNReal} [Fact (1 ≤ p)] (hp : 1 < p) (hp_top : p ≠ ⊤) (k : ℕ) (u : ↥(Lp ℝ p volume)) : TemperedDistribution.MemSobolev (↑k) p (toTemperedDistribution (Complex.ofRealCLM.compLp u)) ↔ ∃ (w : TauCeti.Wkp volume ⊤ p k), ↑↑(TauCeti.Wkp.value k w) =ᵐ[volume] ↑↑u

Weak-derivative and Bessel-potential Sobolev spaces agree (Calderón). For 1 < p < ∞ and every natural order k, a real Lᵖ function lies in Mathlib's Bessel-potential space H^{k,p}(ℝⁿ) exactly when it is the value of an element of the weak-derivative Sobolev space W^{k,p}(ℝⁿ).

theorem TemperedDistribution.fderiv_apply_mem_realSobolevFunctions {E : Type u_1} [MeasurableSpace E] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E] {p : ENNReal} [Fact (1 ≤ p)] (hp : 1 < p) (hp_top : p ≠ ⊤) {s : ℝ} (hs : 0 ≤ s) {f : E → ℝ} (hf : ContDiff ℝ 1 f) (hmem : f ∈ realSobolevFunctions E (s + 1) p) (v : E) : (fun (x : E) => (fderiv ℝ f x) v) ∈ realSobolevFunctions E s p

Classical derivatives of Sobolev functions. For 1 < p < ∞ and s ≥ 0, each classical directional derivative of a real C¹ function in H^{s+1,p} lies in H^{s,p}: the distributional derivative lies in H^{s,p} ⊆ Lᵖ, so it is a weak derivative, and a continuous classical derivative agrees with it almost everywhere.

theorem TemperedDistribution.mem_realSobolevFunctions_add_one_of_fderiv_apply {E : Type u_1} [MeasurableSpace E] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E] {p : ENNReal} [Fact (1 ≤ p)] (hp : 1 < p) (hp_top : p ≠ ⊤) {s : ℝ} {f : E → ℝ} (hf : ContDiff ℝ 1 f) (hmem : f ∈ realSobolevFunctions E s p) (hd : ∀ (v : E), (fun (x : E) => (fderiv ℝ f x) v) ∈ realSobolevFunctions E s p) : f ∈ realSobolevFunctions E (s + 1) p

Sobolev regularity from classical derivatives. For 1 < p < ∞, a real C¹ function in H^{s,p} whose classical directional derivatives all lie in H^{s,p} lies in H^{s+1,p}: the classical derivatives are weak derivatives, hence the distributional ones. This is the converse of fderiv_apply_mem_realSobolevFunctions.