Eq. (6): $\chi_{nl}(r)\sim k_{nl}(\cos r)^{2h_+}$ as $r\to\pi/2$ , with $k_{nl}\ne0$

Proved

Giddings1999.modeRadial_boundary_asymptotics

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

ads-cftmathematical-physics

Let $d\ge2$ , $R>0$ , $m\in\mathbb R$ and $n,l\in\mathbb N$ . There is a constant $k_{nl}\neq0$ such that

\lim_{r\to\pi/2^-}\frac{\chi_{nl}(r)}{(\cos r)^{2h_+}}=k_{nl}.

The constants $k_{nl}$ reappear in the free-field expansion (27) and in the matrix elements (28)–(29).

Preamble

import Mathlib
import Definitions.Def_Giddings1999_AdSModes

open Real Filter Topology

Formal statement

namespace Giddings1999

/-- **Milestone, eq. (6)**: `χ_{nl}(r) → k_{nl} (cos r)^{2h₊}` as `r → π/2`, with `k_{nl} ≠ 0`. -/
theorem modeRadial_boundary_asymptotics (d : ℕ) (hd : 2 ≤ d) (m R : ℝ) (hR : 0 < R) (n l : ℕ) :
    ∃ k : ℝ, k ≠ 0 ∧
      Tendsto (fun r => modeRadial d m R n l r / cos r ^ twoHPlus d m R) (𝓝[<] (π / 2)) (𝓝 k) := 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. (6), 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

Eq. (6): χnl(r)∼knl(cos⁡r)2h+\chi_{nl}(r)\sim k_{nl}(\cos r)^{2h_+}χnl​(r)∼knl​(cosr)2h+​ as r→π/2r\to\pi/2r→π/2, with knl≠0k_{nl}\ne0knl​=0

Eq. (6): $\chi_{nl}(r)\sim k_{nl}(\cos r)^{2h_+}$ as $r\to\pi/2$ , with $k_{nl}\ne0$