pith. machine review for the scientific record. sign in
theorem proved term proof

empiricalCentral_in_band

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)

  49theorem empiricalCentral_in_band :
  50    hubbleRatioLower < empiricalCentral ∧ empiricalCentral < hubbleRatioUpper := by

proof body

Term-mode proof.

  51  unfold hubbleRatioLower hubbleRatioUpper empiricalCentral
  52  refine ⟨?lo, ?hi⟩ <;> norm_num
  53
  54/-- A measurement is consistent with the RS prediction iff it sits in
  55the predicted band. -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (12)

Lean names referenced from this declaration's body.