deriv_pos_self_zero

formal source

 339    _ = 0 := by simp
 340
 341/-- If h' = h and h(0) = 0, then h = 0. -/
 342lemma deriv_pos_self_zero (h : ℝ → ℝ)
 343    (h_diff : Differentiable ℝ h)
 344    (h_deriv : ∀ t, deriv h t = h t)
 345    (h_h0 : h 0 = 0) :
 346    ∀ t, h t = 0 := by
 347  have h_const : ∀ t, deriv (fun s => h s * Real.exp (-s)) t = 0 := by
 348    intro t
 349    have h1 : deriv (fun s => h s * Real.exp (-s)) t =
 350              deriv h t * Real.exp (-t) + h t * deriv (fun s => Real.exp (-s)) t := by
 351      apply deriv_mul h_diff.differentiableAt
 352      exact (Real.differentiable_exp.comp differentiable_neg).differentiableAt
 353    rw [h1, deriv_exp_neg, h_deriv t]
 354    ring
 355  have h_diff_prod : Differentiable ℝ (fun s => h s * Real.exp (-s)) := by
 356    apply Differentiable.mul h_diff
 357    exact Real.differentiable_exp.comp differentiable_neg
 358  have h_is_const := is_const_of_deriv_eq_zero h_diff_prod h_const
 359  intro t
 360  specialize h_is_const t 0
 361  simp only [neg_zero, Real.exp_zero, mul_one] at h_is_const
 362  have h_exp_pos : Real.exp (-t) > 0 := Real.exp_pos (-t)
 363  have h_exp_ne : Real.exp (-t) ≠ 0 := h_exp_pos.ne'
 364  have h_eq : h t * Real.exp (-t) = h 0 := h_is_const
 365  calc h t = h t * Real.exp (-t) / Real.exp (-t) := by field_simp
 366    _ = h 0 / Real.exp (-t) := by rw [h_eq]
 367    _ = 0 / Real.exp (-t) := by rw [h_h0]
 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)