zero derivative from minimum value

Stream: new members

[Nicholas Wilson]

How would I go about proving

import Mathlib.Data.Real.Basic
import Mathlib.Analysis.Calculus.Deriv.Basic

open Real
theorem deriv_zero_min_bound
        (x y : ℝ )
        (f : ℝ → ℝ )
        (hd : Differentiable ℝ f )
        --bounded from below by 0
        (hbbz : 0 ≤ (f y) )
        (hz : (f x = 0) ) : (deriv f x ) = 0
  := by sorry

[Mario Carneiro]

it should follow from Rolle's theorem

[Mario Carneiro]

docs#IsLocalMin.fderiv_eq_zero maybe?

[Mario Carneiro]

your assumption hbbz doesn't say that f is bounded below though, it's not universally quantified over y

[Mario Carneiro]

it just says that f has at least one nonnegative point

[Nicholas Wilson]

it just says that f has at least one nonnegative point

Oh. How would I state "is bounded from below by zero" then? (hbbz : ∀ (y : ℝ) 0 ≤ (f y)) ?

[Mario Carneiro]

yes (you need a comma after the (y : R))

[Nicholas Wilson]

Thanks. How do I use IsLocalMin.fderiv_eq_zero? with

by have hmin : IsLocalMin f x := by sorry
   apply IsLocalMin.fderiv_eq_zero hmin

I get an error

tactic 'apply' failed, failed to unify
  fderiv ℝ f x = 0
with
  deriv f x = 0

[Ruben Van de Velde]

Maybe with docs#fderiv_deriv

[Nicholas Wilson]

scratch that, there is IsLocalMin.deriv_eq_zero

[Nicholas Wilson]

This just leaves have hmin : IsLocalMin f x := by sorry which I have no idea.