feat(Topology/Order/Rolle): versions of Rolle's theorem for unbounded intervals

Mathlib/Analysis/Calculus/LocalExtr/Rolle.lean

@@ -33,6 +33,17 @@ We prove four versions of this theorem.
 * `exists_deriv_eq_zero'` relates to `exists_deriv_eq_zero` as `exists_hasDerivAt_eq_zero'`
   relates to `exists_hasDerivAt_eq_zero`.
 
+We also prove versions of Rolle's Theorem for unbounded intervals, where the assumption that `f`
+takes the same value at the endpoints is replaced by the assumption that `f` tends to the same
+limit `l` at both ends of the interval.
+
+* `exists_hasDerivAt_eq_zero_Ioi` and `exists_deriv_eq_zero_Ioi` are versions for the interval
+  $(a, +∞)$: they assume that `f` tends to `l` at `𝓝[>] a` and along `atTop`;
+* `exists_hasDerivAt_eq_zero_Iio` and `exists_deriv_eq_zero_Iio` are versions for the interval
+  $(-∞, b)$: they assume that `f` tends to `l` along `atBot` and at `𝓝[<] b`;
+* `exists_hasDerivAt_eq_zero_of_tendsto` and `exists_deriv_eq_zero_of_tendsto` are versions for
+  the whole real line: they assume that `f` tends to `l` along `atBot` and along `atTop`.
+
 ## References
 
 * [Rolle's Theorem](https://en.wikipedia.org/wiki/Rolle's_theorem);
@@ -83,3 +94,67 @@ theorem exists_deriv_eq_zero' (hab : a < b) (hfa : Tendsto f (𝓝[>] a) (𝓝 l
   · exact exists_hasDerivAt_eq_zero' hab hfa hfb fun x hx => (h x hx).hasDerivAt
   · obtain ⟨c, hc, hcdiff⟩ : ∃ x ∈ Ioo a b, ¬DifferentiableAt ℝ f x := h
     exact ⟨c, hc, deriv_zero_of_not_differentiableAt hcdiff⟩
+
+/-! ### Rolle's Theorem on unbounded intervals -/
+
+/-- **Rolle's Theorem** on the interval $(a, +∞)$, `HasDerivAt` version: if `f` has derivative `f'`
+on `(a, +∞)` and tends to the same limit `l` at `𝓝[>] a` and along `atTop`, then `f' c = 0`
+for some `c ∈ (a, +∞)`. -/
+theorem exists_hasDerivAt_eq_zero_Ioi (hfa : Tendsto f (𝓝[>] a) (𝓝 l))
+    (hftop : Tendsto f atTop (𝓝 l)) (hff' : ∀ x ∈ Ioi a, HasDerivAt f (f' x) x) :
+    ∃ c ∈ Ioi a, f' c = 0 :=
+  let ⟨c, cmem, hc⟩ := exists_isLocalExtr_Ioi_of_tendsto
+    (fun x hx ↦ (hff' x hx).continuousAt.continuousWithinAt) hfa hftop
+  ⟨c, cmem, hc.hasDerivAt_eq_zero <| hff' c cmem⟩
+
+/-- **Rolle's Theorem** on the interval $(a, +∞)$, `deriv` version: if `f` tends to the same limit
+`l` at `𝓝[>] a` and along `atTop`, then `deriv f c = 0` for some `c ∈ (a, +∞)`. This version does
+not require differentiability of `f` because we define `deriv f c = 0` whenever `f` is not
+differentiable at `c`. -/
+theorem exists_deriv_eq_zero_Ioi (hfa : Tendsto f (𝓝[>] a) (𝓝 l))
+    (hftop : Tendsto f atTop (𝓝 l)) : ∃ c ∈ Ioi a, deriv f c = 0 := by
+  by_cases! h : ∀ x ∈ Ioi a, DifferentiableAt ℝ f x
+  · exact exists_hasDerivAt_eq_zero_Ioi hfa hftop fun x hx => (h x hx).hasDerivAt
+  · obtain ⟨c, hc, hcdiff⟩ : ∃ x ∈ Ioi a, ¬DifferentiableAt ℝ f x := h
+    exact ⟨c, hc, deriv_zero_of_not_differentiableAt hcdiff⟩
+
+/-- **Rolle's Theorem** on the interval $(-∞, b)$, `HasDerivAt` version: if `f` has derivative `f'`
+on `(-∞, b)` and tends to the same limit `l` along `atBot` and at `𝓝[<] b`, then `f' c = 0`
+for some `c ∈ (-∞, b)`. -/
+theorem exists_hasDerivAt_eq_zero_Iio (hfbot : Tendsto f atBot (𝓝 l))
+    (hfb : Tendsto f (𝓝[<] b) (𝓝 l)) (hff' : ∀ x ∈ Iio b, HasDerivAt f (f' x) x) :
+    ∃ c ∈ Iio b, f' c = 0 :=
+  let ⟨c, cmem, hc⟩ := exists_isLocalExtr_Iio_of_tendsto
+    (fun x hx ↦ (hff' x hx).continuousAt.continuousWithinAt) hfbot hfb
+  ⟨c, cmem, hc.hasDerivAt_eq_zero <| hff' c cmem⟩
+
+/-- **Rolle's Theorem** on the interval $(-∞, b)$, `deriv` version: if `f` tends to the same limit
+`l` along `atBot` and at `𝓝[<] b`, then `deriv f c = 0` for some `c ∈ (-∞, b)`. This version does
+not require differentiability of `f` because we define `deriv f c = 0` whenever `f` is not
+differentiable at `c`. -/
+theorem exists_deriv_eq_zero_Iio (hfbot : Tendsto f atBot (𝓝 l))
+    (hfb : Tendsto f (𝓝[<] b) (𝓝 l)) : ∃ c ∈ Iio b, deriv f c = 0 := by
+  by_cases! h : ∀ x ∈ Iio b, DifferentiableAt ℝ f x
+  · exact exists_hasDerivAt_eq_zero_Iio hfbot hfb fun x hx => (h x hx).hasDerivAt
+  · obtain ⟨c, hc, hcdiff⟩ : ∃ x ∈ Iio b, ¬DifferentiableAt ℝ f x := h
+    exact ⟨c, hc, deriv_zero_of_not_differentiableAt hcdiff⟩
+
+/-- **Rolle's Theorem** on the whole real line, `HasDerivAt` version: if `f` has derivative `f'`
+everywhere and tends to the same limit `l` along `atBot` and along `atTop`, then `f' c = 0`
+for some `c`. -/
+theorem exists_hasDerivAt_eq_zero_of_tendsto (hfbot : Tendsto f atBot (𝓝 l))
+    (hftop : Tendsto f atTop (𝓝 l)) (hff' : ∀ x, HasDerivAt f (f' x) x) : ∃ c, f' c = 0 :=
+  let ⟨c, hc⟩ := exists_isLocalExtr_of_tendsto
+    (continuous_iff_continuousAt.2 fun x ↦ (hff' x).continuousAt) hfbot hftop
+  ⟨c, hc.hasDerivAt_eq_zero (hff' c)⟩
+
+/-- **Rolle's Theorem** on the whole real line, `deriv` version: if `f` tends to the same limit `l`
+along `atBot` and along `atTop`, then `deriv f c = 0` for some `c`. This version does not require
+differentiability of `f` because we define `deriv f c = 0` whenever `f` is not differentiable
+at `c`. -/
+theorem exists_deriv_eq_zero_of_tendsto (hfbot : Tendsto f atBot (𝓝 l))
+    (hftop : Tendsto f atTop (𝓝 l)) : ∃ c, deriv f c = 0 := by
+  by_cases! h : ∀ x, DifferentiableAt ℝ f x
+  · exact exists_hasDerivAt_eq_zero_of_tendsto hfbot hftop fun x => (h x).hasDerivAt
+  · obtain ⟨c, hcdiff⟩ : ∃ x, ¬DifferentiableAt ℝ f x := h
+    exact ⟨c, deriv_zero_of_not_differentiableAt hcdiff⟩

Mathlib/Topology/Order/Rolle.lean

@@ -15,7 +15,10 @@ public import Mathlib.Topology.Order.T5
 In this file we prove the purely topological part of Rolle's Theorem:
 a function that is continuous on an interval $[a, b]$, $a < b$,
 has a local extremum at a point $x ∈ (a, b)$ provided that $f(a)=f(b)$.
-We also prove several variations of this statement.
+We also prove several variations of this statement,
+including versions for the unbounded intervals $(a, +∞)$, $(-∞, b)$, and $(-∞, +∞)$,
+where the equality of the values at the endpoints is replaced
+by the equality of the limits along `atTop` and `atBot`.
 
 In `Mathlib/Analysis/Calculus/LocalExtr/Rolle` we use these lemmas
 to prove several versions of Rolle's Theorem from calculus.
@@ -84,6 +87,148 @@ lemma exists_isLocalExtr_Ioo_of_tendsto (hab : a < b) (hfc : ContinuousOn f (Ioo
   let ⟨c, cmem, hc⟩ := exists_isExtrOn_Ioo_of_tendsto hab hfc ha hb
   ⟨c, cmem, hc.isLocalExtr <| Ioo_mem_nhds cmem.1 cmem.2⟩
 
+/-!
+### Rolle's Theorem on an unbounded interval
+
+If `f` tends to the same limit `l` at both ends of an interval that is unbounded on one or both
+sides, then `f` has an extremum in the interior of this interval. If `f` is identically equal to
+`l`, then any interior point will do. Otherwise `f` takes a value `f c₀ ≠ l`, and, in the case
+`l < f c₀`, the maximum of `f` on a compact interval `[p, q]` chosen so that `f x < f c₀` outside
+of `[p, q]` is a maximum of `f` on the whole interval, attained at a point of `(p, q)`. The case
+`f c₀ < l` follows by applying this to the order dual of the codomain.
+-/
+
+omit [DenselyOrdered X] in
+/-- Auxiliary lemma for the unbounded versions of Rolle's Theorem: if `f` is continuous on `s`,
+if the interval `[p, q]` is included in `s` and contains a point `c₀`, and if `f x < f c₀` at the
+points of `s` outside of `(p, q)`, then `f` attains a maximum on `s` at a point of `(p, q)`. -/
+private lemma exists_isMaxOn_of_forall_lt {s : Set X} {p q c₀ : X} (hfc : ContinuousOn f s)
+    (hsub : Icc p q ⊆ s) (hc₀ : c₀ ∈ Icc p q) (hlow : ∀ x ∈ s, x ≤ p → f x < f c₀)
+    (hhigh : ∀ x ∈ s, q ≤ x → f x < f c₀) : ∃ c ∈ Ioo p q, IsMaxOn f s c := by
+  have hpq : p ≤ q := hc₀.1.trans hc₀.2
+  obtain ⟨c, hcmem, hcmax⟩ := isCompact_Icc.exists_isMaxOn (nonempty_Icc.2 hpq) (hfc.mono hsub)
+  have hcc₀ : f c₀ ≤ f c := hcmax hc₀
+  have hcp : p < c := hcmem.1.lt_of_ne fun h =>
+    absurd ((h ▸ hlow p (hsub (left_mem_Icc.2 hpq)) le_rfl).trans_le hcc₀) (lt_irrefl _)
+  have hcq : c < q := hcmem.2.lt_of_ne fun h =>
+    absurd ((h ▸ hhigh q (hsub (right_mem_Icc.2 hpq)) le_rfl).trans_le hcc₀) (lt_irrefl _)
+  refine ⟨c, ⟨hcp, hcq⟩, fun x hx => ?_⟩
+  rcases le_or_gt x p with hxp | hpx
+  · exact ((hlow x hx hxp).trans_le hcc₀).le
+  · rcases le_or_gt q x with hqx | hxq
+    · exact ((hhigh x hx hqx).trans_le hcc₀).le
+    · exact hcmax ⟨hpx.le, hxq.le⟩
+
+/-- If `f` is continuous on `(a, +∞)`, tends to `l` at `𝓝[>] a` and along `atTop`, and takes at
+some point of `(a, +∞)` a value greater than `l`, then `f` attains a maximum on `(a, +∞)`. -/
+private lemma exists_isMaxOn_Ioi_of_tendsto (hfc : ContinuousOn f (Ioi a))
+    (hfa : Tendsto f (𝓝[>] a) (𝓝 l)) (hftop : Tendsto f atTop (𝓝 l)) {c₀ : X} (hc₀ : a < c₀)
+    (hlt : l < f c₀) : ∃ c ∈ Ioi a, IsMaxOn f (Ioi a) c := by
+  obtain ⟨u, hu, hus⟩ := (mem_nhdsGT_iff_exists_mem_Ioc_Ioo_subset hc₀).1
+    (hfa.eventually (gt_mem_nhds hlt))
+  obtain ⟨p, hap, hpu⟩ := exists_between hu.1
+  obtain ⟨q, hq⟩ := eventually_atTop.1 (hftop.eventually (gt_mem_nhds hlt))
+  have hc₀q : c₀ < q := not_le.1 fun h => absurd (hq c₀ h) (lt_irrefl _)
+  obtain ⟨c, hc, hcmax⟩ := exists_isMaxOn_of_forall_lt (p := p) (q := q) hfc
+    (fun x hx => hap.trans_le hx.1) ⟨(hpu.trans_le hu.2).le, hc₀q.le⟩
+    (fun x hx hxp => hus ⟨hx, hxp.trans_lt hpu⟩) fun x _ hqx => hq x hqx
+  exact ⟨c, hap.trans hc.1, hcmax⟩
+
+/-- If `f` is continuous on `(-∞, b)`, tends to `l` along `atBot` and at `𝓝[<] b`, and takes at
+some point of `(-∞, b)` a value greater than `l`, then `f` attains a maximum on `(-∞, b)`. -/
+private lemma exists_isMaxOn_Iio_of_tendsto (hfc : ContinuousOn f (Iio b))
+    (hfbot : Tendsto f atBot (𝓝 l)) (hfb : Tendsto f (𝓝[<] b) (𝓝 l)) {c₀ : X} (hc₀ : c₀ < b)
+    (hlt : l < f c₀) : ∃ c ∈ Iio b, IsMaxOn f (Iio b) c := by
+  obtain ⟨u, hu, hus⟩ := (mem_nhdsLT_iff_exists_mem_Ico_Ioo_subset hc₀).1
+    (hfb.eventually (gt_mem_nhds hlt))
+  obtain ⟨q, huq, hqb⟩ := exists_between hu.2
+  obtain ⟨p, hp⟩ := eventually_atBot.1 (hfbot.eventually (gt_mem_nhds hlt))
+  have hpc₀ : p < c₀ := not_le.1 fun h => absurd (hp c₀ h) (lt_irrefl _)
+  obtain ⟨c, hc, hcmax⟩ := exists_isMaxOn_of_forall_lt (p := p) (q := q) hfc
+    (fun x hx => hx.2.trans_lt hqb) ⟨hpc₀.le, (hu.1.trans_lt huq).le⟩
+    (fun x _ hxp => hp x hxp) fun x hx hqx => hus ⟨huq.trans_le hqx, hx⟩
+  exact ⟨c, hc.2.trans hqb, hcmax⟩
+
+omit [DenselyOrdered X] in
+/-- If `f` is continuous, tends to `l` along `atBot` and along `atTop`, and takes somewhere a value
+greater than `l`, then `f` attains a global maximum. -/
+private lemma exists_isMaxOn_univ_of_tendsto (hfc : Continuous f) (hfbot : Tendsto f atBot (𝓝 l))
+    (hftop : Tendsto f atTop (𝓝 l)) {c₀ : X} (hlt : l < f c₀) : ∃ c, IsMaxOn f univ c := by
+  obtain ⟨p, hp⟩ := eventually_atBot.1 (hfbot.eventually (gt_mem_nhds hlt))
+  obtain ⟨q, hq⟩ := eventually_atTop.1 (hftop.eventually (gt_mem_nhds hlt))
+  have hpc₀ : p < c₀ := not_le.1 fun h => absurd (hp c₀ h) (lt_irrefl _)
+  have hc₀q : c₀ < q := not_le.1 fun h => absurd (hq c₀ h) (lt_irrefl _)
+  obtain ⟨c, -, hcmax⟩ := exists_isMaxOn_of_forall_lt (p := p) (q := q) hfc.continuousOn
+    (subset_univ _) ⟨hpc₀.le, hc₀q.le⟩ (fun x _ hxp => hp x hxp) fun x _ hqx => hq x hqx
+  exact ⟨c, hcmax⟩
+
+/-- If a function `f` is continuous on `(a, +∞)` and tends to the same value at `𝓝[>] a` and along
+`atTop`, then it has an extremum on `(a, +∞)`. -/
+lemma exists_isExtrOn_Ioi_of_tendsto [NoMaxOrder X] (hfc : ContinuousOn f (Ioi a))
+    (hfa : Tendsto f (𝓝[>] a) (𝓝 l)) (hftop : Tendsto f atTop (𝓝 l)) :
+    ∃ c ∈ Ioi a, IsExtrOn f (Ioi a) c := by
+  by_cases! hconst : ∀ x ∈ Ioi a, f x = l
+  · obtain ⟨c, hc⟩ := exists_gt a
+    exact ⟨c, hc, Or.inl fun x hx => (hconst c hc).trans_le (hconst x hx).ge⟩
+  · obtain ⟨c₀, hc₀, hne⟩ := hconst
+    rcases lt_or_gt_of_ne hne with h | h
+    · exact (exists_isMaxOn_Ioi_of_tendsto (Y := Yᵒᵈ) hfc hfa hftop hc₀ h).imp
+        fun c hc => ⟨hc.1, Or.inl hc.2⟩
+    · exact (exists_isMaxOn_Ioi_of_tendsto hfc hfa hftop hc₀ h).imp
+        fun c hc => ⟨hc.1, Or.inr hc.2⟩
+
+/-- If a function `f` is continuous on `(a, +∞)` and tends to the same value at `𝓝[>] a` and along
+`atTop`, then it has a local extremum on `(a, +∞)`. -/
+lemma exists_isLocalExtr_Ioi_of_tendsto [NoMaxOrder X] (hfc : ContinuousOn f (Ioi a))
+    (hfa : Tendsto f (𝓝[>] a) (𝓝 l)) (hftop : Tendsto f atTop (𝓝 l)) :
+    ∃ c ∈ Ioi a, IsLocalExtr f c :=
+  let ⟨c, cmem, hc⟩ := exists_isExtrOn_Ioi_of_tendsto hfc hfa hftop
+  ⟨c, cmem, hc.isLocalExtr <| Ioi_mem_nhds cmem⟩
+
+/-- If a function `f` is continuous on `(-∞, b)` and tends to the same value along `atBot` and at
+`𝓝[<] b`, then it has an extremum on `(-∞, b)`. -/
+lemma exists_isExtrOn_Iio_of_tendsto [NoMinOrder X] (hfc : ContinuousOn f (Iio b))
+    (hfbot : Tendsto f atBot (𝓝 l)) (hfb : Tendsto f (𝓝[<] b) (𝓝 l)) :
+    ∃ c ∈ Iio b, IsExtrOn f (Iio b) c := by
+  by_cases! hconst : ∀ x ∈ Iio b, f x = l
+  · obtain ⟨c, hc⟩ := exists_lt b
+    exact ⟨c, hc, Or.inl fun x hx => (hconst c hc).trans_le (hconst x hx).ge⟩
+  · obtain ⟨c₀, hc₀, hne⟩ := hconst
+    rcases lt_or_gt_of_ne hne with h | h
+    · exact (exists_isMaxOn_Iio_of_tendsto (Y := Yᵒᵈ) hfc hfbot hfb hc₀ h).imp
+        fun c hc => ⟨hc.1, Or.inl hc.2⟩
+    · exact (exists_isMaxOn_Iio_of_tendsto hfc hfbot hfb hc₀ h).imp
+        fun c hc => ⟨hc.1, Or.inr hc.2⟩
+
+/-- If a function `f` is continuous on `(-∞, b)` and tends to the same value along `atBot` and at
+`𝓝[<] b`, then it has a local extremum on `(-∞, b)`. -/
+lemma exists_isLocalExtr_Iio_of_tendsto [NoMinOrder X] (hfc : ContinuousOn f (Iio b))
+    (hfbot : Tendsto f atBot (𝓝 l)) (hfb : Tendsto f (𝓝[<] b) (𝓝 l)) :
+    ∃ c ∈ Iio b, IsLocalExtr f c :=
+  let ⟨c, cmem, hc⟩ := exists_isExtrOn_Iio_of_tendsto hfc hfbot hfb
+  ⟨c, cmem, hc.isLocalExtr <| Iio_mem_nhds cmem⟩
+
+omit [DenselyOrdered X] in
+/-- If a continuous function `f` tends to the same value along `atBot` and along `atTop`,
+then it has a global extremum. -/
+lemma exists_isExtrOn_univ_of_tendsto [Nonempty X] (hfc : Continuous f)
+    (hfbot : Tendsto f atBot (𝓝 l)) (hftop : Tendsto f atTop (𝓝 l)) :
+    ∃ c, IsExtrOn f univ c := by
+  by_cases! hconst : ∀ x, f x = l
+  · exact ⟨Classical.arbitrary X, Or.inl fun x _ => (hconst _).trans_le (hconst x).ge⟩
+  · obtain ⟨c₀, hne⟩ := hconst
+    rcases lt_or_gt_of_ne hne with h | h
+    · exact (exists_isMaxOn_univ_of_tendsto (Y := Yᵒᵈ) hfc hfbot hftop h).imp fun c hc => Or.inl hc
+    · exact (exists_isMaxOn_univ_of_tendsto hfc hfbot hftop h).imp fun c hc => Or.inr hc
+
+omit [DenselyOrdered X] in
+/-- If a continuous function `f` tends to the same value along `atBot` and along `atTop`,
+then it has a local extremum. -/
+lemma exists_isLocalExtr_of_tendsto [Nonempty X] (hfc : Continuous f)
+    (hfbot : Tendsto f atBot (𝓝 l)) (hftop : Tendsto f atTop (𝓝 l)) : ∃ c, IsLocalExtr f c :=
+  let ⟨c, hc⟩ := exists_isExtrOn_univ_of_tendsto hfc hfbot hftop
+  ⟨c, hc.isLocalExtr univ_mem⟩
+
 /-- A continuous function on an unordered closed interval with `f a = f b`
 takes either its maximum or its minimum value at a point in the interior of the interval. -/
 theorem exists_uIoo_isExtrOn_uIcc (hab : a ≠ b) (hfc : ContinuousOn f (uIcc a b))