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