`ode_cos_uniqueness`

proved

show as: view math explainer →

module: IndisputableMonolith.Cost.AczelTheorem
domain: Cost
line: 315 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Cost.AczelTheorem on GitHub at line 315.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

 312  have hEt := hE_eq t 0; simp only [hE0] at hEt
 313  nlinarith [sq_nonneg (f t), sq_nonneg (deriv f t)]
 314
 315private theorem ode_cos_uniqueness (f : ℝ → ℝ)
 316    (h_diff : ContDiff ℝ 2 f)
 317    (h_ode : ∀ t, deriv (deriv f) t = -(f t))
 318    (h_f0 : f 0 = 1) (h_f'0 : deriv f 0 = 0) :
 319    ∀ t, f t = Real.cos t := by
 320  let g := fun t => f t - Real.cos t
 321  have hg_diff : ContDiff ℝ 2 g := h_diff.sub Real.contDiff_cos
 322  have hDf : Differentiable ℝ f :=
 323    h_diff.differentiable (by decide : (2 : WithTop ℕ∞) ≠ 0)
 324  have hg_ode : ∀ t, deriv (deriv g) t = -(g t) := by
 325    intro t
 326    have h1 : deriv g = fun s => deriv f s - deriv Real.cos s :=
 327      funext fun s => deriv_sub hDf.differentiableAt Real.differentiable_cos.differentiableAt
 328    have hDf1 : ContDiff ℝ 1 (deriv f) := by
 329      rw [show (2 : WithTop ℕ∞) = 1 + 1 from rfl] at h_diff
 330      exact (contDiff_succ_iff_deriv.mp h_diff).2.2
 331    have hDcos1 : ContDiff ℝ 1 (deriv Real.cos) := by
 332      rw [Real.deriv_cos']; exact Real.contDiff_sin.neg
 333    have h2 : deriv (deriv g) t = deriv (deriv f) t - deriv (deriv Real.cos) t := by
 334      rw [h1]; exact deriv_sub
 335        (hDf1.differentiable (by decide : (1 : WithTop ℕ∞) ≠ 0) |>.differentiableAt)
 336        (hDcos1.differentiable (by decide : (1 : WithTop ℕ∞) ≠ 0) |>.differentiableAt)
 337    rw [h2, h_ode t]
 338    have : deriv (deriv Real.cos) t = -(Real.cos t) := by
 339      have h_dcos : deriv Real.cos = fun x => -Real.sin x := Real.deriv_cos'
 340      rw [h_dcos]; exact (Real.hasDerivAt_sin t).neg.deriv
 341    rw [this]; ring
 342  have hg0 : g 0 = 0 := by simp [g, h_f0, Real.cos_zero]
 343  have hg'0 : deriv g 0 = 0 := by
 344    have : deriv g 0 = deriv f 0 - deriv Real.cos 0 :=
 345      deriv_sub hDf.differentiableAt Real.differentiable_cos.differentiableAt

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.