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

J_bit_eq_cosh

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)

  63theorem J_bit_eq_cosh : J_bit_val = cosh (log phi) - 1 := by

proof body

Tactic-mode proof.

  64  unfold J_bit_val
  65  have hphi : phi > 0 := phi_pos
  66  have h_exp_log : exp (log phi) = phi := exp_log hphi
  67  calc J phi = J (exp (log phi)) := by rw [h_exp_log]
  68    _ = cosh (log phi) - 1 := J_exp_eq_cosh (log phi)
  69
  70/-- J_bit > 0 since φ > 1 implies cosh(ln φ) > 1. -/

used by (1)

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

depends on (2)

Lean names referenced from this declaration's body.