CoshAddIdentity_implies_DirectCoshAdd

formal source

  35  ∀ t u : ℝ,
  36    Gf (t+u) + Gf (t-u) = 2 * (Gf t * Gf u) + 2 * (Gf t + Gf u)
  37
  38lemma CoshAddIdentity_implies_DirectCoshAdd (F : ℝ → ℝ)
  39  (h : CoshAddIdentity F) :
  40  DirectCoshAdd (G F) := h
  41
  42lemma G_even_of_reciprocal_symmetry
  43  (F : ℝ → ℝ)
  44  (hSymm : ∀ {x : ℝ}, 0 < x → F x = F x⁻¹) :
  45  Function.Even (G F) := by
  46  intro t
  47  have hpos : 0 < Real.exp t := Real.exp_pos t
  48  have hrec : Real.exp (-t) = (Real.exp t)⁻¹ := by simp [Real.exp_neg]
  49  simp [G, hrec, hSymm hpos]
  50
  51lemma G_zero_of_unit (F : ℝ → ℝ) (hUnit : F 1 = 0) : G F 0 = 0 := by
  52  simpa [G] using hUnit
  53
  54theorem Jcost_G_eq_cosh_sub_one (t : ℝ) : G Cost.Jcost t = Real.cosh t - 1 := by
  55  simp only [G, Jcost]
  56  -- Jcost(exp t) = (exp t + exp(-t))/2 - 1 = cosh t - 1
  57  have h1 : (Real.exp t)⁻¹ = Real.exp (-t) := by simp [Real.exp_neg]
  58  rw [h1, Real.cosh_eq]
  59
  60theorem Jcost_cosh_add_identity : CoshAddIdentity Cost.Jcost := by
  61  intro t u
  62  simp only [G, Jcost]
  63  -- Use exp(t+u) = exp(t)*exp(u) and exp(t-u) = exp(t)/exp(u)
  64  have he1 : Real.exp (t + u) = Real.exp t * Real.exp u := Real.exp_add t u
  65  have he2 : Real.exp (t - u) = Real.exp t / Real.exp u := by
  66    rw [sub_eq_add_neg, Real.exp_add, Real.exp_neg]
  67    ring
  68  have hpos_t : Real.exp t > 0 := Real.exp_pos t