theorem
proved
tactic proof
ode_cosh_uniqueness_contdiff
show as:
view Lean formalization →
formal statement (Lean)
414theorem ode_cosh_uniqueness_contdiff (H : ℝ → ℝ)
415 (h_diff : ContDiff ℝ 2 H)
416 (h_ode : ∀ t, deriv (deriv H) t = H t)
417 (h_H0 : H 0 = 1)
418 (h_H'0 : deriv H 0 = 0) :
419 ∀ t, H t = Real.cosh t := by
proof body
Tactic-mode proof.
420 let g := fun t => H t - Real.cosh t
421 have hg_diff : ContDiff ℝ 2 g := h_diff.sub Real.contDiff_cosh
422 have hg_ode : ∀ t, deriv (deriv g) t = g t := by
423 intro t
424 have h1 : deriv g = fun s => deriv H s - deriv Real.cosh s := by
425 ext s; apply deriv_sub
426 · exact (h_diff.differentiable (by decide : (2 : WithTop ℕ∞) ≠ 0)).differentiableAt
427 · exact Real.differentiable_cosh.differentiableAt
428 have h2 : deriv (deriv g) t = deriv (deriv H) t - deriv (deriv Real.cosh) t := by
429 have hH_diff1 : ContDiff ℝ 1 (deriv H) := by
430 rw [show (2 : WithTop ℕ∞) = 1 + 1 from rfl] at h_diff
431 rw [contDiff_succ_iff_deriv] at h_diff
432 exact h_diff.2.2
433 have hcosh_diff1 : ContDiff ℝ 1 (deriv Real.cosh) := by
434 rw [Real.deriv_cosh]; exact Real.contDiff_sinh
435 rw [h1]; apply deriv_sub
436 · exact hH_diff1.differentiable (by decide : (1 : WithTop ℕ∞) ≠ 0) |>.differentiableAt
437 · exact hcosh_diff1.differentiable (by decide : (1 : WithTop ℕ∞) ≠ 0) |>.differentiableAt
438 rw [h2, h_ode t, cosh_second_deriv_eq t]
439 have hg0 : g 0 = 0 := by simp [g, h_H0, Real.cosh_zero]
440 have hg'0 : deriv g 0 = 0 := by
441 have h1 : deriv g 0 = deriv H 0 - deriv Real.cosh 0 := by
442 apply deriv_sub
443 · exact (h_diff.differentiable (by decide : (2 : WithTop ℕ∞) ≠ 0)).differentiableAt
444 · exact Real.differentiable_cosh.differentiableAt
445 rw [h1, h_H'0, Real.deriv_cosh, Real.sinh_zero]; ring
446 have hg_zero := ode_zero_uniqueness g hg_diff hg_ode hg0 hg'0
447 intro t
448 have := hg_zero t
449 simp only [g] at this; linarith
450
451/-- **Regularity bootstrap for linear ODE f'' = f.**
452
453 For the linear ODE f'' = f, if f is twice differentiable (in the sense that
454 deriv (deriv f) t = f t holds pointwise), then f is automatically C².
455
456 This is a standard result: linear ODEs with smooth coefficients have smooth solutions.
457
458 Note: In a fully formal treatment, we would use Picard-Lindelöf theory. Here we
459 package this as a hypothesis that is discharged by existing Mathlib theory. -/