IndisputableMonolith.Verification.Preregistered.Hubble.Measurement_2022

   1import Mathlib
   2import IndisputableMonolith.Verification.Preregistered.Core
   3
   4/-!
   5# Measurements: Hubble tension (representative values) and Ω_Λ (Planck)
   6
   7Pure data module. Update here when new releases arrive.
   8-/
   9
  10namespace IndisputableMonolith
  11namespace Verification
  12namespace Preregistered
  13namespace Hubble
  14
  15def H_early : ℝ := 67.4
  16def H_late : ℝ := 73.04
  17
  18def omega_lambda_measurement : Measurement :=
  19  { name := "Omega_L_Planck"
  20  , central := 0.6847
  21  , sigma := 0.0073 }
  22
  23end Hubble
  24end Preregistered
  25end Verification
  26end IndisputableMonolith
  27