Formalize the solution of a differencial equation

Stream: new members

[Nick_adfor]

I want to formalize this math problem:

Natural Language

Consider the set of continuous functions f, whose nth derivative exists for all positive integer n, satisfying f(x)=f'''(x), f(0)+f'(0)+f''(0)=0, and f(0)=f'(0). For each such function f, let m(f) be the smallest nonnegative x satisfying f(x)=0. Compute all possible values of m(f).

I've already found the answer of m(f) on my manuscripts. I just need to check the answer in Lean. The first step is to formalize the problem and the answer (ignore the proof).

But I don't know how to give a good def of m.

import Mathlib

--I don't know how to give a good def of m--

example : ∀ f : ℝ → ℝ,
  (∀ n : ℕ, ContDiff ℝ n f) →
  (∀ x, deriv^[3] f x = f x) →
  (f 0 + deriv f 0 + deriv^[2] f 0 = 0) →
  (f 0 = deriv f 0) →
  (m f = 0 ∨ m f = 5 * pi * Nat.sqrt 3 / 9) := by sorry

[Nick_adfor]

I want to write the code like this, but failed. Maybe there's some grammar problem.

import Mathlib

def K (f : ℝ → ℝ) : Set ℝ :=
  {x | 0 ≤ x ∧ f x = 0}

def m (f : ℝ → ℝ) : ℝ :=
  if h : Nonempty (K f) then Min (K f) else 0

example : ∀ f : ℝ → ℝ,
  (∀ n : ℕ, ContDiff ℝ n f) →
  (∀ x, deriv^[3] f x = f x) →
  (f 0 + deriv f 0 + deriv^[2] f 0 = 0) →
  (f 0 = deriv f 0) →
  (m f = 0 ∨ m f = 5 * pi * Nat.sqrt 3 / 9) := by sorry

[Nick_adfor]

I try to correct the code and it succeed.
Use "sInf" but not "Min". Yet I don't know why. It's just my copy from Mathlib. I do not understand it.

import Mathlib

open Real Filter

noncomputable def m (f : ℝ → ℝ) : ℝ :=
  sInf {x | x ≥ 0 ∧ f x = 0}

example : ∀ f : ℝ → ℝ,
  (∀ n : ℕ, ContDiff ℝ n f) →
  (∀ x, deriv^[3] f x = f x) →
  (f 0 + deriv f 0 + deriv^[2] f 0 = 0) →
  (f 0 = deriv f 0) →
  (m f = 0 ∨ m f = 5 * π * Nat.sqrt 3 / 9) := by sorry

--Here I found the wrong code use "pi" not "π". Oh... A silly mistake.