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

log_phi_bounds

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)

 326lemma log_phi_bounds (h_low : log_lower_bound_phi_hypothesis) (h_high : log_upper_bound_phi_hypothesis) :
 327    (0.481211 : ℝ) < Real.log phi ∧ Real.log phi < (0.481213 : ℝ) := by

proof body

Tactic-mode proof.

 328  have hphi := phi_bounds
 329  have h_low' : (0.481211 : ℝ) < Real.log (1.618033 : ℝ) := by
 330    simpa [log_lower_bound_phi_hypothesis] using h_low
 331  have h_high' : Real.log (1.618034 : ℝ) < (0.481213 : ℝ) := by
 332    simpa [log_upper_bound_phi_hypothesis] using h_high
 333  constructor
 334  · -- Lower bound: log(φ) > log(1.618033) > 0.481211
 335    have h_mono : Real.log (1.618033 : ℝ) < Real.log phi := by
 336      apply Real.log_lt_log (by norm_num) hphi.1
 337    exact lt_trans h_low' h_mono
 338  · -- Upper bound: log(φ) < log(1.618034) < 0.481213
 339    have h_mono : Real.log phi < Real.log (1.618034 : ℝ) := by
 340      apply Real.log_lt_log (by linarith [hphi.1]) hphi.2
 341    exact lt_trans h_mono h_high'
 342
 343/-! ### Auxiliary numerical log bounds -/
 344
 345/-- Hypothesis for numerical lower bound: log(1 + 24/1.618034) > 2.7613 -/

used by (12)

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

depends on (9)

Lean names referenced from this declaration's body.