ode_neg_energy_constant

formal source

  59For f'' = -f, the characteristic equation is r² = -1, giving r = ±i.
  60The real-valued approach uses: if f'' = -f, then (f' - i·f)' = -i(f' - i·f).
  61In real terms, we use the energy method: E = f² + (f')² is constant. -/
  62theorem ode_neg_energy_constant (f : ℝ → ℝ)
  63    (h_diff2 : ContDiff ℝ 2 f)
  64    (h_ode : ∀ t, deriv (deriv f) t = -f t) :
  65    ∀ t, f t ^ 2 + (deriv f t) ^ 2 = f 0 ^ 2 + (deriv f 0) ^ 2 := by
  66  let E : ℝ → ℝ := fun s => f s * f s + deriv f s * deriv f s
  67  have h_diff1 : Differentiable ℝ f := h_diff2.differentiable (by decide : (2 : WithTop ℕ∞) ≠ 0)
  68  have h_deriv_contdiff : ContDiff ℝ 1 (deriv f) := by
  69    rw [show (2 : WithTop ℕ∞) = 1 + 1 from rfl] at h_diff2
  70    rw [contDiff_succ_iff_deriv] at h_diff2
  71    exact h_diff2.2.2
  72  have h_diff_deriv : Differentiable ℝ (deriv f) :=
  73    h_deriv_contdiff.differentiable (by decide : (1 : WithTop ℕ∞) ≠ 0)
  74  have h_const : ∀ t, deriv E t = 0 := by
  75    intro t
  76    have hE :
  77        deriv E t =
  78          deriv (fun s => f s * f s) t + deriv (fun s => deriv f s * deriv f s) t := by
  79      unfold E
  80      apply deriv_add
  81      · exact (h_diff1.mul h_diff1).differentiableAt
  82      · exact (h_diff_deriv.mul h_diff_deriv).differentiableAt
  83    have hprod1 :
  84        deriv (fun s => f s * f s) t = deriv f t * f t + f t * deriv f t := by
  85      apply deriv_mul h_diff1.differentiableAt h_diff1.differentiableAt
  86    have hprod2 :
  87        deriv (fun s => deriv f s * deriv f s) t =
  88          deriv (deriv f) t * deriv f t + deriv f t * deriv (deriv f) t := by
  89      apply deriv_mul h_diff_deriv.differentiableAt h_diff_deriv.differentiableAt
  90    rw [hE, hprod1, hprod2, h_ode t]
  91    ring
  92  have hE_diff : Differentiable ℝ E := by