def
definition
def or abbrev
log_171p6_lower_hypothesis
show as:
view Lean formalization →
formal statement (Lean)
352def log_171p6_lower_hypothesis : Prop := (5.1442 : ℝ) < Real.log (1 + 276 / (1.618034 : ℝ))
proof body
Definition body.
353
354/-- Hypothesis for numerical upper bound: log(1 + 276/1.618033) < 5.1444 -/