even_deriv_at_zero

formal source

  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
  82    ext x
  83    simp only [Function.comp_apply, negFun]
  84    exact (h_even x).symm
  85  have h2 : deriv (H ∘ negFun) 0 = -deriv H 0 := by
  86    have hd : DifferentiableAt ℝ negFun 0 := differentiable_neg.differentiableAt
  87    have h_diff_neg : DifferentiableAt ℝ H (negFun 0) := by simp [negFun]; exact h_diff
  88    have hchain := deriv_comp (x := (0 : ℝ)) h_diff_neg hd
  89    rw [hchain]
  90    simp only [negFun, neg_zero]
  91    have hdn : deriv negFun 0 = -1 := congrFun deriv_neg' 0
  92    rw [hdn]
  93    ring
  94  rw [h1] at h2
  95  linarith
  96
  97lemma dAlembert_even
  98  (H : ℝ → ℝ)
  99  (h_one : H 0 = 1)
 100  (h_dAlembert : ∀ t u, H (t+u) + H (t-u) = 2 * H t * H u) :
 101  Function.Even H := by
 102  intro u
 103  have h := h_dAlembert 0 u
 104  simpa [h_one, zero_add, sub_eq_add_neg, two_mul] using h
 105
 106lemma dAlembert_double