pith. machine review for the scientific record. sign in
theorem proved tactic proof

ode_cos_uniqueness

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 257private theorem ode_cos_uniqueness (f : ℝ → ℝ)
 258    (h_diff : ContDiff ℝ 2 f)
 259    (h_ode : ∀ t, deriv (deriv f) t = -(f t))
 260    (h_f0 : f 0 = 1) (h_f'0 : deriv f 0 = 0) :
 261    ∀ t, f t = Real.cos t := by

proof body

Tactic-mode proof.

 262  let g := fun t => f t - Real.cos t
 263  have hg_diff : ContDiff ℝ 2 g := h_diff.sub Real.contDiff_cos
 264  have hDf : Differentiable ℝ f :=
 265    h_diff.differentiable (by decide : (2 : WithTop ℕ∞) ≠ 0)
 266  have hg_ode : ∀ t, deriv (deriv g) t = -(g t) := by
 267    intro t
 268    have h1 : deriv g = fun s => deriv f s - deriv Real.cos s :=
 269      funext fun s => deriv_sub hDf.differentiableAt Real.differentiable_cos.differentiableAt
 270    have hDf1 : ContDiff ℝ 1 (deriv f) := by
 271      rw [show (2 : WithTop ℕ∞) = 1 + 1 from rfl] at h_diff
 272      exact (contDiff_succ_iff_deriv.mp h_diff).2.2
 273    have hDcos1 : ContDiff ℝ 1 (deriv Real.cos) := by
 274      rw [Real.deriv_cos']; exact Real.contDiff_sin.neg
 275    have h2 : deriv (deriv g) t = deriv (deriv f) t - deriv (deriv Real.cos) t := by
 276      rw [h1]; exact deriv_sub
 277        (hDf1.differentiable (by decide : (1 : WithTop ℕ∞) ≠ 0) |>.differentiableAt)
 278        (hDcos1.differentiable (by decide : (1 : WithTop ℕ∞) ≠ 0) |>.differentiableAt)
 279    rw [h2, h_ode t]
 280    have : deriv (deriv Real.cos) t = -(Real.cos t) := by
 281      have h_dcos : deriv Real.cos = fun x => -Real.sin x := Real.deriv_cos'
 282      rw [h_dcos]; exact (Real.hasDerivAt_sin t).neg.deriv
 283    rw [this]; ring
 284  have hg0 : g 0 = 0 := by simp [g, h_f0, Real.cos_zero]
 285  have hg'0 : deriv g 0 = 0 := by
 286    have : deriv g 0 = deriv f 0 - deriv Real.cos 0 :=
 287      deriv_sub hDf.differentiableAt Real.differentiable_cos.differentiableAt
 288    rw [this, h_f'0, Real.deriv_cos, Real.sin_zero, neg_zero, sub_zero]
 289  intro t; linarith [ode_neg_zero_uniqueness g hg_diff hg_ode hg0 hg'0 t]
 290
 291/-- **Aczél–Kannappan classification of the d'Alembert functional equation.**
 292
 293Any continuous H : ℝ → ℝ with H(0) = 1 satisfying
 294  H(t+u) + H(t−u) = 2·H(t)·H(u)
 295is exactly one of:
 296* the constant 1,
 297* `Real.cosh (α·)` for some α ∈ ℝ, or
 298* `Real.cos  (α·)` for some α ∈ ℝ.
 299
 300Proof: continuity ⇒ C^∞ via the integration bootstrap (`dAlembert_contDiff_smooth`);
 301C² + d'Alembert ⇒ H'' = c·H with c = H''(0) (`dAlembert_to_ODE_general`);
 302ODE uniqueness in each branch of the trichotomy on c gives the explicit formula. -/

used by (5)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (38)

Lean names referenced from this declaration's body.

… and 8 more