Prove2Me

Eq. (5): χnl\chi_{nl} is a normalizable mode at frequency ωnl\omega_{nl}

Proved
Giddings1999.modeRadial_isNormalizableMode

by Lucas · Oct 13, 2026 · Mathlib 0df444a (Lean v4.33.1)

ads-cftmathematical-physics

Let d≥2d\ge2, R>0R>0, m∈Rm\in\mathbb R and n,l∈Nn,l\in\mathbb N. The profile χnl\chi_{nl} is a normalizable mode with angular momentum ll and frequency ωnl=2h++2n+l\omega_{nl}=2h_++2n+l: it solves the radial equation, is not identically zero on (0,π/2)(0,\pi/2), is bounded near r=0r=0, and satisfies

∫0π/2tan⁡d−1r  χnl(r)2 dr<∞.\int_0^{\pi/2}\tan^{d-1}r\;\chi_{nl}(r)^2\,dr<\infty .

This is the "if" direction of the goal theorem.

Preamble
import Mathlib
import Definitions.Def_Giddings1999_AdSModes

open Real Filter Topology
Formal statement
namespace Giddings1999

/-- **Milestone, eq. (5)**: each `χ_{nl}` is a normalizable mode at frequency `ω_{nl}`. -/
theorem modeRadial_isNormalizableMode (d : ℕ) (hd : 2 ≤ d) (m R : ℝ) (hR : 0 < R) (n l : ℕ) :
    IsNormalizableMode d m R (omegaNL d m R n l) l (modeRadial d m R n l) := by
  sorry

end Giddings1999
Source
S. B. Giddings, Boundary S matrix and the anti-de Sitter space to conformal field theory dictionary, Phys. Rev. Lett. 83, 2707 (1999), https://doi.org/10.1103/PhysRevLett.83.2707, eq. (5), p. 2707
Human review

  • Endorsed by Shuze Chen · Oct 13, 2026

    Confirmed by the moderator at approval.

  • Endorsed by Lucas · Oct 13, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph