theorem
proved
tactic proof
ode_zero_uniqueness_neg
show as:
view Lean formalization →
formal statement (Lean)
102theorem ode_zero_uniqueness_neg (f : ℝ → ℝ)
103 (h_diff2 : ContDiff ℝ 2 f)
104 (h_ode : ∀ t, deriv (deriv f) t = -f t)
105 (h_f0 : f 0 = 0)
106 (h_f'0 : deriv f 0 = 0) :
107 ∀ t, f t = 0 := by
proof body
Tactic-mode proof.
108 intro t
109 have hE := ode_neg_energy_constant f h_diff2 h_ode t
110 have hzero : f t ^ 2 + (deriv f t) ^ 2 = 0 := by
111 simpa [h_f0, h_f'0] using hE
112 have hsq_nonneg : 0 ≤ f t ^ 2 := sq_nonneg (f t)
113 have hderivsq_nonneg : 0 ≤ (deriv f t) ^ 2 := sq_nonneg (deriv f t)
114 have hsq_zero : f t ^ 2 = 0 := by linarith
115 nlinarith [hsq_zero]
116
117/-- cos satisfies the ODE cos'' = -cos. -/