dAlembert_classification

proof body

Tactic-mode proof.

 309  have h_sm : ContDiff ℝ smooth H := dAlembert_contDiff_smooth H h_one h_cont h_dAl
 310  have h2 : ContDiff ℝ 2 H := by exact_mod_cast (contDiff_infty.mp h_sm) 2
 311  have hDiff : Differentiable ℝ H := h2.differentiable (by decide : (2 : WithTop ℕ∞) ≠ 0)
 312  have h_H'0 : deriv H 0 = 0 :=
 313    even_deriv_at_zero H (dAlembert_even H h_one h_dAl) hDiff.differentiableAt
 314  have h_ode := dAlembert_to_ODE_general H h_sm h_dAl
 315  set c := deriv (deriv H) 0 with hc_def
 316  have hDD : Differentiable ℝ (deriv H) := by
 317    rw [show (2 : WithTop ℕ∞) = 1 + 1 from rfl] at h2
 318    exact (contDiff_succ_iff_deriv.mp h2).2.2.differentiable (by decide : (1 : WithTop ℕ∞) ≠ 0)
 319  by_cases hc_pos : 0 < c
 320  · -- c > 0: H = cosh(√c · t)
 321    right; left; refine ⟨Real.sqrt c, ?_⟩
 322    have hsc_ne : Real.sqrt c ≠ 0 := ne_of_gt (Real.sqrt_pos.mpr hc_pos)
 323    let g : ℝ → ℝ := fun s => H (s / Real.sqrt c)
 324    have h_div : ∀ s, HasDerivAt (fun x => x / Real.sqrt c) (Real.sqrt c)⁻¹ s := fun s => by
 325      have := (hasDerivAt_id s).div_const (Real.sqrt c); simp only [id, one_div] at this; exact this
 326    have hg_d : ∀ s, HasDerivAt g (deriv H (s / Real.sqrt c) * (Real.sqrt c)⁻¹) s :=
 327      fun s => (hDiff _).hasDerivAt.comp s (h_div s)
 328    have hg_ode : ∀ t, deriv (deriv g) t = g t := by
 329      intro s
 330      have hg1 : deriv g = fun s => deriv H (s / Real.sqrt c) * (Real.sqrt c)⁻¹ :=
 331        funext fun s => (hg_d s).deriv
 332      have h_dd_g : HasDerivAt (deriv g)
 333          ((deriv (deriv H) (s / Real.sqrt c) * (Real.sqrt c)⁻¹) * (Real.sqrt c)⁻¹) s := by
 334        rw [hg1]
 335        exact ((hDD (s / Real.sqrt c)).hasDerivAt.comp s (h_div s)).mul_const _
 336      rw [h_dd_g.deriv, h_ode (s / Real.sqrt c)]
 337      simp only [g]
 338      rw [show c * H (s / Real.sqrt c) * (Real.sqrt c)⁻¹ * (Real.sqrt c)⁻¹ =
 339          H (s / Real.sqrt c) * (c * ((Real.sqrt c)⁻¹ * (Real.sqrt c)⁻¹)) from by ring,
 340          show (Real.sqrt c)⁻¹ * (Real.sqrt c)⁻¹ = (Real.sqrt c * Real.sqrt c)⁻¹ from
 341            (mul_inv_rev _ _).symm,
 342          Real.mul_self_sqrt (le_of_lt hc_pos),
 343          mul_inv_cancel₀ (ne_of_gt hc_pos), mul_one]
 344    intro t
 345    have := ode_cosh_uniqueness_contdiff g (h2.comp (contDiff_id.div_const _))
 346      hg_ode (by simp [g, h_one]) (by rw [(hg_d 0).deriv]; simp [h_H'0])
 347      (Real.sqrt c * t)
 348    simp only [g, mul_div_cancel_left₀ _ hsc_ne] at this; exact this
 349  · by_cases hc_neg : c < 0
 350    · -- c < 0: H = cos(√(−c) · t)
 351      right; right; refine ⟨Real.sqrt (-c), ?_⟩
 352      set c' := -c
 353      have hsc_ne : Real.sqrt c' ≠ 0 := ne_of_gt (Real.sqrt_pos.mpr (neg_pos.mpr hc_neg))
 354      let g : ℝ → ℝ := fun s => H (s / Real.sqrt c')
 355      have h_div : ∀ s, HasDerivAt (fun x => x / Real.sqrt c') (Real.sqrt c')⁻¹ s := fun s => by
 356        have := (hasDerivAt_id s).div_const (Real.sqrt c'); simp only [id, one_div] at this; exact this
 357      have hg_d : ∀ s, HasDerivAt g (deriv H (s / Real.sqrt c') * (Real.sqrt c')⁻¹) s :=
 358        fun s => (hDiff _).hasDerivAt.comp s (h_div s)
 359      have hg_ode : ∀ t, deriv (deriv g) t = -(g t) := by
 360        intro s
 361        have hg1 : deriv g = fun s => deriv H (s / Real.sqrt c') * (Real.sqrt c')⁻¹ :=
 362          funext fun s => (hg_d s).deriv
 363        have h_dd_g : HasDerivAt (deriv g)
 364            ((deriv (deriv H) (s / Real.sqrt c') * (Real.sqrt c')⁻¹) * (Real.sqrt c')⁻¹) s := by
 365          rw [hg1]
 366          exact ((hDD (s / Real.sqrt c')).hasDerivAt.comp s (h_div s)).mul_const _
 367        rw [h_dd_g.deriv, h_ode (s / Real.sqrt c')]
 368        simp only [g, c']
 369        rw [show c * H (s / Real.sqrt (-c)) * (Real.sqrt (-c))⁻¹ * (Real.sqrt (-c))⁻¹ =
 370            H (s / Real.sqrt (-c)) * (c * ((Real.sqrt (-c))⁻¹ * (Real.sqrt (-c))⁻¹)) from by ring,
 371            show (Real.sqrt (-c))⁻¹ * (Real.sqrt (-c))⁻¹ = (Real.sqrt (-c) * Real.sqrt (-c))⁻¹ from
 372              (mul_inv_rev _ _).symm,
 373            Real.mul_self_sqrt (le_of_lt (neg_pos.mpr hc_neg)),
 374            show c * (-c)⁻¹ = -(1 : ℝ) from by
 375              have hc_ne : c ≠ 0 := ne_of_lt hc_neg
 376              field_simp]
 377        ring
 378      intro t
 379      have := ode_cos_uniqueness g (h2.comp (contDiff_id.div_const _))
 380        hg_ode (by simp [g, h_one]) (by rw [(hg_d 0).deriv]; simp [h_H'0])
 381        (Real.sqrt c' * t)
 382      simp only [g, mul_div_cancel_left₀ _ hsc_ne] at this; exact this
 383    · -- c = 0: H ≡ 1
 384      left
 385      have hc0 : c = 0 := le_antisymm (not_lt.mp hc_pos) (not_lt.mp hc_neg)
 386      have h_H'_zero : ∀ t, deriv H t = 0 := by
 387        have := is_const_of_deriv_eq_zero hDD (fun t => by rw [h_ode t, hc0, zero_mul])
 388        intro t; have := this t 0; simp [h_H'0] at this; exact this
 389-- ... 5 more lines elided ...