J_log_zero

formal source

  47noncomputable def J_log (t : ℝ) : ℝ := Real.cosh t - 1
  48
  49/-- J_log(0) = 0 (the minimum). -/
  50@[simp] theorem J_log_zero : J_log 0 = 0 := by simp [J_log]
  51
  52/-- J_log is non-negative. -/
  53theorem J_log_nonneg (t : ℝ) : J_log t ≥ 0 := by
  54  simp only [J_log]
  55  have h : Real.cosh t ≥ 1 := Real.one_le_cosh t
  56  linarith
  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