flat_ode_unique

proof body

Tactic-mode proof.

 286  intro G hODE hG0 hGderiv0 hSmooth t
 287  let f := fun x => G x - x ^ 2 / 2
 288  have hf_ode : ∀ x, deriv (deriv f) x = 0 := by
 289    intro x
 290    unfold f
 291    rw [deriv_sub, deriv_div_const, deriv_pow]
 292    · simp only [Nat.cast_ofNat, pow_one]
 293      rw [deriv_sub, hODE]
 294      · simp only [deriv_div_const, deriv_id'', sub_self]
 295      · exact hSmooth.iterate_deriv 1 1 |>.differentiable (by decide) |>.differentiableAt
 296      · apply DifferentiableAt.div_const; exact (differentiableAt_pow 2)
 297    · exact hSmooth.differentiable (by decide) |>.differentiableAt
 298    · apply DifferentiableAt.div_const; exact (differentiableAt_pow 2)
 299
 300  -- f'' = 0 everywhere means f' is constant
 301  have hf'_const : ∀ x y, deriv f x = deriv f y := by
 302    have hf'_diff : Differentiable ℝ (deriv f) := by
 303      apply (hSmooth.sub (contDiff_pow 2 |>.div_const 2)).iterate_deriv 1 1 |>.differentiable (by decide)
 304    have hf'_deriv_zero : ∀ z, HasDerivAt (deriv f) 0 z := by
 305      intro z
 306      rw [← hf_ode z]
 307      exact hf'_diff.hasDerivAt z
 308    have := IsLocallyConstant.of_hasDeriv hf'_diff.continuous hf'_deriv_zero
 309    rw [isLocallyConstant_iff_isOpen_fiber] at this
 310    exact this.eq_const
 311
 312  -- f'(0) = G'(0) - 0 = 0, so f' = 0 everywhere
 313  have hf'_zero : ∀ x, deriv f x = 0 := by
 314    intro x
 315    rw [hf'_const x 0]
 316    simp only [f, deriv_sub, deriv_div_const, deriv_pow, Nat.cast_ofNat, pow_one, mul_zero, sub_zero]
 317    · rw [hGderiv0]
 318    · exact hSmooth.differentiable (by decide) |>.differentiableAt
 319    · apply DifferentiableAt.div_const; exact (differentiableAt_pow 2)
 320
 321  -- f' = 0 everywhere means f is constant
 322  have hf_const : ∀ x y, f x = f y := by
 323    have hf_diff : Differentiable ℝ f := by
 324      apply (hSmooth.sub (contDiff_pow 2 |>.div_const 2)).differentiable (by decide)
 325    have hf_deriv_zero : ∀ z, HasDerivAt f 0 z := by
 326      intro z
 327      rw [← hf'_zero z]
 328      exact hf_diff.hasDerivAt z
 329    have := IsLocallyConstant.of_hasDeriv hf_diff.continuous hf_deriv_zero
 330    rw [isLocallyConstant_iff_isOpen_fiber] at this
 331    exact this.eq_const
 332
 333  -- f(0) = G(0) - 0 = 0, so f = 0 everywhere
 334  have hf_zero : f 0 = 0 := by simp [f, hG0]
 335
 336  -- Therefore G(t) = t²/2
 337  have hft : f t = 0 := by rw [hf_const t 0, hf_zero]
 338  simp only [f, sub_eq_zero] at hft
 339  exact hft
 340
 341/-- **THEOREM (ODE Uniqueness - Hyperbolic)**: The only C² solution to G'' = G + 1 with
 342    G(0) = 0, G'(0) = 0 is G(t) = cosh(t) - 1.
 343
 344    **Proof**:
 345    1. Let y(t) = G(t) + 1. Then y''(t) = G''(t) = G(t) + 1 = y(t).
 346    2. Initial conditions: y(0) = G(0) + 1 = 1, y'(0) = G'(0) = 0.
 347    3. Let f(t) = y(t) - cosh(t). Then f''(t) = f(t) with f(0)=0, f'(0)=0.
 348    4. Consider the energy E(t) = f'(t)² - f(t)².
 349    5. E'(t) = 2 f'(t) f''(t) - 2 f(t) f'(t) = 2 f'(t) f(t) - 2 f(t) f'(t) = 0.
 350    6. Since E(0) = 0, E(t) = 0 for all t, so f'(t)² = f(t)².
 351    7. This implies f(t) = 0 for all t. -/