dalembert_deriv_ode

formal source

   6
   7/-- **LEMMA**: Differentiating the d'Alembert functional equation twice.
   8    If f(x+y) + f(x-y) = 2f(x)f(y), then f''(x) = f''(0) f(x). -/
   9theorem dalembert_deriv_ode (f : ℝ → ℝ) (hf : ContDiff ℝ 2 f)
  10    (hDA : ∀ x y, f (x + y) + f (x - y) = 2 * f x * f y) :
  11    ∀ x, deriv (deriv f) x = deriv (deriv f) 0 * f x := by
  12  intro x
  13  -- Differentiate w.r.t y twice at y=0
  14  let g := fun y => f (x + y) + f (x - y)
  15  let h := fun y => 2 * f x * f y
  16  have hgh : g = h := by funext y; exact hDA x y
  17
  18  -- 1. Show that deriv g 0 = 0
  19  have h_deriv_g : HasDerivAt g 0 0 := by
  20    -- g'(y) = f'(x+y) - f'(x-y)
  21    have h1 : HasDerivAt (fun y => f (x + y)) (deriv f x) 0 := by
  22      have hd : HasDerivAt f (deriv f x) x := hf.differentiable (by decide) |>.differentiableAt.hasDerivAt
  23      exact hd.comp 0 (hasDerivAt_id 0 |>.const_add x)
  24    have h2 : HasDerivAt (fun y => f (x - y)) (- deriv f x) 0 := by
  25      have hd : HasDerivAt f (deriv f x) x := hf.differentiable (by decide) |>.differentiableAt.hasDerivAt
  26      have hsub : HasDerivAt (fun y => x - y) (-1) 0 := by
  27        apply HasDerivAt.sub (hasDerivAt_const 0 x) (hasDerivAt_id 0)
  28      exact hd.comp 0 hsub
  29    convert h1.add h2 using 1; ring
  30
  31  -- 2. Show that HasDerivAt (deriv g) (2 * f''(x)) 0
  32  -- We need to compute the derivative of y => deriv f (x+y) - deriv f (x-y)
  33  have h_deriv_fun : ∀ y, deriv g y = deriv f (x + y) - deriv f (x - y) := by
  34    intro y
  35    have h1 : HasDerivAt (fun s => f (x + s)) (deriv f (x + y)) y := by
  36      have hd : HasDerivAt f (deriv f (x + y)) (x + y) := hf.differentiable (by decide) |>.differentiableAt.hasDerivAt
  37      exact hd.comp y (hasDerivAt_id y |>.const_add x)
  38    have h2 : HasDerivAt (fun s => f (x - s)) (- deriv f (x - y)) y := by
  39      have hd : HasDerivAt f (deriv f (x - y)) (x - y) := hf.differentiable (by decide) |>.differentiableAt.hasDerivAt