Sobolev spaces (Bessel potential spaces)

In this file we define Sobolev spaces on normed vector spaces via the Fourier transform. These spaces are also known as Bessel potential spaces. The Bessel potential operator besselPotential is the Fourier multiplier with the symbol x ↦ (1 + ‖x‖ ^ 2) ^ (s / 2) and a tempered distribution u belongs to the Sobolev space H ^ {s, p} if besselPotential E F s u can be represented by a Lp function, informally this is written as 𝓕⁻ (fun x ↦ (1 + ‖x‖ ^ 2) ^ (s / 2)) 𝓕 u ∈ Lp.

Note that the Bessel potential is the operator (1 - (2 * π) ^ (-2) • Δ) ^ (s / 2) and not (1 - Δ) ^ (s / 2) due to the convention of the Fourier transform. This obviously does not impact the definition of the Sobolev spaces.

Main definitions

• TemperedDistribution.besselPotential: The Bessel potential operator is the Fourier multiplier with the function (1 + ‖x‖ ^ 2) ^ (s / 2).
• TemperedDistribution.memSobolev: A tempered distribution lies in the Sobolev space of order s and p if besselPotential E F s u ∈ Lp.

Main statements

• SchwartzMap.memSobolev: Each Schwartz function belongs to every Sobolev space
• TemperedDistribution.memSobolev_two_iff_fourier: The characterization of p = 2 Sobolev functions
• TemperedDistribution.MemSobolev.fourierMultiplierCLM_of_bounded: If u is a Sobolev function, then g • u is a Sobolev function of the same order provided g is bounded.
• TemperedDistribution.MemSobolev.lineDerivOp: If u is a Sobolev function of order s, then ∂_{m} u is a Sobolev function of order s - 1.
• TemperedDistribution.MemSobolev.laplacian: If u is a Sobolev function of order s, then Δ u is a Sobolev function of order s - 2.

References

• M. Taylor, Partial Differential Equations 1
• W. McLean, *Strongly Elliptic Systems and Boundary Integral Equations

noncomputable def TemperedDistribution.besselPotential (E : Type u_1) (F : Type u_2) [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedSpace ℂ F] (s : ℝ) : TemperedDistribution E F →L[ℂ] TemperedDistribution E F

The Bessel potential operator is the Fourier multiplier with the function (1 + ‖x‖ ^ 2) ^ (s / 2).

Note that due to the convention of the Fourier transform, this is the operator (1 - (2 * π) ^ (-2) • Δ) ^ (s / 2) not (1 - Δ) ^ (s / 2).

Equations

• TemperedDistribution.besselPotential E F s = TemperedDistribution.fourierMultiplierCLM F fun (x : E) => ↑((1 + ‖x‖ ^ 2) ^ (s / 2))

@[simp]

theorem TemperedDistribution.besselPotential_zero (E : Type u_1) (F : Type u_2) [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedSpace ℂ F] : besselPotential E F 0 = ContinuousLinearMap.id ℂ (TemperedDistribution E F)

@[simp]

theorem TemperedDistribution.besselPotential_besselPotential_apply {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedSpace ℂ F] (s s' : ℝ) (f : TemperedDistribution E F) : (besselPotential E F s') ((besselPotential E F s) f) = (besselPotential E F (s + s')) f

theorem TemperedDistribution.besselPotential_compL_besselPotential {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedSpace ℂ F] (s s' : ℝ) : (besselPotential E F s').comp (besselPotential E F s) = besselPotential E F (s + s')

theorem TemperedDistribution.besselPotential_neg_apply_eq_iff {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedSpace ℂ F] (s : ℝ) (f g : TemperedDistribution E F) : (besselPotential E F (-s)) f = g ↔ (besselPotential E F s) g = f

theorem TemperedDistribution.besselPotential_neg_one_lineDerivOp_eq {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedSpace ℂ F] {m : E} (f : TemperedDistribution E F) : (besselPotential E F (-1)) (LineDeriv.lineDerivOp m f) = (2 * ↑Real.pi * Complex.I) • (fourierMultiplierCLM F fun (x : E) => ↑(inner ℝ x m * (1 + ‖x‖ ^ 2) ^ (-1 / 2))) f

theorem TemperedDistribution.besselPotential_neg_two_laplacian_eq {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedSpace ℂ F] (f : TemperedDistribution E F) : (besselPotential E F (-2)) (Laplacian.laplacian f) = -(2 * Real.pi) ^ 2 • (fourierMultiplierCLM F fun (x : E) => ↑(‖x‖ ^ 2 * (1 + ‖x‖ ^ 2) ^ (-1))) f

@[simp]

theorem TemperedDistribution.fourier_besselPotential_eq_smulLeftCLM_fourier_apply {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [InnerProductSpace ℂ F] (s : ℝ) (f : TemperedDistribution E F) : FourierTransform.fourier ((besselPotential E F s) f) = (smulLeftCLM F fun (x : E) => ↑((1 + ‖x‖ ^ 2) ^ (s / 2))) (FourierTransform.fourier f)

def TemperedDistribution.MemSobolev {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedSpace ℂ F] [CompleteSpace F] (s : ℝ) (p : ENNReal) [hp : Fact (1 ≤ p)] (f : TemperedDistribution E F) : Prop

A tempered distribution f is a Sobolev function of order s if there exists an Lp function f' such that 𝓕⁻ (1 + ‖x‖ ^ 2) ^ (s / 2) 𝓕 f = f'.

Equations

• TemperedDistribution.MemSobolev s p f = ∃ (f' : ↥(MeasureTheory.Lp F p MeasureTheory.volume)), (TemperedDistribution.besselPotential E F s) f = MeasureTheory.Lp.toTemperedDistribution f'

theorem TemperedDistribution.memSobolev_zero_iff {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedSpace ℂ F] [CompleteSpace F] {p : ENNReal} [hp : Fact (1 ≤ p)] {f : TemperedDistribution E F} : MemSobolev 0 p f ↔ ∃ (f' : ↥(MeasureTheory.Lp F p MeasureTheory.volume)), f = MeasureTheory.Lp.toTemperedDistribution f'

theorem TemperedDistribution.MemSobolev.add {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedSpace ℂ F] [CompleteSpace F] {s : ℝ} {p : ENNReal} [hp : Fact (1 ≤ p)] {f g : TemperedDistribution E F} (hf : MemSobolev s p f) (hg : MemSobolev s p g) : MemSobolev s p (f + g)

theorem TemperedDistribution.MemSobolev.sub {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedSpace ℂ F] [CompleteSpace F] {s : ℝ} {p : ENNReal} [hp : Fact (1 ≤ p)] {f g : TemperedDistribution E F} (hf : MemSobolev s p f) (hg : MemSobolev s p g) : MemSobolev s p (f - g)

theorem TemperedDistribution.MemSobolev.neg {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedSpace ℂ F] [CompleteSpace F] {s : ℝ} {p : ENNReal} [hp : Fact (1 ≤ p)] {f : TemperedDistribution E F} (hf : MemSobolev s p f) : MemSobolev s p (-f)

theorem TemperedDistribution.MemSobolev.smul {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedSpace ℂ F] [CompleteSpace F] {s : ℝ} {p : ENNReal} [hp : Fact (1 ≤ p)] (c : ℂ) {f : TemperedDistribution E F} (hf : MemSobolev s p f) : MemSobolev s p (c • f)

@[simp]

theorem TemperedDistribution.memSobolev_fun_zero (E : Type u_1) (F : Type u_2) [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedSpace ℂ F] [CompleteSpace F] (s : ℝ) (p : ENNReal) [hp : Fact (1 ≤ p)] : MemSobolev s p 0

@[simp]

theorem TemperedDistribution.memSobolev_besselPotential_iff {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedSpace ℂ F] [CompleteSpace F] {s r : ℝ} {p : ENNReal} [hp : Fact (1 ≤ p)] {f : TemperedDistribution E F} : MemSobolev s p ((besselPotential E F r) f) ↔ MemSobolev (r + s) p f

theorem SchwartzMap.memSobolev {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedSpace ℂ F] [CompleteSpace F] {s : ℝ} {p : ENNReal} [hp : Fact (1 ≤ p)] (f : SchwartzMap E F) : TemperedDistribution.MemSobolev s p ((toTemperedDistributionCLM E F MeasureTheory.volume) f)

Schwartz functions are in every Sobolev space.

theorem TemperedDistribution.memSobolev_iff_exists_smulLeftCLM_fourier {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [InnerProductSpace ℂ F] [CompleteSpace F] {s : ℝ} {f : TemperedDistribution E F} : MemSobolev s 2 f ↔ ∃ (f' : ↥(MeasureTheory.Lp F 2 MeasureTheory.volume)), (smulLeftCLM F fun (x : E) => ↑((1 + ‖x‖ ^ 2) ^ (s / 2))) (FourierTransform.fourier f) = MeasureTheory.Lp.toTemperedDistribution f'

A tempered distribution belongs to the Sobolev space of order s and p = 2 if and only if its Fourier transform multiplied by (1 + ‖x‖ ^ 2) ^ (s / 2) is in Lp.

theorem TemperedDistribution.memSobolev_zero_iff_exists_fourier {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [InnerProductSpace ℂ F] [CompleteSpace F] {f : TemperedDistribution E F} : MemSobolev 0 2 f ↔ ∃ (f' : ↥(MeasureTheory.Lp F 2 MeasureTheory.volume)), FourierTransform.fourier f = MeasureTheory.Lp.toTemperedDistribution f'

theorem TemperedDistribution.MemSobolev.fourier_memL1 {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [InnerProductSpace ℂ F] [CompleteSpace F] {s : ℝ} (hs : ↑(Module.finrank ℝ E) < 2 * s) {f : TemperedDistribution E F} (hf : MemSobolev s 2 f) : ∃ (v : ↥(MeasureTheory.Lp F 1 MeasureTheory.volume)), FourierTransform.fourier f = MeasureTheory.Lp.toTemperedDistribution v

The Fourier transform of a Sobolev function of order s with s > d / 2 can be represented by a L1 function.

This is the main calculation of the Sobolev embedding theorem.

theorem TemperedDistribution.MemSobolev.fourierMultiplierCLM_of_bounded {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [InnerProductSpace ℂ F] [CompleteSpace F] {s : ℝ} {f : TemperedDistribution E F} (hf : MemSobolev s 2 f) {g : E → ℂ} (hg₁ : Function.HasTemperateGrowth g) (hg₂ : ∃ (C : ℝ), ∀ (x : E), ‖g x‖ ≤ C) : MemSobolev s 2 ((fourierMultiplierCLM F g) f)

The Fourier multiplier with a bounded function maps H ^ s to H ^ s.

theorem TemperedDistribution.MemSobolev.mono {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [InnerProductSpace ℂ F] [CompleteSpace F] {s s' : ℝ} (h : s' ≤ s) {f : TemperedDistribution E F} (hf : MemSobolev s 2 f) : MemSobolev s' 2 f

theorem TemperedDistribution.MemSobolev.lineDerivOp {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [InnerProductSpace ℂ F] [CompleteSpace F] {s : ℝ} {f : TemperedDistribution E F} (hf : MemSobolev s 2 f) {m : E} : MemSobolev (s - 1) 2 (LineDeriv.lineDerivOp m f)

The directional derivative maps H ^ s to H ^ {s - 1}.

theorem TemperedDistribution.MemSobolev.laplacian {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [InnerProductSpace ℂ F] [CompleteSpace F] {s : ℝ} {f : TemperedDistribution E F} (hf : MemSobolev s 2 f) : MemSobolev (s - 2) 2 (Laplacian.laplacian f)

The Laplacian maps H ^ s to H ^ {s - 2}.