module module

`IndisputableMonolith.Physics.BAO`

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

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Cost.JcostCore module_import

declarations in this module (21)

def baryon_loading L30
theorem baryon_loading_decreasing L33
def sound_speed L41
theorem sound_speed_positive L44
theorem sound_speed_radiation_limit L52
theorem sound_speed_decreasing L58
def rs_omega_b_h2 L70
def rs_omega_m_h2 L73
theorem matter_exceeds_baryons L76
def rs_spectral_index L81
theorem spectral_index_60efolds L84
theorem spectral_index_red_tilt L90
def rs_drag_redshift L99
abbrev sound_horizon_approx L106
theorem sound_horizon_positive L109
theorem rs_sound_horizon_consistent L114
def bao_peak_wavenumber L121
theorem first_peak_wavenumber L125
theorem bao_peaks_evenly_spaced L132
def bao_correlation_peak L139
theorem bao_peak_approximately_150 L141