Ground-state energy of dilute Bose gases

DefinitionThe box \(((0,L)^3)^N\)#✓fully proved

For a natural number \(N\) and a real number \(L\), the box \(([0,L]^3)^N\) is the set of configurations \((x_1, \dots, x_N)\) of \(N\) points of \(\mathbb{R}^3\) such that every coordinate of every point \(x_i\) lies in the closed interval \([0, L]\).

def box (N : ℕ) (L : ℝ) : Set (Fin N → ℝ³) := {x | ∀ i k, x i k ∈ Set.Icc 0 L}

Used by 2

Used bySmooth functions supported inside the box · Lee–Huang–Yang lower bound for dilute Bose gases

StructureSmooth functions supported inside the box#✓fully proved

For a natural number \(N\) and a real number \(L\), \(C_0^\infty(([0,L]^3)^N) \setminus \{0\}\) consists of the functions \(\Psi : (\mathbb{R}^3)^N \to \mathbb{R}\) that are smooth on the box \(([0,L]^3)^N\), whose closed support is contained in the interior of the box, and that are not identically zero.

The functions are defined on all of \((\mathbb{R}^3)^N\) rather than on the box only.

structure CInfty0Box (N : ℕ) (L : ℝ) where
  /-- The underlying function `(ℝ³)ᴺ → ℝ`. Note that unlike the paper the domain of the
  function is `(ℝ³)ᴺ` rather than `[0,L]³ᴺ` since this makes it easier to state differentiability
  in Lean. -/
  toFun : (Fin N → ℝ³) → ℝ
  /-- If `Ψ : C₀^∞(([0,L]³)ᴺ)\{0}` then `Ψ` is smooth on `([0,L]³)ᴺ`. -/
  contDiff : ContDiffOn ℝ ∞ toFun (box N L)
  /-- If `Ψ : C₀^∞(([0,L]³)ᴺ)\{0}` then the support of `Ψ` is contained in the interior
  of `([0,L]³)ᴺ`. -/
  support : tsupport toFun ⊆ interior (box N L)
  /-- If `Ψ : C₀^∞(([0,L]³)ᴺ)\{0}` then `Ψ ≠ 0`. -/
  nezero : toFun ≠ 0

Uses 1 · Used by 1

Statement usesThe box \(((0,L)^3)^N\)

Used byLee–Huang–Yang lower bound for dilute Bose gases

DefinitionRadial functions#✓fully proved

A function \(v : \mathbb{R}^3 \to \mathbb{R}\) is radial if \(v(x) = v(y)\) for all \(x, y \in \mathbb{R}^3\) with \(\|x\| = \|y\|\).

def IsRadial (v : ℝ³ → ℝ) : Prop := ∀ x y, ‖x‖ = ‖y‖ → v x = v y

Used by 2

Used byScattering length · Lee–Huang–Yang lower bound for dilute Bose gases

StructureScattering solutions#✓fully proved

Let \(v, w : \mathbb{R}^3 \to \mathbb{R}\). The function \(w\) is a scattering solution for the potential \(v\) if \(w\) and \(v\,(1 - w)\) are locally integrable, \(w(x) \to 0\) as \(\|x\| \to \infty\), and \(w\) solves the scattering equation \(-\Delta w = \frac{1}{2} v\,(1 - w)\) (Equation (3.4) of Fournais–Solovej) in the weak sense: for every smooth, compactly supported \(\varphi : \mathbb{R}^3 \to \mathbb{R}\),

\[-\int_{\mathbb{R}^3} w\,\Delta\varphi = \frac{1}{2} \int_{\mathbb{R}^3} v\,(1 - w)\,\varphi.\]

structure IsScatteringSolution (w v : ℝ³ → ℝ) where
  lhs_integrable : LocallyIntegrable w
  rhs_integrable : LocallyIntegrable (v * (1 - w))
  eq : ∀ φ, ContDiff ℝ ∞ φ ∧ HasCompactSupport φ →
    - ∫ x, w x * (Δ φ) x = (1 / 2) * ∫ x, v x * (1 - w x) * φ x
  lim : Tendsto w (cocompact ℝ³) (𝓝 0)

Used by 1

Used byScattering length

DefinitionScattering length#✓fully proved

Let \(v : \mathbb{R}^3 \to \mathbb{R}\) be a potential. If there is a radial scattering solution \(w\) to the scattering equation with potential \(v\), the scattering length of \(v\) is \(a(v) = (8\pi)^{-1} \int_{\mathbb{R}^3} v(x)\,(1 - w(x))\,dx\), where \(w\) is one such solution, chosen arbitrarily; if there is no radial scattering solution, \(a(v) = 0\).

This is Equation (3.5) of Fournais–Solovej. Under the assumptions of Theorem 1.2 the radial scattering solution exists and is unique, so the choice does not matter there.

noncomputable def a (v : ℝ³ → ℝ) : ℝ :=
  if w : ∃ w, IsRadial w ∧ IsScatteringSolution w v then
    (8 * π)⁻¹ * ∫ x, (v x * (1 - w.choose x))
  else
    0

Uses 2 · Used by 2

Statement usesRadial functions · Scattering solutions

Used byLee–Huang–Yang lower bound for dilute Bose gases · The ratio \(\mathcal{R}(v)\)

DefinitionThe ratio \(\mathcal{R}(v)\)#✓fully proved

For a potential \(v : \mathbb{R}^3 \to \mathbb{R}\) with scattering length \(a(v)\), let \(\mathcal{R}(v) = \int_{\mathbb{R}^3} v(x)/(8\pi a(v))\,dx\). When \(a(v) \neq 0\) this is the ratio of \((8\pi)^{-1} \int v\) to \(a(v)\).

noncomputable def 𝓡 (v : ℝ³ → ℝ) := ∫ x, v x / (8 * π * a v)

Uses 1 · Used by 1

Statement usesScattering length

Used byLee–Huang–Yang lower bound for dilute Bose gases

DefinitionLee–Huang–Yang error exponent#●ready to state

\(\eta\) is a real constant, not given explicitly, that serves as the exponent in the error term \((\rho a^3)^{1/2 + \eta}\) of the Lee–Huang–Yang lower bound (Theorem 1.2), where \(\rho\) is the density and \(a\) the scattering length of the potential; that theorem asserts \(\eta > 0\).

public def_wanted η : ℝ

Sources

• S. Fournais and J. P. Solovej, The energy of dilute Bose gases, Annals of Math, 192 (3) 2020. Statement taken from https://github.com/ImperialCollegeLondon/AnnalsChallenge. Problem annals_bose_gases of the lean-eval benchmark.

Used by 1

Used byLee–Huang–Yang lower bound for dilute Bose gases

DefinitionLee–Huang–Yang error constant#●ready to state

\(\mathcal{C}\) is a real-valued function of two real variables, not given explicitly. Let \(v\) be a potential with scattering length \(a\) whose closed support lies in the open ball \(B(0, R)\), and let \(\mathcal{R}(v) = \int v/(8\pi a)\). In the Lee–Huang–Yang lower bound (Theorem 1.2) for \(v\) at density \(\rho\), the error term is \(\mathcal{C}(\mathcal{R}(v), R/a)\,(\rho a^3)^{1/2 + \eta}\), where \(\eta\) is the Lee–Huang–Yang error exponent, so its constant depends only on \(\mathcal{R}(v)\) and \(R/a\).

public def_wanted 𝓒 (𝓡 : ℝ) (r : ℝ) : ℝ

Sources

• S. Fournais and J. P. Solovej, The energy of dilute Bose gases, Annals of Math, 192 (3) 2020. Statement taken from https://github.com/ImperialCollegeLondon/AnnalsChallenge. Problem annals_bose_gases of the lean-eval benchmark.

Used by 1

Used byLee–Huang–Yang lower bound for dilute Bose gases

TheoremLee–Huang–Yang lower bound for dilute Bose gases#●statement formalized

There are a real number \(\eta\) and a function \(\mathcal{C}\) of two real variables such that the following holds. Let \(v : \mathbb{R}^3 \to \mathbb{R}\) be a non-negative, radial, integrable potential that is not almost everywhere zero, and let \(R > 0\) be such that the closed support of \(v\) lies in the open ball \(B(0, R)\). Let \(a\) be the scattering length of \(v\), let \(\mathcal{R}(v) = \int v/(8\pi a)\), and let \(e(\rho, v)\) be the ground state energy density at density \(\rho\): the limit, as \(L \to \infty\) and \(N/L^3 \to \rho\), of \(L^{-3}\) times the infimum, over \(\Psi \in C_0^\infty(([0,L]^3)^N) \setminus \{0\}\), of \(\langle \Psi, H_N \Psi \rangle / \|\Psi\|^2\), where the inner product and norm are those of \(L^2(([0,L]^3)^N)\) and, writing points of \((\mathbb{R}^3)^N\) as \((x_1, \dots, x_N)\) and \(\Delta_{x_i}\) for the Laplacian in the variable \(x_i\), \(H_N = \sum_{i=1}^{N} -\Delta_{x_i} + \sum_{1 \le i < j \le N} v(x_i - x_j)\). Then \(\eta > 0\), and for all sufficiently small \(\rho > 0\),

\[ e(\rho, v) \ge 4\pi\rho^2 a \left(1 + \frac{128}{15\sqrt{\pi}}\sqrt{\rho a^3} - \mathcal{C}(\mathcal{R}(v), R/a)\,(\rho a^3)^{1/2 + \eta}\right). \]

The source takes the limit \(\rho a^3 \to 0^+\); for fixed \(v\) this is the same as \(\rho \to 0^+\). Although the wording of Theorem 1.2 in the source suggests that \(\eta\) may depend on \(\mathcal{R}(v)\) and \(R/a\), Theorem 6.8 there shows that \(\eta\) is a universal constant.

public theorem_wanted theorem_1_2 (v : ℝ³ → ℝ) (hv_ne_zero : ¬ v =ᵐ[volume] 0) (hv_nonneg : 0 ≤ v)
    (hv_radial : IsRadial v) (hv_memL1 : MemLp v 1) {R : ℝ} (hR : 0 < R)
    (hv_supp : tsupport v ⊆ ball 0 R) : 0 < ❰η❱ ∧ ∀ᶠ ρ in 𝓝[>] 0,
      e ρ v ≥ 4 * π * ρ ^ 2 * a v * (1 + (128 / (15 * √ π)) * √ (ρ * a v ^ 3) -
        ❰𝓒❱ (𝓡 v) (R / a v) * (ρ * a v ^ 3) ^ (1 / 2 + ❰η❱))

Sources

• S. Fournais and J. P. Solovej, The energy of dilute Bose gases, Annals of Math, 192 (3) 2020. Statement taken from https://github.com/ImperialCollegeLondon/AnnalsChallenge. Problem annals_bose_gases of the lean-eval benchmark.

Uses 7

Statement usesSmooth functions supported inside the box · Radial functions · Scattering length · The box \(((0,L)^3)^N\) · Lee–Huang–Yang error exponent · Lee–Huang–Yang error constant · The ratio \(\mathcal{R}(v)\)

6 fully proved1 statement formalized2 ready to state

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.