separable_forces_flat_ode

formal source

 154    1. Differentiate functional equation twice in u: G''(t+u) + G''(t-u) = 2G''(u).
 155    2. Evaluate at u=0: 2G''(t) = 2G''(0) = 2.
 156    3. Thus G''(t) = 1. -/
 157theorem separable_forces_flat_ode :
 158    ∀ G : ℝ → ℝ,
 159    (∀ t u, G (t + u) + G (t - u) = 2 * G t + 2 * G u) →
 160    G 0 = 0 →
 161    deriv G 0 = 0 →
 162    deriv (deriv G) 0 = 1 →
 163    ContDiff ℝ 2 G →
 164    SatisfiesFlatODE G := by
 165  intro G hFE hG0 hGderiv0 hCalib hSmooth t
 166  -- Differentiate hFE twice with respect to u at u=0
 167  -- LHS: d²/du² [G(t+u) + G(t-u)] = G''(t+u) + G''(t-u) => 2G''(t) at u=0
 168  -- RHS: d²/du² [2G(t) + 2G(u)] = 2G''(u) => 2G''(0) = 2 at u=0
 169  let f := fun u => G (t + u) + G (t - u)
 170  let g := fun u => 2 * G t + 2 * G u
 171  have hfg : f = g := by funext u; exact hFE t u
 172
 173  -- First derivative of f
 174  have h_deriv_f : ∀ u, deriv f u = deriv G (t + u) - deriv G (t - u) := by
 175    intro u
 176    have h1 : HasDerivAt (fun u => G (t + u)) (deriv G (t + u)) u := by
 177      have hd : HasDerivAt G (deriv G (t + u)) (t + u) := hSmooth.differentiable (by decide) |>.differentiableAt.hasDerivAt
 178      exact hd.comp u (hasDerivAt_id u |>.const_add t)
 179    have h2 : HasDerivAt (fun u => G (t - u)) (- deriv G (t - u)) u := by
 180      have hd : HasDerivAt G (deriv G (t - u)) (t - u) := hSmooth.differentiable (by decide) |>.differentiableAt.hasDerivAt
 181      have hsub : HasDerivAt (fun u => t - u) (-1) u := by
 182        apply HasDerivAt.sub (hasDerivAt_const u t) (hasDerivAt_id u)
 183      exact hd.comp u hsub
 184    exact (h1.add h2).deriv
 185
 186  -- Second derivative of f at 0
 187  have h_2deriv_f_0 : deriv (deriv f) 0 = 2 * deriv (deriv G) t := by