theorem
proved
tactic proof
ode_neg_energy_constant
show as:
view Lean formalization →
formal statement (Lean)
62theorem ode_neg_energy_constant (f : ℝ → ℝ)
63 (h_diff2 : ContDiff ℝ 2 f)
64 (h_ode : ∀ t, deriv (deriv f) t = -f t) :
65 ∀ t, f t ^ 2 + (deriv f t) ^ 2 = f 0 ^ 2 + (deriv f 0) ^ 2 := by
proof body
Tactic-mode proof.
66 let E : ℝ → ℝ := fun s => f s * f s + deriv f s * deriv f s
67 have h_diff1 : Differentiable ℝ f := h_diff2.differentiable (by decide : (2 : WithTop ℕ∞) ≠ 0)
68 have h_deriv_contdiff : ContDiff ℝ 1 (deriv f) := by
69 rw [show (2 : WithTop ℕ∞) = 1 + 1 from rfl] at h_diff2
70 rw [contDiff_succ_iff_deriv] at h_diff2
71 exact h_diff2.2.2
72 have h_diff_deriv : Differentiable ℝ (deriv f) :=
73 h_deriv_contdiff.differentiable (by decide : (1 : WithTop ℕ∞) ≠ 0)
74 have h_const : ∀ t, deriv E t = 0 := by
75 intro t
76 have hE :
77 deriv E t =
78 deriv (fun s => f s * f s) t + deriv (fun s => deriv f s * deriv f s) t := by
79 unfold E
80 apply deriv_add
81 · exact (h_diff1.mul h_diff1).differentiableAt
82 · exact (h_diff_deriv.mul h_diff_deriv).differentiableAt
83 have hprod1 :
84 deriv (fun s => f s * f s) t = deriv f t * f t + f t * deriv f t := by
85 apply deriv_mul h_diff1.differentiableAt h_diff1.differentiableAt
86 have hprod2 :
87 deriv (fun s => deriv f s * deriv f s) t =
88 deriv (deriv f) t * deriv f t + deriv f t * deriv (deriv f) t := by
89 apply deriv_mul h_diff_deriv.differentiableAt h_diff_deriv.differentiableAt
90 rw [hE, hprod1, hprod2, h_ode t]
91 ring
92 have hE_diff : Differentiable ℝ E := by
93 unfold E
94 exact (h_diff1.mul h_diff1).add (h_diff_deriv.mul h_diff_deriv)
95 have h_is_const := is_const_of_deriv_eq_zero hE_diff h_const
96 intro t
97 specialize h_is_const t 0
98 simpa [E, pow_two] using h_is_const
99
100/-- **Theorem (ODE Zero Uniqueness for f'' = -f)**:
101The unique solution to f'' = -f with f(0) = 0 and f'(0) = 0 is f = 0. -/