lemma
proved
tactic proof
deriv_pos_self_zero
show as:
view Lean formalization →
formal statement (Lean)
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
proof body
Tactic-mode proof.
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. -/