No prose has been written for this declaration yet. The Lean source and graph data below render
without it.
generate prose now
formal statement (Lean)
130noncomputable def powerSpectrum (φ : ℝ) (hφ : φ > 0) : ℝ :=
proof body
Definition body.
131 let V := inflatonPotential φ hφ
132 let Vp := (1 - 1/φ^2) / 2
133 if Vp ≠ 0 then V^3 / Vp^2 else 0
134
135/-- The scalar spectral index n_s.
136 n_s = 1 - 6ε + 2η ≈ 0.96 for slow-roll inflation. -/
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.
-
FourierOperation
in IndisputableMonolith.Mathematics.FourierAnalysisFromRS
decl_use
depends on (5)
Lean names referenced from this declaration's body.
-
inflatonPotential
in IndisputableMonolith.Cosmology.Inflation
decl_use
-
V
in IndisputableMonolith.Cosmology.InflatonPotentialFromJCost
decl_use
-
V
in IndisputableMonolith.Foundation.SpectralEmergence
decl_use
-
for
in IndisputableMonolith.Foundation.UniversalForcingSelfReference
decl_use
-
V
in IndisputableMonolith.RRF.Core.Glossary
decl_use