theorem
proved
tactic proof
J_log_eq_zero_iff
show as:
view Lean formalization →
formal statement (Lean)
60theorem J_log_eq_zero_iff {t : ℝ} : J_log t = 0 ↔ t = 0 := by
proof body
Tactic-mode proof.
61 constructor
62 · intro h
63 simp only [J_log] at h
64 have h1 : Real.cosh t = 1 := by linarith
65 -- cosh t = (e^t + e^{-t})/2 = 1 iff e^t + e^{-t} = 2
66 -- By AM-GM, equality holds iff e^t = e^{-t}, i.e., t = 0
67 rw [Real.cosh_eq] at h1
68 have h2 : Real.exp t + Real.exp (-t) = 2 := by linarith
69 -- The only solution is t = 0 (from e^t = e^{-t})
70 have hprod : Real.exp t * Real.exp (-t) = 1 := by rw [← Real.exp_add]; simp
71 -- From e^t + e^{-t} = 2 and e^t · e^{-t} = 1, we get e^t = 1, hence t = 0
72 have h3 : Real.exp t > 0 := Real.exp_pos t
73 have h4 : Real.exp (-t) > 0 := Real.exp_pos (-t)
74 have hsq : (Real.exp t - 1)^2 = 0 := by nlinarith
75 have heq : Real.exp t = 1 := by nlinarith [sq_nonneg (Real.exp t - 1)]
76 have ht_zero : t = 0 := by
77 have := Real.exp_injective (heq.trans Real.exp_zero.symm)
78 linarith
79 exact ht_zero
80 · intro h
81 simp [h, J_log]
82
83/-- J_log is strictly positive for t ≠ 0. -/