Jlog_as_exp

formal source

   6
   7noncomputable def Jlog (t : ℝ) : ℝ := ((Real.exp t + Real.exp (-t)) / 2) - 1
   8
   9@[simp] lemma Jlog_as_exp (t : ℝ) : Jlog t = ((Real.exp t + Real.exp (-t)) / 2) - 1 := rfl
  10
  11@[simp] lemma Jlog_zero : Jlog 0 = 0 := by
  12  simp [Jlog]
  13
  14open Complex
  15
  16@[simp] lemma Jlog_eq_cosh_sub_one (t : ℝ) : Jlog t = Real.cosh t - 1 := by
  17  -- `Real.cosh_eq` gives `cosh t = (exp t + exp (-t))/2`.
  18  -- Rewrite the RHS in terms of `exp` and close by reflexivity.
  19  unfold Jlog
  20  rw [Real.cosh_eq t]
  21
  22/-! ## Basic order facts (used in "cost ⇒ atomicity" bridges) -/
  23
  24@[simp] lemma Jlog_nonneg (t : ℝ) : 0 ≤ Jlog t := by
  25  -- rewrite to `0 ≤ cosh t - 1` and discharge via `1 ≤ cosh t`
  26  rw [Jlog_eq_cosh_sub_one]
  27  exact sub_nonneg.mpr (Real.one_le_cosh t)
  28
  29@[simp] lemma Jlog_pos_iff (t : ℝ) : 0 < Jlog t ↔ t ≠ 0 := by
  30  -- rewrite to `0 < cosh t - 1` and use `one_lt_cosh`
  31  rw [Jlog_eq_cosh_sub_one]
  32  constructor
  33  · intro ht
  34    have : (1 : ℝ) < Real.cosh t := (sub_pos).1 ht
  35    exact (Real.one_lt_cosh (x := t)).1 this
  36  · intro hne
  37    have : (1 : ℝ) < Real.cosh t := (Real.one_lt_cosh (x := t)).2 hne
  38    exact (sub_pos).2 this
  39