J_log_eq_zero_iff

formal source

  57
  58/-- J_log is zero iff t = 0.
  59    Proof: cosh t = 1 iff t = 0 (by AM-GM on e^t + e^{-t}). -/
  60theorem J_log_eq_zero_iff {t : ℝ} : J_log t = 0 ↔ t = 0 := by
  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. -/
  84theorem J_log_pos {t : ℝ} (ht : t ≠ 0) : J_log t > 0 := by
  85  have hne : J_log t ≠ 0 := fun h => ht (J_log_eq_zero_iff.mp h)
  86  have hge : J_log t ≥ 0 := J_log_nonneg t
  87  exact lt_of_le_of_ne hge (Ne.symm hne)
  88
  89/-- J_log is symmetric: J_log(-t) = J_log(t). -/
  90theorem J_log_symmetric (t : ℝ) : J_log (-t) = J_log t := by