CoshAddIdentity

formal source

  26@[simp] noncomputable def H (F : ℝ → ℝ) (t : ℝ) : ℝ := G F t + 1
  27
  28/-- The cosh-type functional identity for `G_F`. -/
  29def CoshAddIdentity (F : ℝ → ℝ) : Prop :=
  30  ∀ t u : ℝ,
  31    G F (t+u) + G F (t-u) = 2 * (G F t * G F u) + 2 * (G F t + G F u)
  32
  33/-- Direct cosh-add identity on a function. -/
  34def DirectCoshAdd (Gf : ℝ → ℝ) : Prop :=
  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