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

jcost_exp_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)

  41private theorem jcost_exp_eq_cosh (t : ℝ) :
  42    Jcost (Real.exp t) = Real.cosh t - 1 := by

proof body

Term-mode proof.

  43  rw [Jcost_exp, Real.cosh_eq]
  44
  45/-! ## §1. The defect-coordinate map -/
  46
  47/-- The defect-coordinate map: σ ↦ e^{2(σ − 1/2)}.
  48    Maps the critical strip to ℝ₊ with the critical line 1/2 ↦ 1. -/

used by (1)

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

depends on (4)

Lean names referenced from this declaration's body.