`bao_correlation_peak`

definition

show as: view math explainer →

module: IndisputableMonolith.Physics.BAO
domain: Physics
line: 139 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Physics.BAO on GitHub at line 139.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

used by

bao_peak_approximately_150 IndisputableMonolith.Physics.BAO

formal source

 136  ring
 137
 138/-- The correlation function peak in real space: r = 2π/k₁ ≈ 150 h⁻¹ Mpc. -/
 139noncomputable def bao_correlation_peak (r_s : ℝ) : ℝ := 2 * r_s
 140
 141theorem bao_peak_approximately_150 :
 142    |bao_correlation_peak sound_horizon_approx - 294| < 1 := by
 143  norm_num [bao_correlation_peak, sound_horizon_approx]
 144
 145end BAO
 146end Physics
 147end IndisputableMonolith

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.