 312    ring
 313
 314/-- If g' = -g and g(0) = 0, then g = 0. -/
 315lemma deriv_neg_self_zero (g : ℝ → ℝ)
 316    (h_diff : Differentiable ℝ g)
 317    (h_deriv : ∀ t, deriv g t = -g t)
 318    (h_g0 : g 0 = 0) :
 319    ∀ t, g t = 0 := by
 320  have h_const : ∀ t, deriv (fun s => g s * Real.exp s) t = 0 := by
 321    intro t
 322    have h1 : deriv (fun s => g s * Real.exp s) t =
 323              deriv g t * Real.exp t + g t * deriv Real.exp t := by
 324      apply deriv_mul h_diff.differentiableAt Real.differentiable_exp.differentiableAt
 325    rw [h1, Real.deriv_exp, h_deriv t]
 326    ring
 327  have h_diff_prod : Differentiable ℝ (fun s => g s * Real.exp s) := by
 328    apply Differentiable.mul h_diff Real.differentiable_exp
 329  have h_is_const := is_const_of_deriv_eq_zero h_diff_prod h_const
 330  intro t
 331  specialize h_is_const t 0
 332  simp only [Real.exp_zero, mul_one] at h_is_const
 333  have h_exp_pos : Real.exp t > 0 := Real.exp_pos t
 334  have h_exp_ne : Real.exp t ≠ 0 := h_exp_pos.ne'
 335  have h_eq : g t * Real.exp t = g 0 := h_is_const
 336  calc g t = g t * Real.exp t / Real.exp t := by field_simp
 337    _ = g 0 / Real.exp t := by rw [h_eq]
 338    _ = 0 / Real.exp t := by rw [h_g0]
 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) :

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.