theorem
proved
tactic proof
ode_cos_unit_uniqueness
show as:
view Lean formalization →
formal statement (Lean)
110theorem ode_cos_unit_uniqueness (f : ℝ → ℝ)
111 (h_diff : ContDiff ℝ 2 f)
112 (h_ode : ∀ t, deriv (deriv f) t = -(f t))
113 (h_f0 : f 0 = 1) (h_f'0 : deriv f 0 = 0) :
114 ∀ t, f t = Real.cos t := by
proof body
Tactic-mode proof.
115 let g := fun t => f t - Real.cos t
116 have hg_diff : ContDiff ℝ 2 g := h_diff.sub Real.contDiff_cos
117 have hDf : Differentiable ℝ f :=
118 h_diff.differentiable (by decide : (2 : WithTop ℕ∞) ≠ 0)
119 have hg_ode : ∀ t, deriv (deriv g) t = -(g t) := by
120 intro t
121 have h1 : deriv g = fun s => deriv f s - deriv Real.cos s :=
122 funext fun s => deriv_sub hDf.differentiableAt Real.differentiable_cos.differentiableAt
123 have hDf1 : ContDiff ℝ 1 (deriv f) := by
124 rw [show (2 : WithTop ℕ∞) = 1 + 1 from rfl] at h_diff
125 exact (contDiff_succ_iff_deriv.mp h_diff).2.2
126 have hDcos1 : ContDiff ℝ 1 (deriv Real.cos) := by
127 rw [Real.deriv_cos']; exact Real.contDiff_sin.neg
128 have h2 : deriv (deriv g) t = deriv (deriv f) t - deriv (deriv Real.cos) t := by
129 rw [h1]
130 exact deriv_sub
131 (hDf1.differentiable (by decide : (1 : WithTop ℕ∞) ≠ 0) |>.differentiableAt)
132 (hDcos1.differentiable (by decide : (1 : WithTop ℕ∞) ≠ 0) |>.differentiableAt)
133 rw [h2, h_ode t]
134 have : deriv (deriv Real.cos) t = -(Real.cos t) := by
135 have h_dcos : deriv Real.cos = fun x => -Real.sin x := Real.deriv_cos'
136 rw [h_dcos]
137 exact (Real.hasDerivAt_sin t).neg.deriv
138 rw [this]
139 ring
140 have hg0 : g 0 = 0 := by simp [g, h_f0, Real.cos_zero]
141 have hg'0 : deriv g 0 = 0 := by
142 have : deriv g 0 = deriv f 0 - deriv Real.cos 0 :=
143 deriv_sub hDf.differentiableAt Real.differentiable_cos.differentiableAt
144 rw [this, h_f'0, Real.deriv_cos, Real.sin_zero, neg_zero, sub_zero]
145 intro t
146 linarith [ode_neg_zero_uniqueness g hg_diff hg_ode hg0 hg'0 t]
147
148/-- **Cosine case (proved)**: a smooth function with `H(0) = 1`,
149`H'(0) = 0`, and `H''(x) = -β² · H(x)` is `cos(β·)`. We rescale
150`H_β(t) := H(t/β)` to reduce to the unit-frequency cosine uniqueness
151theorem. -/