IndisputableMonolith.Relativity.Calculus.FunctionalEquationDeriv

   1import Mathlib
   2
   3namespace IndisputableMonolith
   4namespace Relativity
   5namespace Calculus
   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
  40      have hsub : HasDerivAt (fun s => x - s) (-1) y := by
  41        apply HasDerivAt.sub (hasDerivAt_const y x) (hasDerivAt_id y)
  42      exact hd.comp y hsub
  43    exact (h1.add h2).deriv
  44
  45  have h_second_deriv_g : HasDerivAt (deriv g) (2 * deriv (deriv f) x) 0 := by
  46    simp_rw [h_deriv_fun]
  47    -- Differentiate y => deriv f (x+y) - deriv f (x-y)
  48    have h1 : HasDerivAt (fun y => deriv f (x + y)) (deriv (deriv f) x) 0 := by
  49      have hd : HasDerivAt (deriv f) (deriv (deriv f) x) x :=
  50        hf.iterate_deriv 1 1 |>.differentiable (by decide) |>.differentiableAt.hasDerivAt
  51      exact hd.comp 0 (hasDerivAt_id 0 |>.const_add x)
  52    have h2 : HasDerivAt (fun y => deriv f (x - y)) (- deriv (deriv f) x) 0 := by
  53      have hd : HasDerivAt (deriv f) (deriv (deriv f) x) x :=
  54        hf.iterate_deriv 1 1 |>.differentiable (by decide) |>.differentiableAt.hasDerivAt
  55      have hsub : HasDerivAt (fun y => x - y) (-1) 0 := by
  56        apply HasDerivAt.sub (hasDerivAt_const 0 x) (hasDerivAt_id 0)
  57      exact hd.comp 0 hsub
  58    convert h1.sub h2 using 1; ring
  59
  60  -- 3. Show that HasDerivAt (deriv h) (2 * f(x) * f''(0)) 0
  61  have h_second_deriv_h : HasDerivAt (deriv h) (2 * f x * deriv (deriv f) 0) 0 := by
  62    unfold h
  63    have h_deriv_fun : ∀ y, deriv h y = 2 * f x * deriv f y := by
  64      intro y; rw [deriv_const_mul]; exact hf.differentiable (by decide) |>.differentiableAt
  65    simp_rw [h_deriv_fun]
  66    apply HasDerivAt.const_mul
  67    exact hf.iterate_deriv 1 1 |>.differentiable (by decide) |>.differentiableAt.hasDerivAt
  68
  69  -- 4. Equate
  70  have h_eq : deriv (deriv g) 0 = deriv (deriv h) 0 := by rw [hgh]
  71  rw [h_second_deriv_g.deriv, h_second_deriv_h.deriv] at h_eq
  72  linarith
  73
  74end Calculus
  75end Relativity
  76end IndisputableMonolith
  77