Local minimum of a function from second derivative

Stream: Is there code for X?

[Max Bobbin]

I'm trying to show that a single variable function has a local minimum at a point because the second derivative at that point is positive. I know that is_local_min f a can be simplified to ∀ᶠ (x : α) in l, f a ≤ f x, but I didn't know how to show such a thing from the derivative. I hav a mwe attached below

example
{a : ℝ} (f : ℝ → ℝ) (hf'' : 0 <( deriv^[2] f a)) (hf' : deriv f a = 0)
:
is_local_min f a :=
begin

end

[Sebastien Gouezel]

This is not true as stated: the function f given by f x = x^2 for x \le 0 and f x = x^2 - 1 for x > 0 is a counterexample (can you see why?)

[Max Bobbin]

but for your first example, if x < 0 that then means the hypothesis hf' isn't true, by assuming hf' that means we can't also say x < 0

[Max Bobbin]

same thing for your second example

[Mauricio Collares]

There's only one example in the above example, as it is a function defined by parts. It is not differentiable at 0, but in Mathlib deriv f a equals 0 when f is not differentiable at a.

[Max Bobbin]

I see, so would this be sovled by requiring f be differentiable at a, or is the derivative not the way to go about this?