cosh_satisfies_dalembert

formal source

  57  ∀ t u : ℝ, H (t + u) + H (t - u) = 2 * H t * H u
  58
  59/-- cosh satisfies the d'Alembert equation. -/
  60theorem cosh_satisfies_dalembert : SatisfiesDAlembert Real.cosh := by
  61  intro t u
  62  rw [Real.cosh_add, Real.cosh_sub]
  63  ring
  64
  65/-- The RS cost function G(t) = J(e^t) = cosh(t) - 1 shifted by 1
  66    gives H(t) = cosh(t) which satisfies d'Alembert. -/
  67theorem rs_cost_satisfies_dalembert :
  68    SatisfiesDAlembert (fun t => Cost.Jcost (Real.exp t) + 1) := by
  69  intro t u
  70  simp only [Cost.Jcost_exp_cosh]
  71  rw [Real.cosh_add, Real.cosh_sub]
  72  ring
  73
  74/-- cosh has no real zeros: cosh(t) ≥ 1 for all t ∈ ℝ. -/
  75theorem cosh_no_real_zeros (t : ℝ) : 1 ≤ Real.cosh t := by
  76  have h := Real.cosh_pos t
  77  have h2 := Cost.cosh_quadratic_lower_bound t
  78  linarith [sq_nonneg t]
  79
  80/-- cosh(0) = 1: the unique real minimum. -/
  81theorem cosh_at_zero : Real.cosh 0 = 1 := by
  82  simp [Real.cosh_zero]
  83
  84/-- The J-cost G(t) = cosh(t) - 1 has its unique real zero at t = 0.
  85    In log coordinates, t = 0 means x = e⁰ = 1: the RS balance point. -/
  86theorem jcost_log_zero_unique (t : ℝ) :
  87    Cost.Jcost (Real.exp t) = 0 ↔ t = 0 := by
  88  rw [show Cost.Jcost (Real.exp t) = Cost.Jlog t from rfl]
  89  exact Cost.Jlog_eq_zero_iff t
  90