Sobolev embedding theorem

DefinitionHomogeneous Sobolev seminorm for the Hölder embedding#✓fully proved

For a real number \(s\) and a Schwartz function \(f : \mathbb{R} \to \mathbb{C}\) with Fourier transform \(\hat f(\xi) = \int_{\mathbb{R}} e^{-2\pi i x \xi} f(x) \, dx\), the homogeneous Sobolev seminorm of \(f\) is

\[ \|f\|_{\dot H^s} = \left( \int_{\mathbb{R}} |\xi|^{2s} \, |\hat f(\xi)|^2 \, d\xi \right)^{1/2}, \]

where the integral is taken to be \(0\) when the integrand is not integrable.

noncomputable def dotHSeminorm (s : ℝ) (f : SchwartzMap ℝ ℂ) : ℝ :=
  Real.sqrt (∫ ξ : ℝ, Real.rpow ‖ξ‖ (2 * s) * ‖(𝓕 f) ξ‖ ^ 2)

Used by 1

Used byThe homogeneous Sobolev seminorm controls the Hölder seminorm

TheoremThe homogeneous Sobolev seminorm controls the Hölder seminorm#●ready to prove

Let \(s \in (\tfrac12, 1]\), and for a Schwartz function \(f : \mathbb{R} \to \mathbb{C}\) with Fourier transform \(\hat f\) let \(\|f\|_{\dot H^s} = \left( \int_{\mathbb{R}} |\xi|^{2s} |\hat f(\xi)|^2 \, d\xi \right)^{1/2}\) be its homogeneous Sobolev seminorm. There is a constant \(C_3 > 0\) such that for every Schwartz function \(f : \mathbb{R} \to \mathbb{C}\),

\[ \sup_{x \ne y} \frac{|f(x) - f(y)|}{|x - y|^{s - \frac12}} \le C_3 \, \|f\|_{\dot H^s}. \]

public theorem_wanted exists_holderSeminorm_le_mul_dotHSeminorm
    (s : ℝ) (hs : s ∈ Set.Ioc (1 / 2 : ℝ) 1) :
    ∃ C3 > 0, ∀ f : SchwartzMap ℝ ℂ,
      sSup
          (Set.range
            (fun p : {xy : ℝ × ℝ // xy.1 ≠ xy.2} =>
              ‖f p.1.1 - f p.1.2‖ / Real.rpow ‖p.1.1 - p.1.2‖ (s - 1 / 2)))
        ≤ C3 * dotHSeminorm s f

Sources

• MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level II (Functional analysis; Linear function spaces and their duals), problem ma_proofbench_l2_21.

Uses 1

Statement usesHomogeneous Sobolev seminorm for the Hölder embedding

AbbreviationEuclidean space \(\mathbb{R}^n\)#✓fully proved

For a natural number \(n\), \(\mathbb{R}^n\) denotes the real Euclidean space of dimension \(n\): real vectors with coordinates indexed by \(0, \dots, n-1\), with the Euclidean inner product and norm.

abbrev E (n : ℕ) := EuclideanSpace ℝ (Fin n)

Used by 6

Used byWeak derivative · Hölder space \(C^{r,\alpha}(\mathbb{R}^n)\) · Sobolev space \(W^{k,p}(\mathbb{R}^n)\) · Mixed partial derivative · Partial derivative · Sobolev embedding theorem (Morrey regime)

DefinitionPartial derivative#✓fully proved

For a coordinate index \(i \in \{0, \dots, n-1\}\) and a function \(\varphi : \mathbb{R}^n \to \mathbb{R}\), the partial derivative \(\partial_i \varphi\) is the function \(\mathbb{R}^n \to \mathbb{R}\) sending \(x\) to \(D\varphi(x)(e_i)\), the Fréchet derivative of \(\varphi\) at \(x\) applied to the \(i\)-th standard basis vector \(e_i\). At points where \(\varphi\) is not differentiable its value is \(0\).

noncomputable def partialDeriv {n : ℕ} (i : Fin n) (φ : E n → ℝ) : E n → ℝ :=
  fun x => fderiv ℝ φ x (EuclideanSpace.single i (1 : ℝ))

Uses 1 · Used by 1

Statement usesEuclidean space \(\mathbb{R}^n\)

Used byMixed partial derivative

DefinitionMixed partial derivative#✓fully proved

For a multi-index \(m = (m_0, \dots, m_{n-1})\) of natural numbers and a function \(\varphi : \mathbb{R}^n \to \mathbb{R}\), the mixed partial derivative is \(D^m \varphi = \partial_0^{m_0} \partial_1^{m_1} \cdots \partial_{n-1}^{m_{n-1}} \varphi\), where \(\partial_i^{j}\) is the \(j\)-fold iterate of the partial derivative \(\partial_i\); thus \(\partial_{n-1}\) is applied first and \(\partial_0\) last.

noncomputable def mixedDeriv {n : ℕ} (m : Fin n → ℕ) (φ : E n → ℝ) : E n → ℝ :=
  (List.finRange n).foldr (fun i ψ => (partialDeriv i)^[m i] ψ) φ

Uses 2 · Used by 1

Statement usesEuclidean space \(\mathbb{R}^n\) · Partial derivative

Used byWeak derivative

DefinitionWeak derivative#✓fully proved

Let \(f, g : \mathbb{R}^n \to \mathbb{R}\) and let \(m = (m_0, \dots, m_{n-1})\) be a multi-index of order \(|m| = m_0 + \cdots + m_{n-1}\). Then \(g\) is a weak derivative \(D^m f\) of \(f\) when every smooth (\(C^\infty\)) compactly supported function \(\varphi : \mathbb{R}^n \to \mathbb{R}\) satisfies

\[\int_{\mathbb{R}^n} f \, D^m \varphi \, dx = (-1)^{|m|} \int_{\mathbb{R}^n} g \, \varphi \, dx,\]

where \(D^m \varphi\) is the classical mixed partial derivative and each integral is the Lebesgue integral, taken to be \(0\) when the integrand is not integrable.

def IsWeakDeriv {n : ℕ} (f g : E n → ℝ) (m : Fin n → ℕ) : Prop :=
  ∀ φ : E n → ℝ, ContDiff ℝ (⊤ : ℕ∞) φ → HasCompactSupport φ →
    ∫ x, f x * mixedDeriv m φ x = (-1) ^ (∑ i, m i) * ∫ x, g x * φ x

Uses 2 · Used by 1

Statement usesEuclidean space \(\mathbb{R}^n\) · Mixed partial derivative

Used bySobolev space \(W^{k,p}(\mathbb{R}^n)\)

DefinitionSobolev space \(W^{k,p}(\mathbb{R}^n)\)#✓fully proved

For a natural number \(k\) and \(p \in [0, \infty]\), a function \(f : \mathbb{R}^n \to \mathbb{R}\) belongs to \(W^{k,p}(\mathbb{R}^n)\) when \(f\) is locally integrable and, for every multi-index \(m = (m_0, \dots, m_{n-1})\) of natural numbers with \(m_0 + \cdots + m_{n-1} \le k\), \(f\) has a weak derivative \(D^m f\) that lies in \(L^p(\mathbb{R}^n)\). Local integrability and \(L^p\) are with respect to Lebesgue measure.

def MemSobolevWk {n : ℕ} (k : ℕ) (p : ℝ≥0∞) (f : E n → ℝ) : Prop :=
  LocallyIntegrable f volume ∧
  ∀ m : Fin n → ℕ, (∑ i, m i) ≤ k →
    ∃ g : E n → ℝ, IsWeakDeriv f g m ∧ MemLp g p volume

Uses 2 · Used by 1

Statement usesEuclidean space \(\mathbb{R}^n\) · Weak derivative

Used bySobolev embedding theorem (Morrey regime)

DefinitionHölder space \(C^{r,\alpha}(\mathbb{R}^n)\)#✓fully proved

For a natural number \(r\) and a real number \(\alpha\), a function \(g : \mathbb{R}^n \to \mathbb{R}\) belongs to \(C^{r,\alpha}(\mathbb{R}^n)\) when \(g\) is \(r\) times continuously differentiable, its iterated derivatives \(D^j g\) for \(j \le r\) are bounded on \(\mathbb{R}^n\), and its \(r\)-th derivative is \(\alpha\)-Hölder: there is \(C \ge 0\) with \(\|D^r g(x) - D^r g(y)\| \le C \|x - y\|^{\alpha}\) for all \(x, y \in \mathbb{R}^n\). Here \(D^j g(x)\) is the \(j\)-th Fréchet derivative of \(g\) at \(x\), a \(j\)-linear map measured in the operator norm, and a negative \(\alpha\) is replaced by \(0\).

def MemHolder {n : ℕ} (r : ℕ) (α : ℝ) (g : E n → ℝ) : Prop :=
  ContDiff ℝ (r : ℕ∞) g ∧
  (∃ C : NNReal, HolderWith C α.toNNReal (iteratedFDeriv ℝ r g)) ∧
  (∀ j ≤ r, ∃ M : ℝ, ∀ x, ‖iteratedFDeriv ℝ j g x‖ ≤ M)

Uses 1 · Used by 1

Statement usesEuclidean space \(\mathbb{R}^n\)

Used bySobolev embedding theorem (Morrey regime)

TheoremSobolev embedding theorem (Morrey regime)#●ready to prove

Let \(n, k, r\) be natural numbers and \(\alpha, p\) real numbers with \(n < p\), \(0 < \alpha \le 1\) and \(r + \alpha < k - n/p\). Then every function \(f : \mathbb{R}^n \to \mathbb{R}\) in the Sobolev space \(W^{k,p}(\mathbb{R}^n)\) is equal almost everywhere, for Lebesgue measure, to some function \(g\) in the Hölder space \(C^{r,\alpha}(\mathbb{R}^n)\).

public theorem_wanted sobolev_embedding {n k r : ℕ} {α p : ℝ}
    (_hp : (n : ℝ) < p) (_hα : 0 < α) (_hα1 : α ≤ 1)
    (_hgap : (r : ℝ) + α < (k : ℝ) - n / p)
    (f : E n → ℝ) (_hf : MemSobolevWk k (ENNReal.ofReal p) f) :
    ∃ g : E n → ℝ, f =ᵐ[volume] g ∧ MemHolder r α g

Sources

• C.B. Morrey, 'Functions of several variables and absolute continuity, II', Duke Math. J. 6 (1940) 187–215; full Sobolev-embedding development in Multiple Integrals in the Calculus of Variations, Springer 1966. Listed as §111 in O. Knill, Some Fundamental Theorems in Mathematics (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf). Problem sobolev_embedding_morrey of the lean-eval benchmark.

Uses 3

Statement usesEuclidean space \(\mathbb{R}^n\) · Hölder space \(C^{r,\alpha}(\mathbb{R}^n)\) · Sobolev space \(W^{k,p}(\mathbb{R}^n)\)

7 fully proved2 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.