Prove2Me

Eq. (4.11): Re[−∫−∞0idηη2∏j(1−ikjη)eiktη]=−kt+∑i>jkikjkt+k1k2k3kt2\mathrm{Re}\big[-\int_{-\infty}^0 i\frac{d\eta}{\eta^2}\prod_j(1-ik_j\eta)e^{ik_t\eta}\big] = -k_t+\frac{\sum_{i>j}k_ik_j}{k_t}+\frac{k_1k_2k_3}{k_t^2}

Proved
Maldacena2003.graviton_vertex_integral_I

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

cosmologyinflationmathematical-physics

Let k1,k2,k3>0k_1,k_2,k_3>0 and kt=k1+k2+k3k_t = k_1+k_2+k_3. For a cutoff η0<0\eta_0<0 and ϵ>0\epsilon>0, consider

Jϵ(η0)=Re[− i∫−∞η0(1−ik1η)(1−ik2η)(1−ik3η)η2 eiktη eϵη dη].J_\epsilon(\eta_0) = \mathrm{Re}\Big[-\,i\int_{-\infty}^{\eta_0}\frac{(1-ik_1\eta)(1-ik_2\eta)(1-ik_3\eta)}{\eta^2}\,e^{ik_t\eta}\,e^{\epsilon\eta}\,d\eta\Big].

Then there is a function JJ such that Jϵ(η0)→J(η0)J_\epsilon(\eta_0)\to J(\eta_0) as ϵ→0+\epsilon\to0^+ for every η0<0\eta_0<0, and

lim⁡η0→0−J(η0)=−kt+k1k2+k1k3+k2k3kt+k1k2k3kt2=I.\lim_{\eta_0\to0^-}J(\eta_0) = -k_t + \frac{k_1k_2+k_1k_3+k_2k_3}{k_t} + \frac{k_1k_2k_3}{k_t^2} = I .

This is the integral II of eq. (4.11). It controls the graviton–scalar–scalar correlator (4.10) and the three-graviton correlator (4.15). The integral diverges at η→0\eta\to0, but the divergence is purely imaginary, so the real part has a finite limit.

Formalization Note The iϵi\epsilon prescription is the damping factor eϵηe^{\epsilon\eta} with ϵ→0+\epsilon\to0^+. The upper endpoint 00 is reached as the limit η0→0−\eta_0\to0^- of the real part.

Preamble
import Mathlib
import Definitions.Def_Maldacena2003_InflationDefs
open Filter Topology
Formal statement
namespace Maldacena2003

theorem graviton_vertex_integral_I (k₁ k₂ k₃ : ℝ) (h₁ : 0 < k₁) (h₂ : 0 < k₂) (h₃ : 0 < k₃) :
    ∃ J : ℝ → ℝ,
      (∀ η₀ : ℝ, η₀ < 0 →
        Tendsto
          (fun ε : ℝ => (-(Complex.I * ∫ η in Set.Iic η₀,
            (1 - Complex.I * (k₁ : ℂ) * (η : ℂ)) * (1 - Complex.I * (k₂ : ℂ) * (η : ℂ))
              * (1 - Complex.I * (k₃ : ℂ) * (η : ℂ))
              * Complex.exp (Complex.I * ((k₁ + k₂ + k₃ : ℝ) : ℂ) * (η : ℂ)) / (η : ℂ) ^ 2
              * (Real.exp (ε * η) : ℂ))).re)
          (𝓝[>] 0) (𝓝 (J η₀))) ∧
      Tendsto J (𝓝[<] 0)
        (𝓝 (-(k₁ + k₂ + k₃) + (k₂ * k₁ + k₃ * k₁ + k₃ * k₂) / (k₁ + k₂ + k₃)
          + k₁ * k₂ * k₃ / (k₁ + k₂ + k₃) ^ 2)) := by sorry

end Maldacena2003
Source
J. Maldacena, Non-Gaussian features of primordial fluctuations in single field inflationary models, JHEP 05 (2003) 013, https://doi.org/10.1088/1126-6708/2003/05/013 (arXiv:astro-ph/0210603), p. 18, eq. (4.11) and footnote 17
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