Heisenberg uncertainty principle
TheoremIntegration-by-parts identity for Heisenberg's inequality#✓fully proved
The integration-by-parts identity underlying Heisenberg's inequality:
for real-valued Schwartz f, ∫ (f x)² = -2 * ∫ x * f x * f' x.
theorem schwartz_integral_sq_eq_neg_two_mul (f : 𝓢(ℝ, ℝ)) :
∫ x, (f x) ^ 2 = -2 * ∫ x, x * (f x * deriv f x)Used by 1
TheoremHeisenberg's uncertainty principle#✓fully proved
Heisenberg's uncertainty principle for real-valued Schwartz functions:
(∫ (f x)²)² ≤ 4 * (∫ x² * (f x)²) * (∫ (f' x)²).
theorem heisenberg_uncertainty_real (f : 𝓢(ℝ, ℝ)) :
(∫ x, (f x) ^ 2) ^ 2
≤ 4 * (∫ x, x ^ 2 * (f x) ^ 2) * (∫ x, (deriv f x) ^ 2)Uses 1 · Used by 1
TheoremHeisenberg's uncertainty principle#✓fully proved
Heisenberg's uncertainty principle for complex-valued Schwartz functions:
(∫ ‖f x‖²)² ≤ 4 * (∫ x² * ‖f x‖²) * (∫ ‖f' x‖²).
theorem heisenberg_uncertainty_complex (f : 𝓢(ℝ, ℂ)) :
(∫ x, ‖f x‖ ^ 2) ^ 2
≤ 4 * (∫ x, x ^ 2 * ‖f x‖ ^ 2) * (∫ x, ‖deriv f x‖ ^ 2)Uses 1 · Used by 2
TheoremHeisenberg's uncertainty principle#✓fully proved
Heisenberg's uncertainty principle in Fourier form: with Mathlib's
Fourier normalization, the Fourier second moment about zero is ∫ ξ² * ‖𝓕 f ξ‖², and
(∫ ‖f x‖²)² ≤ 16 * π² * (∫ x² * ‖f x‖²) * (∫ ξ² * ‖𝓕 f ξ‖²).
theorem heisenberg_uncertainty_fourier (f : 𝓢(ℝ, ℂ)) :
(∫ x, ‖f x‖ ^ 2) ^ 2 ≤ 16 * Real.pi ^ 2 * (∫ x, x ^ 2 * ‖f x‖ ^ 2)
* (∫ ξ, ξ ^ 2 * ‖FourierTransform.fourier f ξ‖ ^ 2)Uses 1 · Used by 1
TheoremHeisenberg's uncertainty principle#✓fully proved
Heisenberg's uncertainty principle about an arbitrary center a:
the position second moment is measured about a; the derivative factor is unchanged.
theorem heisenberg_uncertainty_shifted (f : 𝓢(ℝ, ℂ)) (a : ℝ) :
(∫ x, ‖f x‖ ^ 2) ^ 2
≤ 4 * (∫ x, (x - a) ^ 2 * ‖f x‖ ^ 2) * (∫ x, ‖deriv f x‖ ^ 2)Uses 1 · Used by 1
TheoremHeisenberg's uncertainty principle#✓fully proved
Heisenberg's uncertainty principle with the position factor centered: for
μ = (∫ y * ‖f y‖²) / (∫ ‖f x‖²), the position second moment about μ satisfies
the same bound. For positive L2 mass, μ is the mean position. Zero L2 mass occurs
only for f = 0, where μ = 0 / 0 = 0 by Lean's convention.
Only the position factor is centered.
theorem heisenberg_uncertainty_centered (f : 𝓢(ℝ, ℂ)) :
(∫ x, ‖f x‖ ^ 2) ^ 2 ≤ 4
* (∫ x, (x - (∫ y, y * ‖f y‖ ^ 2) / (∫ z, ‖f z‖ ^ 2)) ^ 2 * ‖f x‖ ^ 2)
* (∫ x, ‖deriv f x‖ ^ 2)Uses 1
TheoremHeisenberg uncertainty principle#✓fully proved
Denote by \(\mathcal{S}(\mathbb{R})\) the Schwartz space on \(\mathbb{R}\) consisting of all complex-valued \(C^\infty\) functions \(f(x)\) on \(\mathbb{R}\) such that [ \sup_{x\in\mathbb{R}} |x|^k \left|\frac{d^\ell f}{dx^\ell}(x)\right| < \infty \quad\text{for all } k,\ell\in\mathbb{N}\cup{0}. ] Suppose \(\psi(x)\in\mathcal{S}(\mathbb{R})\) satisfies [ \int_{-\infty}^{\infty}|\psi(x)|^2\,dx=1. ] Denote by \(\hat{\psi}(\xi)\) the Fourier transform of \(\psi(x)\) defined by [ \hat{\psi}(\xi)=\int_{-\infty}^{\infty}\psi(x)e^{-2\pi i x\xi}\,dx. ] The normalized Fourier Heisenberg corollary then gives [ \left(\int_{-\infty}^{\infty} x^2|\psi(x)|^2\,dx\right) \left(\int_{-\infty}^{\infty} \xi^2|\hat{\psi}(\xi)|^2\,d\xi\right) \ge \frac{1}{16\pi^2}. ]
Lean variant: the Fourier transform is Mathlib's 𝓕, which has the source's normalization ∫ ψ(x)
e^{-2πixξ} dx, instead of the source's helper definition.
public theorem integral_sq_mul_norm_sq_mul_integral_sq_mul_norm_fourier_sq_ge
(ψ : SchwartzMap ℝ ℂ)
(hL2 : (∫ x : ℝ, ‖ψ x‖ ^ 2) = 1) :
( (∫ x : ℝ, (x ^ 2) * (‖ψ x‖ ^ 2)) *
(∫ ξ : ℝ, (ξ ^ 2) * (‖𝓕 (⇑ψ) ξ‖ ^ 2)) )
≥ 1 / (16 * Real.pi ^ 2)Sources
- MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level II (Functional analysis; Distributions, generalized functions, distribution spaces), problem
ma_proofbench_l2_57, with the change above.
Uses 1
TheoremHeisenberg uncertainty inequality with shifted moments#●ready to prove
For a complex-valued Schwartz function \(f\) on \(\mathbb{R}\), write \(\hat{f}(\xi) = \int_{\mathbb{R}} f(x) e^{-2\pi i x \xi}\, dx\) for its Fourier transform. There is a constant \(C > 0\) such that for all real numbers \(c\) and \(d\) and every complex-valued Schwartz function \(f\) on \(\mathbb{R}\),
public theorem_wanted exists_const_sq_integral_sq_le_mul_shifted_moments_fourier :
∃ C : ℝ, 0 < C ∧
∀ c d : ℝ, ∀ f : SchwartzMap ℝ ℂ,
(∫ x : ℝ, ‖f x‖ ^ 2) ^ 2 ≤
C * (∫ x : ℝ, (x - c) ^ 2 * ‖f x‖ ^ 2) *
(∫ ξ : ℝ, (ξ - d) ^ 2 * ‖(𝓕 f) ξ‖ ^ 2)Sources
- MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level II (Functional analysis; Distributions, generalized functions, distribution spaces), problem
ma_proofbench_l2_46.
TheoremWeighted \(L^2\) inequality for real Schwartz functions#●ready to prove
For every real-valued Schwartz function \(f : \mathbb{R} \to \mathbb{R}\),
that is, \(\|f\|_{L^2}^2 \le 2 \, \|x f\|_{L^2} \, \|f'\|_{L^2}\).
public theorem_wanted integral_sq_le_two_mul_sqrt_integral_mul_sq_mul_sqrt_integral_deriv_sq
(f : SchwartzMap ℝ ℝ) :
(∫ x : ℝ, ‖f x‖ ^ 2) ≤
2 * Real.sqrt (∫ x : ℝ, ‖x * f x‖ ^ 2) *
Real.sqrt (∫ x : ℝ, ‖deriv (fun y : ℝ => f y) x‖ ^ 2)Sources
- MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level II (Real functions; Inequalities in real analysis), problem
ma_proofbench_l2_40.
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.