lemma
proved
tactic proof
ode_diagonalization
show as:
view Lean formalization →
formal statement (Lean)
291lemma ode_diagonalization (f : ℝ → ℝ)
292 (h_diff2 : ContDiff ℝ 2 f)
293 (h_ode : ∀ t, deriv (deriv f) t = f t) :
294 (∀ t, deriv (fun s => deriv f s - f s) t = -(deriv f t - f t)) ∧
295 (∀ t, deriv (fun s => deriv f s + f s) t = deriv f t + f t) := by
proof body
Tactic-mode proof.
296 have h_diff1 : Differentiable ℝ f := h_diff2.differentiable (by decide : (2 : WithTop ℕ∞) ≠ 0)
297 have h_deriv_contdiff : ContDiff ℝ 1 (deriv f) := by
298 rw [show (2 : WithTop ℕ∞) = 1 + 1 from rfl] at h_diff2
299 rw [contDiff_succ_iff_deriv] at h_diff2
300 exact h_diff2.2.2
301 have h_diff_deriv : Differentiable ℝ (deriv f) := h_deriv_contdiff.differentiable (by decide : (1 : WithTop ℕ∞) ≠ 0)
302 constructor
303 · intro t
304 have h1 : deriv (fun s => deriv f s - f s) t = deriv (deriv f) t - deriv f t := by
305 apply deriv_sub h_diff_deriv.differentiableAt h_diff1.differentiableAt
306 rw [h1, h_ode t]
307 ring
308 · intro t
309 have h2 : deriv (fun s => deriv f s + f s) t = deriv (deriv f) t + deriv f t := by
310 apply deriv_add h_diff_deriv.differentiableAt h_diff1.differentiableAt
311 rw [h2, h_ode t]
312 ring
313
314/-- If g' = -g and g(0) = 0, then g = 0. -/