Lemma 10.1 — H²(ℝⁿ) ⊆ C_∞(ℝⁿ) with ‖ψ‖_∞ ≤ a‖H₀ψ‖ + b‖ψ‖ for n ≤ 3

Proved

TeschlQM.OneParticle.sup_norm_bound

by mikedeng1 · Sep 29, 2026 · Mathlib 0df444a (Lean v4.33.1)

functional-analysisp2o-batch-books5p2o-gran-per-chapterp2o-plan-bookp2o-v1schrodinger-operatorssobolev-spaces

Let $n \le 3$ and let $H_0 = -\Delta$ with domain $H^2(\mathbb R^n)$ . Every $\psi \in H^2(\mathbb R^n)$ lies in $C_\infty(\mathbb R^n)$ , i.e. it has a continuous representative vanishing at infinity. Moreover, for any $a > 0$ there is a $b > 0$ such that for all $\psi \in H^2(\mathbb R^n)$

\|\psi\|_\infty \le a \|H_0 \psi\| + b \|\psi\|,

where $\|\psi\|_\infty$ is the supremum of the continuous representative.

This says that multiplication by a bounded function, and by an $L^2$ function in low dimension, is $H_0$ -bounded with bound $0$ ; it is the first step of Theorem 10.2.

Formalization Note. $C_\infty(\mathbb R^n)$ is Mathlib's ℝⁿ →C₀ ℂ with its sup norm; the bound is asserted for every such representative of $\psi$ (the continuous representative is unique). The constant $b$ depends only on $a$ and $n$ , not on $\psi$ , as in the book's proof.

Preamble

import Mathlib
import Definitions.Def_TeschlQM_OneParticle_freeHamiltonian

Formal statement

namespace TeschlQM.OneParticle

open MeasureTheory
open scoped ZeroAtInfty

/-- Teschl, Lemma 10.1, p. 221. Suppose `n ≤ 3` and `ψ ∈ H²(ℝⁿ)`. Then `ψ ∈ C_∞(ℝⁿ)` (it has a
continuous representative vanishing at infinity, an element of `ℝⁿ →C₀ ℂ`), and for any `a > 0`
there is a `b > 0` such that `‖ψ‖_∞ ≤ a‖H₀ψ‖ + b‖ψ‖` (10.2), where `‖ψ‖_∞` is the sup norm of that
continuous representative. The constant `b` depends only on `a` (and `n`), not on `ψ`, as in the
book's proof. -/
theorem sup_norm_bound (n : ℕ) (hn : n ≤ 3) :
    (∀ ψ ∈ sobolevH2 n, ∃ f : EuclideanSpace ℝ (Fin n) →C₀ ℂ,
        (ψ : EuclideanSpace ℝ (Fin n) → ℂ) =ᵐ[volume] f) ∧
      ∀ a : ℝ, 0 < a → ∃ b : ℝ, 0 < b ∧
        ∀ (ψ : (freeHamiltonian n).domain) (f : EuclideanSpace ℝ (Fin n) →C₀ ℂ),
          ((ψ : L2 n) : EuclideanSpace ℝ (Fin n) → ℂ) =ᵐ[volume] f →
            ‖f‖ ≤ a * ‖freeHamiltonian n ψ‖ + b * ‖(ψ : L2 n)‖ := by sorry

end TeschlQM.OneParticle

Source

Teschl, Mathematical Methods in Quantum Mechanics, AMS GSM 99, 2009, p. 221, Lemma 10.1

Read-back

What the Lean code literally says, in plain math · claude-opus-5-5

Setting.

$n\in\mathbb{N}$ with $n\le 3$ , so $n=0$ is included.
$L^2(\mathbb{R}^n)$ is the space of square-integrable complex functions on Euclidean $\mathbb{R}^n$ with Lebesgue measure, modulo equality almost everywhere.
$\mathcal{F}$ is Mathlib's unitary $L^2$ Fourier transform, the extension of $\hat\psi(\xi)=\int e^{-2\pi i\langle x,\xi\rangle}\psi(x)\,dx$ .
$H^2(\mathbb{R}^n)=\{\psi\in L^2:\ (2\pi\|\xi\|)^2\hat\psi(\xi)\in L^2\}$ .
$H_0$ is the operator with domain $H^2(\mathbb{R}^n)$ and $H_0\psi=\mathcal{F}^{-1}[(2\pi\|\xi\|)^2\hat\psi]$ .
$C_0(\mathbb{R}^n)$ is the space of continuous functions $\mathbb{R}^n\to\mathbb{C}$ that tend to $0$ along the cocompact filter. It carries the sup norm $\|f\|_\infty=\sup_x|f(x)|$ .

Claim. The statement asserts both of the following.

Continuous representative. For every $\psi\in H^2(\mathbb{R}^n)$ there is some $f\in C_0(\mathbb{R}^n)$ with $\psi=f$ almost everywhere.
Uniform bound. For every real $a>0$ there is a real $b>0$ , depending only on $a$ (and $n$ ), such that

\|f\|_\infty\;\le\;a\,\|H_0\psi\|_{L^2}+b\,\|\psi\|_{L^2}

for every $\psi\in H^2(\mathbb{R}^n)$ and every $f\in C_0(\mathbb{R}^n)$ that equals $\psi$ almost everywhere. The same $b$ serves for all $\psi$ and all such $f$ .

Part 2 by itself constrains only those $\psi$ that have such an $f$ . Part 1 asserts that every $\psi$ does.

Degenerate case: $n=0$ . $\mathbb{R}^0$ is one compact point with unit point mass, so the following reductions apply:

$L^2\cong\mathbb{C}$ , and $H^2$ is everything.
$H_0=0$ .
Every function on the point lies in $C_0$ , and $\|f\|_\infty=|f(0)|$ .

Part 1 is then trivially true. Part 2 says: for each $a>0$ there is $b>0$ with $|c|\le b|c|$ for all $c\in\mathbb{C}$ .

Human review

Endorsed by Shuze Chen · Oct 2, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Oct 2, 2026
Confirmed by the mission captain (proposal self-audit).

View graph