ode_neg_zero_uniqueness

formal source

 226
 227/-! ## Phase 3: Classification and Analyticity -/
 228
 229private theorem ode_neg_zero_uniqueness (f : ℝ → ℝ)
 230    (h_diff2 : ContDiff ℝ 2 f)
 231    (h_ode : ∀ t, deriv (deriv f) t = -(f t))
 232    (h_f0 : f 0 = 0) (h_f'0 : deriv f 0 = 0) :
 233    ∀ t, f t = 0 := by
 234  have h_d1 : Differentiable ℝ f := h_diff2.differentiable (by decide : (2 : WithTop ℕ∞) ≠ 0)
 235  have hCD1 : ContDiff ℝ 1 (deriv f) := by
 236    rw [show (2 : WithTop ℕ∞) = 1 + 1 from rfl] at h_diff2
 237    rw [contDiff_succ_iff_deriv] at h_diff2; exact h_diff2.2.2
 238  have h_dd : Differentiable ℝ (deriv f) := hCD1.differentiable (by decide : (1 : WithTop ℕ∞) ≠ 0)
 239  -- Energy E(t) = f(t)² + f'(t)² has E' = 2f'(f + f'') = 2f'(f - f) = 0
 240  -- So E is constant = E(0) = 0, giving f(t)² ≤ 0, hence f = 0.
 241  have hE_deriv_zero : ∀ s, deriv (fun t => f t ^ 2 + deriv f t ^ 2) s = 0 := by
 242    intro s
 243    have h1 : HasDerivAt (fun x => f x ^ 2 + deriv f x ^ 2)
 244        (↑2 * f s ^ (2 - 1) * deriv f s + ↑2 * deriv f s ^ (2 - 1) * deriv (deriv f) s) s :=
 245      ((h_d1 s).hasDerivAt.pow 2).add ((h_dd s).hasDerivAt.pow 2)
 246    have h2 := h1.deriv; rw [h_ode s] at h2; push_cast at h2; simp only [pow_one] at h2
 247    linarith
 248  have hE_eq := is_const_of_deriv_eq_zero
 249    (show Differentiable ℝ (fun t => f t ^ 2 + deriv f t ^ 2) from
 250      (h_d1.pow 2).add (h_dd.pow 2))
 251    hE_deriv_zero
 252  intro t
 253  have hE0 : f 0 ^ 2 + deriv f 0 ^ 2 = 0 := by rw [h_f0, h_f'0]; ring
 254  have hEt := hE_eq t 0; simp only [hE0] at hEt
 255  nlinarith [sq_nonneg (f t), sq_nonneg (deriv f t)]
 256
 257private theorem ode_cos_uniqueness (f : ℝ → ℝ)
 258    (h_diff : ContDiff ℝ 2 f)
 259    (h_ode : ∀ t, deriv (deriv f) t = -(f t))