flat_ode_unique

formal source

 276    5. Since f' = 0, f(t) is constant.
 277    6. f(0) = G(0) - 0 = 0, so f(t) = 0 for all t.
 278    7. Thus G(t) = t²/2. -/
 279theorem flat_ode_unique :
 280    ∀ G : ℝ → ℝ,
 281    SatisfiesFlatODE G →
 282    G 0 = 0 →
 283    deriv G 0 = 0 →
 284    ContDiff ℝ 2 G →
 285    ∀ t, G t = t ^ 2 / 2 := by
 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