theorem
proved
tactic proof
ode_neg_zero_uniqueness
show as:
view Lean formalization →
formal statement (Lean)
76theorem ode_neg_zero_uniqueness (f : ℝ → ℝ)
77 (h_diff2 : ContDiff ℝ 2 f)
78 (h_ode : ∀ t, deriv (deriv f) t = -(f t))
79 (h_f0 : f 0 = 0) (h_f'0 : deriv f 0 = 0) :
80 ∀ t, f t = 0 := by
proof body
Tactic-mode proof.
81 have h_d1 : Differentiable ℝ f := h_diff2.differentiable (by decide : (2 : WithTop ℕ∞) ≠ 0)
82 have hCD1 : ContDiff ℝ 1 (deriv f) := by
83 rw [show (2 : WithTop ℕ∞) = 1 + 1 from rfl] at h_diff2
84 rw [contDiff_succ_iff_deriv] at h_diff2
85 exact h_diff2.2.2
86 have h_dd : Differentiable ℝ (deriv f) :=
87 hCD1.differentiable (by decide : (1 : WithTop ℕ∞) ≠ 0)
88 have hE_deriv_zero : ∀ s, deriv (fun t => f t ^ 2 + deriv f t ^ 2) s = 0 := by
89 intro s
90 have h1 : HasDerivAt (fun x => f x ^ 2 + deriv f x ^ 2)
91 (↑2 * f s ^ (2 - 1) * deriv f s + ↑2 * deriv f s ^ (2 - 1) * deriv (deriv f) s) s :=
92 ((h_d1 s).hasDerivAt.pow 2).add ((h_dd s).hasDerivAt.pow 2)
93 have h2 := h1.deriv
94 rw [h_ode s] at h2
95 push_cast at h2
96 simp only [pow_one] at h2
97 linarith
98 have hE_eq := is_const_of_deriv_eq_zero
99 (show Differentiable ℝ (fun t => f t ^ 2 + deriv f t ^ 2) from
100 (h_d1.pow 2).add (h_dd.pow 2))
101 hE_deriv_zero
102 intro t
103 have hE0 : f 0 ^ 2 + deriv f 0 ^ 2 = 0 := by rw [h_f0, h_f'0]; ring
104 have hEt := hE_eq t 0
105 simp only [hE0] at hEt
106 nlinarith [sq_nonneg (f t), sq_nonneg (deriv f t)]
107
108/-- **Unit-frequency cosine uniqueness**: a C² solution of `f'' = -f`
109with `f(0)=1` and `f'(0)=0` is `cos`. -/