ode_zero_uniqueness

formal source

 368    _ = 0 := by simp
 369
 370/-- **Theorem (ODE Zero Uniqueness)**: The unique solution to f'' = f with f(0) = f'(0) = 0 is f = 0. -/
 371theorem ode_zero_uniqueness (f : ℝ → ℝ)
 372    (h_diff2 : ContDiff ℝ 2 f)
 373    (h_ode : ∀ t, deriv (deriv f) t = f t)
 374    (h_f0 : f 0 = 0)
 375    (h_f'0 : deriv f 0 = 0) :
 376    ∀ t, f t = 0 := by
 377  have ⟨h_minus, h_plus⟩ := ode_diagonalization f h_diff2 h_ode
 378  have h_diff1 : Differentiable ℝ f := h_diff2.differentiable (by decide : (2 : WithTop ℕ∞) ≠ 0)
 379  have h_deriv_contdiff : ContDiff ℝ 1 (deriv f) := by
 380    rw [show (2 : WithTop ℕ∞) = 1 + 1 from rfl] at h_diff2
 381    rw [contDiff_succ_iff_deriv] at h_diff2
 382    exact h_diff2.2.2
 383  have h_diff_deriv : Differentiable ℝ (deriv f) := h_deriv_contdiff.differentiable (by decide : (1 : WithTop ℕ∞) ≠ 0)
 384  let g := fun s => deriv f s - f s
 385  let hf := fun s => deriv f s + f s
 386  have hg_diff : Differentiable ℝ g := h_diff_deriv.sub h_diff1
 387  have hh_diff : Differentiable ℝ hf := h_diff_deriv.add h_diff1
 388  have hg0 : g 0 = 0 := by simp [g, h_f0, h_f'0]
 389  have hh0 : hf 0 = 0 := by simp [hf, h_f0, h_f'0]
 390  have hg_deriv : ∀ t, deriv g t = -g t := h_minus
 391  have hh_deriv : ∀ t, deriv hf t = hf t := h_plus
 392  have hg_zero := deriv_neg_self_zero g hg_diff hg_deriv hg0
 393  have hh_zero := deriv_pos_self_zero hf hh_diff hh_deriv hh0
 394  intro t
 395  have hgt := hg_zero t
 396  have hht := hh_zero t
 397  simp only [g, hf] at hgt hht
 398  linarith
 399
 400theorem cosh_second_deriv_eq : ∀ t, deriv (deriv (fun x => Real.cosh x)) t = Real.cosh t := by
 401  intro t