pith. machine review for the scientific record. sign in
def definition def or abbrev

running_observed

show as:
view Lean formalization →

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)

 202noncomputable def running_observed : ℝ := -0.006

proof body

Definition body.

 203
 204/-! ## Primordial Non-Gaussianity -/
 205
 206/-- Deviations from Gaussian statistics (f_NL):
 207
 208    Local f_NL = -2 ± 5 (Planck 2018)
 209
 210    RS prediction: f_NL may have φ-structure, but small.
 211    Single-field slow-roll gives f_NL ~ slow-roll parameters ~ 0.01. -/

depends on (1)

Lean names referenced from this declaration's body.