theorem
proved
tactic proof
ode_cos_uniqueness_contdiff
show as:
view Lean formalization →
formal statement (Lean)
137theorem ode_cos_uniqueness_contdiff (H : ℝ → ℝ)
138 (h_diff : ContDiff ℝ 2 H)
139 (h_ode : ∀ t, deriv (deriv H) t = -H t)
140 (h_H0 : H 0 = 1)
141 (h_H'0 : deriv H 0 = 0) :
142 ∀ t, H t = Real.cos t := by
proof body
Tactic-mode proof.
143 let g := fun t => H t - Real.cos t
144 have hg_diff : ContDiff ℝ 2 g := h_diff.sub Real.contDiff_cos
145 have hg_ode : ∀ t, deriv (deriv g) t = -g t := by
146 intro t
147 have h1 : deriv g = fun s => deriv H s - deriv (fun x => Real.cos x) s := by
148 ext s
149 apply deriv_sub
150 · exact (h_diff.differentiable (by decide : (2 : WithTop ℕ∞) ≠ 0)).differentiableAt
151 · exact Real.differentiable_cos.differentiableAt
152 have h2 : deriv (deriv g) t = deriv (deriv H) t - deriv (deriv (fun x => Real.cos x)) t := by
153 have hH_diff1 : ContDiff ℝ 1 (deriv H) := by
154 rw [show (2 : WithTop ℕ∞) = 1 + 1 from rfl] at h_diff
155 rw [contDiff_succ_iff_deriv] at h_diff
156 exact h_diff.2.2
157 have hcos_diff1 : ContDiff ℝ 1 (deriv (fun x => Real.cos x)) := by
158 simpa [Real.deriv_cos] using (Real.contDiff_sin.neg)
159 rw [h1]
160 apply deriv_sub
161 · exact hH_diff1.differentiable (by decide : (1 : WithTop ℕ∞) ≠ 0) |>.differentiableAt
162 · exact hcos_diff1.differentiable (by decide : (1 : WithTop ℕ∞) ≠ 0) |>.differentiableAt
163 rw [h2, h_ode t, cos_second_deriv_eq t]
164 ring
165 have hg0 : g 0 = 0 := by
166 simp [g, h_H0, Real.cos_zero]
167 have hg'0 : deriv g 0 = 0 := by
168 have h1 : deriv g 0 = deriv H 0 - deriv (fun x => Real.cos x) 0 := by
169 apply deriv_sub
170 · exact (h_diff.differentiable (by decide : (2 : WithTop ℕ∞) ≠ 0)).differentiableAt
171 · exact Real.differentiable_cos.differentiableAt
172 rw [h1, h_H'0, Real.deriv_cos]
173 simp [Real.sin_zero]
174 have hg_zero := ode_zero_uniqueness_neg g hg_diff hg_ode hg0 hg'0
175 intro t
176 have hgt := hg_zero t
177 simp [g] at hgt
178 linarith
179
180/-! ## Part 2: Regularity Hypotheses for Cosine Branch
181
182Mirror the structure from Cost.FunctionalEquation but for H'' = -H.
183-/
184
185/-- **Regularity bootstrap for linear ODE f'' = -f.**
186
187For the linear ODE f'' = -f, if f is twice differentiable (in the sense that
188deriv (deriv f) t = -f t holds pointwise), then f is automatically C².
189
190This is a standard result: linear ODEs with smooth coefficients have smooth solutions. -/