ode_constant_case

formal source

  41gives `deriv H` constant; `deriv H 0 = 0` then forces
  42`deriv H ≡ 0`; differentiability of `H` plus this gives `H` constant;
  43`H 0 = 1` finishes. -/
  44theorem ode_constant_case
  45    (H : ℝ → ℝ) (h_smooth : ContDiff ℝ 2 H)
  46    (h_one : H 0 = 1) (h_deriv0 : deriv H 0 = 0)
  47    (h_d2_zero : ∀ x, deriv (deriv H) x = 0) :
  48    ∀ x, H x = 1 := by
  49  -- Step 1: H is differentiable.
  50  have hDiffH : Differentiable ℝ H :=
  51    h_smooth.differentiable (by decide : (2 : WithTop ℕ∞) ≠ 0)
  52  -- Step 2: deriv H is differentiable.
  53  have hC2 : ContDiff ℝ 2 H := h_smooth
  54  have hC2eq : (2 : WithTop ℕ∞) = 1 + 1 := rfl
  55  rw [hC2eq] at hC2
  56  rw [contDiff_succ_iff_deriv] at hC2
  57  have hC1_dH : ContDiff ℝ 1 (deriv H) := hC2.2.2
  58  have hDiff_dH : Differentiable ℝ (deriv H) :=
  59    hC1_dH.differentiable (by decide : (1 : WithTop ℕ∞) ≠ 0)
  60  -- Step 3: deriv H is globally constant (its derivative is everywhere 0).
  61  have h_dH_const : ∀ x y, deriv H x = deriv H y :=
  62    is_const_of_deriv_eq_zero hDiff_dH h_d2_zero
  63  -- Step 4: deriv H is identically 0.
  64  have h_dH_zero : ∀ x, deriv H x = 0 := fun x => by
  65    rw [h_dH_const x 0, h_deriv0]
  66  -- Step 5: H is globally constant.
  67  have h_H_const : ∀ x y, H x = H y :=
  68    is_const_of_deriv_eq_zero hDiffH h_dH_zero
  69  -- Step 6: H ≡ H 0 = 1.
  70  intro x
  71  rw [h_H_const x 0, h_one]
  72
  73/-- **Zero uniqueness for `f'' = -f`**: if `f(0)=0` and `f'(0)=0`,
  74then `f ≡ 0`. Proof by conservation of the energy