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