## Stream: new members

### Topic: zero derivative from minimum value

#### Nicholas Wilson (Nov 08 2023 at 04:29):

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 (Nov 08 2023 at 04:30):

it should follow from Rolle's theorem

#### Mario Carneiro (Nov 08 2023 at 04:32):

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

#### Mario Carneiro (Nov 08 2023 at 04:33):

it just says that f has at least one nonnegative point

#### Nicholas Wilson (Nov 08 2023 at 04:44):

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 (Nov 08 2023 at 04:47):

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

#### Nicholas Wilson (Nov 08 2023 at 05:04):

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 (Nov 08 2023 at 05:54):

Maybe with docs#fderiv_deriv

#### Nicholas Wilson (Nov 08 2023 at 06:57):

scratch that, there is IsLocalMin.deriv_eq_zero

#### Nicholas Wilson (Nov 08 2023 at 07:01):

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

Last updated: Dec 20 2023 at 11:08 UTC