Second Derivative Test

Stream: maths

[Bjørn Kjos-Hanssen]

Where can I find the good old Second Derivative Test in Mathlib? Or the First Derivative Test?
Searching only brought up the partial converse, Fermat's theorem.

[Ralf Stephan]

Did you try https://leansearch.net/?

[Bjørn Kjos-Hanssen]

Tried it now but the result is about the same for the query "derivative maximum" as on Moogle.AI

[Julian Berman]

I don't know the calculus API but I don't see it myself either looking at Mathlib/Analysis/Calculus/LocalExtr which seems like where it might be. (I also don't know what generality it's true in? But it might be a decent exercise to prove it and see if someone comes along and gives tips if it needs generalizing.)

[Bjørn Kjos-Hanssen]

Julian Berman said:

I don't know the calculus API but I don't see it myself either looking at Mathlib/Analysis/Calculus/LocalExtr which seems like where it might be. (I also don't know what generality it's true in? But it might be a decent exercise to prove it and see if someone comes along and gives tips if it needs generalizing.)

I proved a version of the First Derivative Test just now and indeed it was a fun exercise.

[Julian Berman]

Nice. And ah ok so now that I was going to say "maybe the undergrad.yml file has something", I see it indeed has:

    local extrema: 'IsLocalMin.fderiv_eq_zero'

i.e. docs#IsLocalMin.fderiv_eq_zero -- just pointing that out as well in case you didn't see that (I glanced over it until now). Edit: you mentioned this in your original message, so I guess you did (and so must have I). Slow morning, forgive me :)

[Adomas Baliuka]

Any progress on the second derivative test? Unless I'm missing something, it's still not in Mathlib, right?

[Bjørn Kjos-Hanssen]

@Adomas Baliuka Correct. I can send in the first derivative test as a first step. Are you thinking of working on the 2nd derivative test?

[Adomas Baliuka]

I certainly won't work on 2nd derivative test this week. Maybe I could look at it next week but I'm not sure how big a project that is (and what generality one would have to state this at; The application I wanted to have it for was just Real -> Real).

I guess the first step would be to merge the first derivative test. Actually, I'm not even sure what "first derivative test" means exactly. Is it (informally, for Real -> Real at lest) "first derivative changes sign at x"-> "x is extremal point"?

Second derivative test would be (I assume) f' x = 0 -> f'' x > 0 -> "local minimum at x" (and analogous thing for f'' > 0)?

[Bjørn Kjos-Hanssen]

Adomas Baliuka said:

I guess the first step would be to merge the first derivative test. Actually, I'm not even sure what "first derivative test" means exactly. Is it (informally, for Real -> Real at lest) "first derivative changes sign at x"-> "x is extremal point"?

I have a couple of different statements depending on whether you have bounded intervals or not. For example:

lemma first_derivative_test {f : ℝ → ℝ} (h : Continuous f) {a b c:ℝ}
  {g₀ : a < b} {g₁ : b < c}
  (h₀ :  ∀ x ∈ interior (Set.Icc a b), 0 < deriv f x)
  (h₁ :  ∀ x ∈ interior (Set.Icc b c), deriv f x < 0)
  : IsLocalMax f b

This one "works" in the sense that I can use it to prove IsLocalMax Real.sin (Real.pi/2) by invoking apply first_derivative_test.

[David Loeffler]

If you're willing to assume the second derivative exists, and is positive, on some interval around x, then you should be able to show that f' x = 0 implies x is a local minimum by combining 2 things that are already in mathlib:

• docs#strictConvexOn_of_deriv2_pos to show that f is strictly convex on an interval around x
• docs#StrictConvexOn.deriv_lt_slope and its mirror-image docs#StrictConvexOn.slope_lt_deriv to show that f y > f x for y slightly less than, resp. greater than, x.

[Bjørn Kjos-Hanssen]

@David Loeffler Thanks, that looks like a quick way. And if we're not willing to assume all that then Wikipedia's proof is rather short (although it does involve ε's).

[Bjørn Kjos-Hanssen]

I submitted a PR now with this result (and the corresponding one for minima):

lemma first_derivative_test_max {f : ℝ → ℝ} {a b c : ℝ}
    (g₀ : a < b) (g₁ : b < c)
    (h : ContinuousAt f b)
    (hd₀ : DifferentiableOn ℝ f (Set.Ioo a b))
    (hd₁ : DifferentiableOn ℝ f (Set.Ioo b c))
    (h₀ :  ∀ x ∈ Set.Ioo a b, 0 ≤ deriv f x)
    (h₁ :  ∀ x ∈ Set.Ioo b c, deriv f x ≤ 0)
    : IsLocalMax f b

which matches the statement on Wikipedia.

[Adomas Baliuka]

This is the PR: https://github.com/leanprover-community/mathlib4/pull/16351

[Patrick Massot]

Nice! I took a look at the first two lemmas. You are making proofs more complicated than they need to be. The first lemma can be proven by hd₀.differentiableAt <| Ioo_mem_nhds hab.1 hab.2 which is short enough to be inlined in the proof of the second lemma which could be

  fun _ hx ↦ (Ioo_union_right g₀ ▸ hx).elim
     (fun hx ↦ (hd₀.differentiableAt <| Ioo_mem_nhds hx.1 hx.2).continuousAt.continuousWithinAt)
     (fun hx ↦ mem_singleton_iff.1 hx ▸ h.continuousWithinAt)

(after opening the Set namespace).

[Patrick Massot]

More seriously, I think those lemmas are too specialized, it would be nice to have more generic versions, at least involving the union of an open set and another set instead of the special case $(a, b] = (a, b) \cup \{b\}$.

[Patrick Massot]

If you want to study the short proof above then it will probably help to start with the following expanded version:

by
  intro x hx
  rw [← Ioo_union_right g₀] at hx
  rcases hx with hx | hx
  · exact (hd₀.differentiableAt <| Ioo_mem_nhds hx.1 hx.2).continuousAt.continuousWithinAt
  · rw [mem_singleton_iff] at hx
    rw [hx]
    exact h.continuousWithinAt

[Bjørn Kjos-Hanssen]

Thanks @Patrick Massot for the feedback! So similarly the third lemma is proved by

      fun _ hx ↦ (Ioo_union_left g₁ ▸ hx).elim
     (fun hx ↦ (hd₁.differentiableAt <| Ioo_mem_nhds hx.1 hx.2).continuousAt.continuousWithinAt)
     (fun hx ↦ mem_singleton_iff.1 hx ▸ h.continuousWithinAt)

Regarding the more generic version, do you have a specific statement in mind?

[Bjørn Kjos-Hanssen]

Here's a proof of the fourth lemma in your style:

theorem differentiableOn_neg_Ioo
  {f : ℝ → ℝ} {s : Set ℝ} (hd₀ : DifferentiableOn ℝ f s) :
    DifferentiableOn ℝ (-f) s :=
    (show -f = ((fun x => -x) ∘ (fun x => f x)) by rfl) ▸ (DifferentiableOn.comp (differentiableOn_neg Set.univ) hd₀)
    (fun _ _ ↦ trivial)

[Patrick Massot]

I’m sorry I’ve been very today, so I didn’t have time to follow up. I’m happy to see you are having fun with proof terms and the rewriting triangle. Note that one you have a proof term you almost never need a show in front. You can compress your last proof to (differentiableOn_neg univ).comp hd₀ fun _ _ ↦ trivial.

[Patrick Massot]

Understanding this kind of proof style is useful and fun, but the next thing I want to say is more important. In isLocalMax_of_mono_anti, you are fighting against the library. It is written in the language of filters you are probably not familiar with (I certainly wasn’t when I started playing this game). So you unfold definitions and apply lemmas translating to more familiar grounds. But in the long run you will have a lot more fun if you learn this new language. Hopefully the topology chapter of MIL could help.

[Patrick Massot]

In this specific case you can write

open Filter

lemma isLocalMax_of_mono_anti
  {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α]
    {β : Type v} [Preorder β]
    {a b c : α} (g₀ : a < b) (g₁ : b < c)
    {f : α → β}
    (h₀ : MonotoneOn f (Set.Ioc a b))
    (h₁ : AntitoneOn f (Set.Ico b c)) : IsLocalMax f b := by
  apply mem_of_superset (Ioo_mem_nhds g₀ g₁)
  intro x hx
  rcases le_total x b with hx' | hx' <;> aesop

[Patrick Massot]

(and you could merge the first two lines if you are really enthusiastic about code golf).

[Patrick Massot]

Let me translate this. By definition, the statement says: the set of points {x | f x ≤ f b} is a neighborhood of b. The term Ioo_mem g₀ g₁ says Ioo a c is a neighborhood of b. And, crucially, docs#Filter.mem_of_superset says, in the particular case of the filter of neighborhoods of b that any set that contains a neighborhood of b is a neighborhood of b. So after this line you only need to prove that Ioo a c is contained in {x | f x ≤ f b}`. The required idea is to split the discussion using docs#le_total. Then automation takes over in both cases.

[Patrick Massot]

Of course you can also go over the board with the full proof being

  mem_of_superset (Ioo_mem_nhds g₀ g₁) fun x _ ↦ by apply (le_total x b).elim  <;> aesop

[Bjørn Kjos-Hanssen]

That's a great proof of isLocalMax_of_mono_anti. Verbatim the same proof proves the IsLocalMin version as well.
And thanks for MIL which indeed explains very well why filters.

[Bjørn Kjos-Hanssen]

Update --- the First Derivative Test is now in Mathlib
Thanks to @Patrick Massot and @Floris van Doorn for the help.

I have also written a proof of the Second Derivative Test in the following surprisingly(?) clean form:

/-- The Second-Derivative Test from calculus. -/
theorem isLocalMin_of_deriv_deriv_pos {f : ℝ → ℝ}  {x₀ : ℝ}
    (hf : deriv (deriv f) x₀ > 0) (hd : deriv f x₀ = 0)
    (hc : ContinuousAt f x₀) : IsLocalMin f x₀

Is the assumption hc needed?

Spoiler

Yes it is needed because
this function

$$f(x)=x^2, x<0 \text{ and } x^2+1, x \ge 0$$

has ∀ x, deriv f x = 2 * x and hence deriv (deriv f) 0 > 0 and deriv f 0 = 0.

I made a #18266
with the comment that it is only a first draft and still needs to be optimized and reduced in size.

[Yaël Dillies]

(don't write PR#18266, write #18266, else your link will pointing to PR number 18266 on the repository called PR, which doesn't exist)

[Johan Commelin]

maybe we should rename mathlib to PR then?

[Yaël Dillies]

Actually Bhavik and I have a project that should be called PR, or maybe PRPR :grinning:

[Ruben Van de Velde]

@Johannes Riesterer

[Bjørn Kjos-Hanssen]

Thoughts about #18266?

[Jireh Loreaux]

I've left some comments, but probably I'll have a bunch more when I can sit down at a computer.

But is there a reason we're doing only the single variable version of this? Was there a discussion already about that which I missed?

[Bjørn Kjos-Hanssen]

Thanks for the comments!
I think multivariable versions would be harder to prove. Recent thread about it
I suppose the single-variable version could be deleted if/when somebody generalizes it?

[Jireh Loreaux]

Okay, @Bjørn Kjos-Hanssen ☀️ , after having a more thorough look just now, I think there are a plethora of issues:

1. Many of the lemmas have an extra deriv in them which is totally unnecessary. (e.g., deriv_pos_of_lt_of_slope_pos, deriv_neg_of_gt_of_slope_pos, deriv_neg_of_deriv_deriv_pos, deriv_pos_of_deriv_deriv_pos)
2. you keep going to intervals, but you really want to continue working with neighborhood filters.
3. It's handy to use docs#SignType.sign or docs#Real.sign to indicate sign changes on either side of x₀.
4. The main theorem should be proven using docs#isLocalMin_of_deriv

So, I suggest you mostly scrap what's there. And instead take these results:

lemma pos_of_slope_pos {b : ℝ} (hb : x₀ < b) (hbf : 0 < slope f x₀ b)
    (hf : f x₀ = 0) : 0 < f b := by
  simp_all [slope, hf]

lemma neg_of_slope_neg {b : ℝ} (hb : b < x₀) (hbf : 0 < slope f x₀ b)
    (hf : f x₀ = 0) : f b < 0 := by
  simp_all [slope]
  exact neg_of_mul_pos_right hbf <| le_of_lt <| inv_lt_zero.mpr <| by linarith

open SignType in
lemma eventually_nhdsWithin_sign_eq_of_deriv_pos (hf : deriv f x₀ > 0) (hx : f x₀ = 0) :
    ∀ᶠ x in 𝓝 x₀, sign (f x) = sign (x - x₀) := by
  rw [← nhdsWithin_compl_singleton_sup_pure x₀, eventually_sup]
  refine ⟨?_, by simpa⟩
  have h_tendsto := hasDerivAt_iff_tendsto_slope.mp
    (differentiableAt_of_deriv_ne_zero <| ne_of_gt hf).hasDerivAt
  filter_upwards [(h_tendsto.eventually <| eventually_gt_nhds hf),
    self_mem_nhdsWithin] with x hx₀ hx₁
  rw [mem_compl_iff, mem_singleton_iff, ← Ne.eq_def] at hx₁
  obtain (hx' | hx') := hx₁.lt_or_lt
  · rw [sign_neg (neg_of_slope_pos hx' hx₀ hx), sign_neg (sub_neg.mpr hx')]
  · rw [sign_pos (pos_of_slope_pos hx' hx₀ hx), sign_pos (sub_pos.mpr hx')]

This should allow you to easily prove the second derivative test using docs#isLocalMin_of_deriv (especially if you rewrite that lemma to take the sign version as a hypothesis, instead of the two separate pieces; although it would probably be good to provide a rewrite lemma to go between the two also).

[Jireh Loreaux]

Of course, you'll want to have the symmetric variants of these results also.

[Jireh Loreaux]

Does this line of attack make sense to you?

[Jireh Loreaux]

Another option instead of sign would be to say that the product is positive. Same can go (with nonnegativity) for the first derivative test.

[Bjørn Kjos-Hanssen]

Thanks @Jireh Loreaux , yes it's hard to shake the habit of thinking in terms of intervals rather than filters :embarrassed: Good point about the extra deriv's, too.

[Bjørn Kjos-Hanssen]

I've fixed all that and switched to using filters throughout with no more Ioo in #18266. @Jireh Loreaux, thanks again for suggestions and help!