omega_lambda_positive

proof body

Tactic-mode proof.

 118  have h_alphaInv_pos : alphaInv > 0 := by unfold alphaInv alpha_seed; positivity
 119  have h_alpha_pos : alpha > 0 := by unfold alpha; positivity
 120  -- alpha < 1/2 since alphaInv > 2
 121  have h_alpha_lt_half : alpha < 1/2 := by
 122    have h_eq : alpha = 1/alphaInv := by unfold alpha; field_simp
 123    rw [h_eq]
 124    rw [div_lt_div_iff₀ h_alphaInv_pos (by norm_num : (0:ℝ) < 2)]
 125    linarith [alphaInv_gt_2]
 126  -- alpha/pi < alpha (since pi > 1)
 127  have h_pi_gt_1 : Real.pi > 1 := by linarith [Real.pi_gt_three]
 128  have h_ratio : alpha / Real.pi < alpha := div_lt_self h_alpha_pos h_pi_gt_1
 129  linarith
 130
 131/-- **BOUNDS**: 0 < Ω_Λ < 11/16 -/