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

Omega_0_pos

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)

  91theorem Omega_0_pos : 0 < Omega_0 := by

proof body

Term-mode proof.

  92  unfold Omega_0
  93  apply div_pos (mul_pos (by norm_num) Real.pi_pos)
  94  apply Real.log_pos
  95  rw [one_lt_div phi_pos]
  96  exact lt_of_lt_of_le (by linarith [phi_lt_two]) (le_of_lt Real.pi_gt_three)
  97
  98/-! ## UV Knee -/
  99
 100/-- The UV knee (comoving): k_rec,com ≈ 1.4 × 10⁶ Mpc⁻¹.
 101    Above this scale, the recognition lattice structure becomes visible
 102    and the primordial spectrum softens. -/

used by (1)

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

depends on (8)

Lean names referenced from this declaration's body.