Eqs. (4.15) → (4.17): squeezed limit of
ProvedMaldacena2003.threeGraviton_squeezed_limitcosmologyinflationmathematical-physics
Let be a unit vector and , with . Let be real symmetric traceless matrices with , and . These are the polarizations of the soft graviton and of the two hard gravitons, the latter in the limiting configuration . Let be real. Put and . Then, with the correlator (4.15),
For equal hard polarizations, , and the right-hand side is the coefficient in (4.17). The statement is the agreement of (4.15) with (4.17) in the overlapping region.
Formalization Note , and the horizon-crossing times , are identified at leading order. The polarizations are held fixed along the limit, and the hard polarizations are taken transverse to , the limiting direction of .
Preamble
import Mathlib import Definitions.Def_Maldacena2003_InflationDefs open Filter Topology
Formal statement
namespace Maldacena2003
theorem threeGraviton_squeezed_limit (ρd : ℝ) (n k₂ : EuclideanSpace ℝ (Fin 3))
(hn : ‖n‖ = 1) (hk₂ : k₂ ≠ 0) (ε₁ ε₂ ε₃ : Matrix (Fin 3) (Fin 3) ℝ)
(hε₁symm : ∀ i j, ε₁ i j = ε₁ j i) (hε₁tr : Matrix.trace ε₁ = 0)
(hε₁tv : ∀ i, ∑ j, ε₁ i j * n j = 0)
(hε₂symm : ∀ i j, ε₂ i j = ε₂ j i) (hε₂tr : Matrix.trace ε₂ = 0)
(hε₂tv : ∀ i, ∑ j, ε₂ i j * k₂ j = 0)
(hε₃symm : ∀ i j, ε₃ i j = ε₃ j i) (hε₃tr : Matrix.trace ε₃ = 0)
(hε₃tv : ∀ i, ∑ j, ε₃ i j * k₂ j = 0) :
Tendsto
(fun t : ℝ => 2 * t ^ 3 * threeGravitonBispectrum ρd ε₁ ε₂ ε₃ (t • n) k₂ (-(t • n) - k₂))
(𝓝[>] 0)
(𝓝 ((∑ i, ∑ j, ε₂ i j * ε₃ i j) * ρd ^ 2 * (1 / (2 * ‖k₂‖ ^ 5)) * (2 * ρd ^ 2) * (3 / 2)
* ∑ i, ∑ j, ε₁ i j * k₂ i * k₂ j)) := by sorry
end Maldacena2003Source
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), pp. 19–20, eqs. (4.15)–(4.17)
Human review
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.