G_zero_of_unit

formal source

  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
  69  have hpos_u : Real.exp u > 0 := Real.exp_pos u
  70  have hne_t : Real.exp t ≠ 0 := hpos_t.ne'
  71  have hne_u : Real.exp u ≠ 0 := hpos_u.ne'
  72  rw [he1, he2]
  73  field_simp
  74  ring
  75
  76theorem even_deriv_at_zero (H : ℝ → ℝ)
  77  (h_even : Function.Even H) (h_diff : DifferentiableAt ℝ H 0) : deriv H 0 = 0 := by
  78  -- For even functions, the derivative at 0 is 0
  79  let negFun : ℝ → ℝ := fun x => -x
  80  have h1 : deriv H 0 = deriv (H ∘ negFun) 0 := by
  81    congr 1