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

alphaG_pred_lower

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)

 149theorem alphaG_pred_lower : (4.5e9 : ℝ) < row_alphaG_pred := by

proof body

Tactic-mode proof.

 150  have hφ : (1.618 : ℝ) < phi := by
 151    simpa [show phi = (Real.goldenRatio : ℝ) from rfl] using phi_gt_1618
 152  have hpiUB : (Real.pi : ℝ) < 3.142 := by
 153    linarith [Real.pi_lt_d6, Real.pi_pos]
 154  have hN :
 155      (2 : ℝ) ^ (-(44 : ℤ)) * (1.618 : ℝ) ^ (112 : ℝ) < (2 : ℝ) ^ (-(44 : ℤ)) * phi ^ (112 : ℝ) := by
 156    have hr112 : (1.618 : ℝ) ^ (112 : ℝ) < phi ^ (112 : ℝ) := by
 157      exact Real.rpow_lt_rpow (by norm_num) hφ (by nlinarith)
 158    nlinarith [hr112, zpow_pos (by norm_num : (0 : ℝ) < (2 : ℝ))]
 159  have h0 : (4.5e9 : ℝ) * (3.142 : ℝ) < (2 : ℝ) ^ (-(44 : ℤ)) * (1.618 : ℝ) ^ (112 : ℝ) := by
 160    -- conservative numeric bound (independent of the model)
 161    nlinarith
 162  have hltNum : (4.5e9 : ℝ) * Real.pi < (2 : ℝ) ^ (-(44 : ℤ)) * phi ^ (112 : ℝ) := by
 163    nlinarith [h0, hN, hpiUB, Real.pi_pos]
 164  have h1 : (4.5e9 : ℝ) < (2 : ℝ) ^ (-(44 : ℤ)) * phi ^ (112 : ℝ) / Real.pi := by
 165    rw [lt_div_iff₀ Real.pi_pos]
 166    simpa [mul_assoc, mul_left_comm, mul_comm] using hltNum
 167  simpa [alphaG_pred_closed] using h1
 168

used by (2)

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

depends on (14)

Lean names referenced from this declaration's body.