1. Analysis
  2. 10.2. Local maxima, local minima, and derivatives
Imports
import Mathlib.Tactic import Analysis.Section_9_6

Analysis I, Section 10.2: Local maxima, local minima, and derivatives

I have attempted to make the translation as faithful a paraphrasing as possible of the original text. When there is a choice between a more idiomatic Lean solution and a more faithful translation, I have generally chosen the latter. In particular, there will be places where the Lean code could be "golfed" to be more elegant and idiomatic, but I have consciously avoided doing so.

Main constructions and results of this section:

  • Relation between local extrema and derivatives.

  • Rolle's theorem.

  • mean value theorem.

open Chapter9namespace Chapter10

Definition 10.2.1 (Local maxima and minima). Here we use Mathlib's IsLocalMaxOn type.

theorem IsLocalMaxOn.iff (X:Set ℝ) (f:ℝ → ℝ) (x₀:ℝ) : IsLocalMaxOn f X x₀ ↔ ∃ δ > 0, IsMaxOn f (X ∩ .Ioo (x₀ - δ) (x₀ + δ)) x₀ := X:Set ℝf:ℝ → ℝx₀:ℝ⊢ IsLocalMaxOn f X x₀ ↔ ∃ δ > 0, IsMaxOn f (X ∩ Set.Ioo (x₀ - δ) (x₀ + δ)) x₀ X:Set ℝf:ℝ → ℝx₀:ℝ⊢ (∃ ε, 0 < ε ∧ ∀ ⦃y : ℝ⦄, y - x₀ < ε → x₀ - y < ε → y ∈ X → f y ≤ f x₀) ↔ ∃ δ, 0 < δ ∧ ∀ x ∈ X, x₀ - δ < x → x < x₀ + δ → f x ≤ f x₀ X:Set ℝf:ℝ → ℝx₀:ℝa✝²:ℝa✝¹:0 < a✝²a✝:ℝ⊢ a✝ - x₀ < a✝² → x₀ - a✝ < a✝² → a✝ ∈ X → f a✝ ≤ f x₀ ↔ a✝ ∈ X → x₀ - a✝² < a✝ → a✝ < x₀ + a✝² → f a✝ ≤ f x₀; X:Set ℝf:ℝ → ℝx₀:ℝa✝²:ℝa✝¹:0 < a✝²a✝:ℝ⊢ (a✝ - x₀ < a✝² → x₀ - a✝ < a✝² → a✝ ∈ X → f a✝ ≤ f x₀) → a✝ ∈ X → x₀ - a✝² < a✝ → a✝ < x₀ + a✝² → f a✝ ≤ f x₀X:Set ℝf:ℝ → ℝx₀:ℝa✝²:ℝa✝¹:0 < a✝²a✝:ℝ⊢ (a✝ ∈ X → x₀ - a✝² < a✝ → a✝ < x₀ + a✝² → f a✝ ≤ f x₀) → a✝ - x₀ < a✝² → x₀ - a✝ < a✝² → a✝ ∈ X → f a✝ ≤ f x₀ X:Set ℝf:ℝ → ℝx₀:ℝa✝²:ℝa✝¹:0 < a✝²a✝:ℝ⊢ (a✝ - x₀ < a✝² → x₀ - a✝ < a✝² → a✝ ∈ X → f a✝ ≤ f x₀) → a✝ ∈ X → x₀ - a✝² < a✝ → a✝ < x₀ + a✝² → f a✝ ≤ f x₀X:Set ℝf:ℝ → ℝx₀:ℝa✝²:ℝa✝¹:0 < a✝²a✝:ℝ⊢ (a✝ ∈ X → x₀ - a✝² < a✝ → a✝ < x₀ + a✝² → f a✝ ≤ f x₀) → a✝ - x₀ < a✝² → x₀ - a✝ < a✝² → a✝ ∈ X → f a✝ ≤ f x₀ intro h X:Set ℝf:ℝ → ℝx₀:ℝa✝³:ℝa✝²:0 < a✝²a✝¹:ℝh:a✝¹ ∈ X → x₀ - a✝³ < a✝¹ → a✝¹ < x₀ + a✝³ → f a✝¹ ≤ f x₀a✝:a✝¹ - x₀ < a✝³⊢ x₀ - a✝¹ < a✝³ → a✝¹ ∈ X → f a✝¹ ≤ f x₀ X:Set ℝf:ℝ → ℝx₀:ℝa✝⁴:ℝa✝³:0 < a✝²a✝²:ℝh:a✝¹ ∈ X → x₀ - a✝³ < a✝¹ → a✝¹ < x₀ + a✝³ → f a✝¹ ≤ f x₀a✝¹:a✝¹ - x₀ < a✝³a✝:x₀ - a✝² < a✝⁴⊢ a✝² ∈ X → f a✝² ≤ f x₀ X:Set ℝf:ℝ → ℝx₀:ℝa✝⁵:ℝa✝⁴:0 < a✝²a✝³:ℝh:a✝¹ ∈ X → x₀ - a✝³ < a✝¹ → a✝¹ < x₀ + a✝³ → f a✝¹ ≤ f x₀a✝²:a✝¹ - x₀ < a✝³a✝¹:x₀ - a✝² < a✝⁴a✝:a✝³ ∈ X⊢ f a✝³ ≤ f x₀ X:Set ℝf:ℝ → ℝx₀:ℝa✝⁵:ℝa✝⁴:0 < a✝²a✝³:ℝh:a✝³ - x₀ < a✝⁵ → x₀ - a✝³ < a✝⁵ → a✝³ ∈ X → f a✝³ ≤ f x₀a✝²:a✝³ ∈ Xa✝¹:x₀ - a✝⁵ < a✝³a✝:a✝³ < x₀ + a✝⁵⊢ f a✝³ ≤ f x₀X:Set ℝf:ℝ → ℝx₀:ℝa✝⁵:ℝa✝⁴:0 < a✝²a✝³:ℝh:a✝¹ ∈ X → x₀ - a✝³ < a✝¹ → a✝¹ < x₀ + a✝³ → f a✝¹ ≤ f x₀a✝²:a✝¹ - x₀ < a✝³a✝¹:x₀ - a✝² < a✝⁴a✝:a✝³ ∈ X⊢ f a✝³ ≤ f x₀ X:Set ℝf:ℝ → ℝx₀:ℝa✝⁵:ℝa✝⁴:0 < a✝²a✝³:ℝh:a✝¹ ∈ X → x₀ - a✝³ < a✝¹ → a✝¹ < x₀ + a✝³ → f a✝¹ ≤ f x₀a✝²:a✝¹ - x₀ < a✝³a✝¹:x₀ - a✝² < a✝⁴a✝:a✝³ ∈ X⊢ a✝³ ∈ XX:Set ℝf:ℝ → ℝx₀:ℝa✝⁵:ℝa✝⁴:0 < a✝²a✝³:ℝh:a✝¹ ∈ X → x₀ - a✝³ < a✝¹ → a✝¹ < x₀ + a✝³ → f a✝¹ ≤ f x₀a✝²:a✝¹ - x₀ < a✝³a✝¹:x₀ - a✝² < a✝⁴a✝:a✝³ ∈ X⊢ x₀ - a✝⁵ < a✝³X:Set ℝf:ℝ → ℝx₀:ℝa✝⁵:ℝa✝⁴:0 < a✝²a✝³:ℝh:a✝¹ ∈ X → x₀ - a✝³ < a✝¹ → a✝¹ < x₀ + a✝³ → f a✝¹ ≤ f x₀a✝²:a✝¹ - x₀ < a✝³a✝¹:x₀ - a✝² < a✝⁴a✝:a✝³ ∈ X⊢ a✝³ < x₀ + a✝⁵ X:Set ℝf:ℝ → ℝx₀:ℝa✝⁵:ℝa✝⁴:0 < a✝²a✝³:ℝh:a✝³ - x₀ < a✝⁵ → x₀ - a✝³ < a✝⁵ → a✝³ ∈ X → f a✝³ ≤ f x₀a✝²:a✝³ ∈ Xa✝¹:x₀ - a✝⁵ < a✝³a✝:a✝³ < x₀ + a✝⁵⊢ a✝¹ - x₀ < a✝³X:Set ℝf:ℝ → ℝx₀:ℝa✝⁵:ℝa✝⁴:0 < a✝²a✝³:ℝh:a✝³ - x₀ < a✝⁵ → x₀ - a✝³ < a✝⁵ → a✝³ ∈ X → f a✝³ ≤ f x₀a✝²:a✝³ ∈ Xa✝¹:x₀ - a✝⁵ < a✝³a✝:a✝³ < x₀ + a✝⁵⊢ x₀ - a✝² < a✝⁴X:Set ℝf:ℝ → ℝx₀:ℝa✝⁵:ℝa✝⁴:0 < a✝²a✝³:ℝh:a✝³ - x₀ < a✝⁵ → x₀ - a✝³ < a✝⁵ → a✝³ ∈ X → f a✝³ ≤ f x₀a✝²:a✝³ ∈ Xa✝¹:x₀ - a✝⁵ < a✝³a✝:a✝³ < x₀ + a✝⁵⊢ a✝³ ∈ XX:Set ℝf:ℝ → ℝx₀:ℝa✝⁵:ℝa✝⁴:0 < a✝²a✝³:ℝh:a✝¹ ∈ X → x₀ - a✝³ < a✝¹ → a✝¹ < x₀ + a✝³ → f a✝¹ ≤ f x₀a✝²:a✝¹ - x₀ < a✝³a✝¹:x₀ - a✝² < a✝⁴a✝:a✝³ ∈ X⊢ a✝³ ∈ XX:Set ℝf:ℝ → ℝx₀:ℝa✝⁵:ℝa✝⁴:0 < a✝²a✝³:ℝh:a✝¹ ∈ X → x₀ - a✝³ < a✝¹ → a✝¹ < x₀ + a✝³ → f a✝¹ ≤ f x₀a✝²:a✝¹ - x₀ < a✝³a✝¹:x₀ - a✝² < a✝⁴a✝:a✝³ ∈ X⊢ x₀ - a✝⁵ < a✝³X:Set ℝf:ℝ → ℝx₀:ℝa✝⁵:ℝa✝⁴:0 < a✝²a✝³:ℝh:a✝¹ ∈ X → x₀ - a✝³ < a✝¹ → a✝¹ < x₀ + a✝³ → f a✝¹ ≤ f x₀a✝²:a✝¹ - x₀ < a✝³a✝¹:x₀ - a✝² < a✝⁴a✝:a✝³ ∈ X⊢ a✝³ < x₀ + a✝⁵ All goals completed! 🐙
theorem IsLocalMinOn.iff (X:Set ℝ) (f:ℝ → ℝ) (x₀:ℝ) : IsLocalMinOn f X x₀ ↔ ∃ δ > 0, IsMinOn f (X ∩ .Ioo (x₀ - δ) (x₀ + δ)) x₀ := X:Set ℝf:ℝ → ℝx₀:ℝ⊢ IsLocalMinOn f X x₀ ↔ ∃ δ > 0, IsMinOn f (X ∩ Set.Ioo (x₀ - δ) (x₀ + δ)) x₀ X:Set ℝf:ℝ → ℝx₀:ℝ⊢ (∃ ε, 0 < ε ∧ ∀ ⦃y : ℝ⦄, y - x₀ < ε → x₀ - y < ε → y ∈ X → f x₀ ≤ f y) ↔ ∃ δ, 0 < δ ∧ ∀ x ∈ X, x₀ - δ < x → x < x₀ + δ → f x₀ ≤ f x X:Set ℝf:ℝ → ℝx₀:ℝa✝²:ℝa✝¹:0 < a✝²a✝:ℝ⊢ a✝ - x₀ < a✝² → x₀ - a✝ < a✝² → a✝ ∈ X → f x₀ ≤ f a✝ ↔ a✝ ∈ X → x₀ - a✝² < a✝ → a✝ < x₀ + a✝² → f x₀ ≤ f a✝; X:Set ℝf:ℝ → ℝx₀:ℝa✝²:ℝa✝¹:0 < a✝²a✝:ℝ⊢ (a✝ - x₀ < a✝² → x₀ - a✝ < a✝² → a✝ ∈ X → f x₀ ≤ f a✝) → a✝ ∈ X → x₀ - a✝² < a✝ → a✝ < x₀ + a✝² → f x₀ ≤ f a✝X:Set ℝf:ℝ → ℝx₀:ℝa✝²:ℝa✝¹:0 < a✝²a✝:ℝ⊢ (a✝ ∈ X → x₀ - a✝² < a✝ → a✝ < x₀ + a✝² → f x₀ ≤ f a✝) → a✝ - x₀ < a✝² → x₀ - a✝ < a✝² → a✝ ∈ X → f x₀ ≤ f a✝ X:Set ℝf:ℝ → ℝx₀:ℝa✝²:ℝa✝¹:0 < a✝²a✝:ℝ⊢ (a✝ - x₀ < a✝² → x₀ - a✝ < a✝² → a✝ ∈ X → f x₀ ≤ f a✝) → a✝ ∈ X → x₀ - a✝² < a✝ → a✝ < x₀ + a✝² → f x₀ ≤ f a✝X:Set ℝf:ℝ → ℝx₀:ℝa✝²:ℝa✝¹:0 < a✝²a✝:ℝ⊢ (a✝ ∈ X → x₀ - a✝² < a✝ → a✝ < x₀ + a✝² → f x₀ ≤ f a✝) → a✝ - x₀ < a✝² → x₀ - a✝ < a✝² → a✝ ∈ X → f x₀ ≤ f a✝ intro h X:Set ℝf:ℝ → ℝx₀:ℝa✝³:ℝa✝²:0 < a✝²a✝¹:ℝh:a✝¹ ∈ X → x₀ - a✝³ < a✝¹ → a✝¹ < x₀ + a✝³ → f x₀ ≤ f a✝¹a✝:a✝¹ - x₀ < a✝³⊢ x₀ - a✝¹ < a✝³ → a✝¹ ∈ X → f x₀ ≤ f a✝¹ X:Set ℝf:ℝ → ℝx₀:ℝa✝⁴:ℝa✝³:0 < a✝²a✝²:ℝh:a✝¹ ∈ X → x₀ - a✝³ < a✝¹ → a✝¹ < x₀ + a✝³ → f x₀ ≤ f a✝¹a✝¹:a✝¹ - x₀ < a✝³a✝:x₀ - a✝² < a✝⁴⊢ a✝² ∈ X → f x₀ ≤ f a✝² X:Set ℝf:ℝ → ℝx₀:ℝa✝⁵:ℝa✝⁴:0 < a✝²a✝³:ℝh:a✝¹ ∈ X → x₀ - a✝³ < a✝¹ → a✝¹ < x₀ + a✝³ → f x₀ ≤ f a✝¹a✝²:a✝¹ - x₀ < a✝³a✝¹:x₀ - a✝² < a✝⁴a✝:a✝³ ∈ X⊢ f x₀ ≤ f a✝³ X:Set ℝf:ℝ → ℝx₀:ℝa✝⁵:ℝa✝⁴:0 < a✝²a✝³:ℝh:a✝³ - x₀ < a✝⁵ → x₀ - a✝³ < a✝⁵ → a✝³ ∈ X → f x₀ ≤ f a✝³a✝²:a✝³ ∈ Xa✝¹:x₀ - a✝⁵ < a✝³a✝:a✝³ < x₀ + a✝⁵⊢ f x₀ ≤ f a✝³X:Set ℝf:ℝ → ℝx₀:ℝa✝⁵:ℝa✝⁴:0 < a✝²a✝³:ℝh:a✝¹ ∈ X → x₀ - a✝³ < a✝¹ → a✝¹ < x₀ + a✝³ → f x₀ ≤ f a✝¹a✝²:a✝¹ - x₀ < a✝³a✝¹:x₀ - a✝² < a✝⁴a✝:a✝³ ∈ X⊢ f x₀ ≤ f a✝³ X:Set ℝf:ℝ → ℝx₀:ℝa✝⁵:ℝa✝⁴:0 < a✝²a✝³:ℝh:a✝¹ ∈ X → x₀ - a✝³ < a✝¹ → a✝¹ < x₀ + a✝³ → f x₀ ≤ f a✝¹a✝²:a✝¹ - x₀ < a✝³a✝¹:x₀ - a✝² < a✝⁴a✝:a✝³ ∈ X⊢ a✝³ ∈ XX:Set ℝf:ℝ → ℝx₀:ℝa✝⁵:ℝa✝⁴:0 < a✝²a✝³:ℝh:a✝¹ ∈ X → x₀ - a✝³ < a✝¹ → a✝¹ < x₀ + a✝³ → f x₀ ≤ f a✝¹a✝²:a✝¹ - x₀ < a✝³a✝¹:x₀ - a✝² < a✝⁴a✝:a✝³ ∈ X⊢ x₀ - a✝⁵ < a✝³X:Set ℝf:ℝ → ℝx₀:ℝa✝⁵:ℝa✝⁴:0 < a✝²a✝³:ℝh:a✝¹ ∈ X → x₀ - a✝³ < a✝¹ → a✝¹ < x₀ + a✝³ → f x₀ ≤ f a✝¹a✝²:a✝¹ - x₀ < a✝³a✝¹:x₀ - a✝² < a✝⁴a✝:a✝³ ∈ X⊢ a✝³ < x₀ + a✝⁵ X:Set ℝf:ℝ → ℝx₀:ℝa✝⁵:ℝa✝⁴:0 < a✝²a✝³:ℝh:a✝³ - x₀ < a✝⁵ → x₀ - a✝³ < a✝⁵ → a✝³ ∈ X → f x₀ ≤ f a✝³a✝²:a✝³ ∈ Xa✝¹:x₀ - a✝⁵ < a✝³a✝:a✝³ < x₀ + a✝⁵⊢ a✝¹ - x₀ < a✝³X:Set ℝf:ℝ → ℝx₀:ℝa✝⁵:ℝa✝⁴:0 < a✝²a✝³:ℝh:a✝³ - x₀ < a✝⁵ → x₀ - a✝³ < a✝⁵ → a✝³ ∈ X → f x₀ ≤ f a✝³a✝²:a✝³ ∈ Xa✝¹:x₀ - a✝⁵ < a✝³a✝:a✝³ < x₀ + a✝⁵⊢ x₀ - a✝² < a✝⁴X:Set ℝf:ℝ → ℝx₀:ℝa✝⁵:ℝa✝⁴:0 < a✝²a✝³:ℝh:a✝³ - x₀ < a✝⁵ → x₀ - a✝³ < a✝⁵ → a✝³ ∈ X → f x₀ ≤ f a✝³a✝²:a✝³ ∈ Xa✝¹:x₀ - a✝⁵ < a✝³a✝:a✝³ < x₀ + a✝⁵⊢ a✝³ ∈ XX:Set ℝf:ℝ → ℝx₀:ℝa✝⁵:ℝa✝⁴:0 < a✝²a✝³:ℝh:a✝¹ ∈ X → x₀ - a✝³ < a✝¹ → a✝¹ < x₀ + a✝³ → f x₀ ≤ f a✝¹a✝²:a✝¹ - x₀ < a✝³a✝¹:x₀ - a✝² < a✝⁴a✝:a✝³ ∈ X⊢ a✝³ ∈ XX:Set ℝf:ℝ → ℝx₀:ℝa✝⁵:ℝa✝⁴:0 < a✝²a✝³:ℝh:a✝¹ ∈ X → x₀ - a✝³ < a✝¹ → a✝¹ < x₀ + a✝³ → f x₀ ≤ f a✝¹a✝²:a✝¹ - x₀ < a✝³a✝¹:x₀ - a✝² < a✝⁴a✝:a✝³ ∈ X⊢ x₀ - a✝⁵ < a✝³X:Set ℝf:ℝ → ℝx₀:ℝa✝⁵:ℝa✝⁴:0 < a✝²a✝³:ℝh:a✝¹ ∈ X → x₀ - a✝³ < a✝¹ → a✝¹ < x₀ + a✝³ → f x₀ ≤ f a✝¹a✝²:a✝¹ - x₀ < a✝³a✝¹:x₀ - a✝² < a✝⁴a✝:a✝³ ∈ X⊢ a✝³ < x₀ + a✝⁵ All goals completed! 🐙

Example 10.2.3

abbrev f_10_2_3 : ℝ → ℝ := fun x ↦ x^2 - x^4
declaration uses `sorry`example : ¬ IsMinOn f_10_2_3 .univ 0 := ⊢ ¬IsMinOn f_10_2_3 Set.univ 0 All goals completed! 🐙declaration uses `sorry`example : IsMinOn f_10_2_3 (.Ioo (-1) 1) 0 := ⊢ IsMinOn f_10_2_3 (Set.Ioo (-1) 1) 0 All goals completed! 🐙declaration uses `sorry`example : IsLocalMinOn f_10_2_3 .univ 0 := ⊢ IsLocalMinOn f_10_2_3 Set.univ 0 All goals completed! 🐙/-- Example 10.2.4 -/ declaration uses `sorry`example : ¬ ∃ x, IsMaxOn (· : ℝ → ℝ) ((↑· : ℤ → ℝ) '' .univ) x := ⊢ ¬∃ x, IsMaxOn (fun x ↦ x) ((fun x ↦ ↑x) '' Set.univ) x All goals completed! 🐙declaration uses `sorry`example : ¬ ∃ x, IsMinOn (· : ℝ → ℝ) ((↑· : ℤ → ℝ) '' .univ) x := ⊢ ¬∃ x, IsMinOn (fun x ↦ x) ((fun x ↦ ↑x) '' Set.univ) x All goals completed! 🐙declaration uses `sorry`example (n:ℤ) : IsLocalMaxOn (· : ℝ → ℝ) ((↑· : ℤ → ℝ) '' .univ) n := n:ℤ⊢ IsLocalMaxOn (fun x ↦ x) ((fun x ↦ ↑x) '' Set.univ) ↑n All goals completed! 🐙declaration uses `sorry`example (n:ℤ) : IsLocalMinOn (· : ℝ → ℝ) ((↑· : ℤ → ℝ) '' .univ) n := n:ℤ⊢ IsLocalMinOn (fun x ↦ x) ((fun x ↦ ↑x) '' Set.univ) ↑n All goals completed! 🐙

Remark 10.2.5

theorem declaration uses `sorry`IsLocalMaxOn.of_restrict {X Y:Set ℝ} (hXY: Y ⊆ X) (f:ℝ → ℝ) (x₀:ℝ) (h: IsLocalMaxOn f X x₀) : IsLocalMaxOn f Y x₀ := X:Set ℝY:Set ℝhXY:Y ⊆ Xf:ℝ → ℝx₀:ℝh:IsLocalMaxOn f X x₀⊢ IsLocalMaxOn f Y x₀ All goals completed! 🐙
theorem declaration uses `sorry`IsLocalMinOn.of_restrict {X Y:Set ℝ} (hXY: Y ⊆ X) (f:ℝ → ℝ) (x₀:ℝ) (h: IsLocalMinOn f X x₀) : IsLocalMinOn f Y x₀ := X:Set ℝY:Set ℝhXY:Y ⊆ Xf:ℝ → ℝx₀:ℝh:IsLocalMinOn f X x₀⊢ IsLocalMinOn f Y x₀ All goals completed! 🐙

Proposition 10.2.6 (i) (Local extrema are stationary) / Exercise 10.2.1

theorem declaration uses `sorry`IsLocalMaxOn.deriv_eq_zero {a b:ℝ} {f:ℝ → ℝ} {x₀:ℝ} (hx₀: x₀ ∈ Set.Ioo a b) (h: IsLocalMaxOn f (.Ioo a b) x₀) {L:ℝ} (hderiv: HasDerivWithinAt f L (.Ioo a b) x₀) : L = 0 := a:ℝb:ℝf:ℝ → ℝx₀:ℝhx₀:x₀ ∈ Set.Ioo a bh:IsLocalMaxOn f (Set.Ioo a b) x₀L:ℝhderiv:HasDerivWithinAt f L (Set.Ioo a b) x₀⊢ L = 0 All goals completed! 🐙

Proposition 10.2.6 (ii) (Local extrema are stationary) / Exercise 10.2.1

theorem declaration uses `sorry`IsLocalMinOn.deriv_eq_zero {a b:ℝ} {f:ℝ → ℝ} {x₀:ℝ} (hx₀: x₀ ∈ Set.Ioo a b) (h: IsLocalMinOn f (.Ioo a b) x₀) {L:ℝ} (hderiv: HasDerivWithinAt f L (.Ioo a b) x₀) : L = 0 := a:ℝb:ℝf:ℝ → ℝx₀:ℝhx₀:x₀ ∈ Set.Ioo a bh:IsLocalMinOn f (Set.Ioo a b) x₀L:ℝhderiv:HasDerivWithinAt f L (Set.Ioo a b) x₀⊢ L = 0 All goals completed! 🐙
theorem declaration uses `sorry`IsMaxOn.deriv_eq_zero_counter : ∃ (a b:ℝ) (f:ℝ → ℝ) (x₀:ℝ) (hx₀: x₀ ∈ Set.Icc a b) (h: IsMaxOn f (.Icc a b) x₀) (L:ℝ) (hderiv: HasDerivWithinAt f L (.Icc a b) x₀), L ≠ 0 := ⊢ ∃ a b f x₀, ∃ (_ : x₀ ∈ Set.Icc a b) (_ : IsMaxOn f (Set.Icc a b) x₀), ∃ L, ∃ (_ : HasDerivWithinAt f L (Set.Icc a b) x₀), L ≠ 0 All goals completed! 🐙

Theorem 10.2.7 (Rolle's theorem) / Exercise 10.2.4

theorem declaration uses `sorry`_root_.HasDerivWithinAt.exist_zero {a b:ℝ} (hab: a < b) {g:ℝ → ℝ} (hcont: ContinuousOn g (.Icc a b)) (hderiv: DifferentiableOn ℝ g (.Ioo a b)) (hgab: g a = g b) : ∃ x ∈ Set.Ioo a b, HasDerivWithinAt g 0 (.Ioo a b) x := a:ℝb:ℝhab:a < bg:ℝ → ℝhcont:ContinuousOn g (Set.Icc a b)hderiv:DifferentiableOn ℝ g (Set.Ioo a b)hgab:g a = g b⊢ ∃ x ∈ Set.Ioo a b, HasDerivWithinAt g 0 (Set.Ioo a b) x All goals completed! 🐙

Corollary 10.2.9 (Mean value theorem) / Exercise 10.2.5

theorem declaration uses `sorry`_root_.HasDerivWithinAt.mean_value {a b:ℝ} (hab: a < b) {f:ℝ → ℝ} (hcont: ContinuousOn f (.Icc a b)) (hderiv: DifferentiableOn ℝ f (.Ioo a b)) : ∃ x ∈ Set.Ioo a b, HasDerivWithinAt f ((f b - f a) / (b - a)) (.Ioo a b) x := a:ℝb:ℝhab:a < bf:ℝ → ℝhcont:ContinuousOn f (Set.Icc a b)hderiv:DifferentiableOn ℝ f (Set.Ioo a b)⊢ ∃ x ∈ Set.Ioo a b, HasDerivWithinAt f ((f b - f a) / (b - a)) (Set.Ioo a b) x All goals completed! 🐙
/-- Exercise 10.2.2 -/ declaration uses `sorry`example : ∃ f:ℝ → ℝ, ContinuousOn f (.Icc (-1) 1) ∧ IsMaxOn f (.Icc (-1) 1) 0 ∧ ¬ DifferentiableWithinAt ℝ f (.Icc (-1) 1) 0 := ⊢ ∃ f, ContinuousOn f (Set.Icc (-1) 1) ∧ IsMaxOn f (Set.Icc (-1) 1) 0 ∧ ¬DifferentiableWithinAt ℝ f (Set.Icc (-1) 1) 0 All goals completed! 🐙/-- Exercise 10.2.3 -/ declaration uses `sorry`example : ∃ f:ℝ → ℝ, DifferentiableOn ℝ f (.Icc (-1) 1) ∧ HasDerivWithinAt f 0 (.Ioo (-1) 1) 0 ∧ ¬ IsLocalMaxOn f (.Icc (-1) 1) 0 ∧ ¬ IsLocalMinOn f (.Icc (-1) 1) 0 := ⊢ ∃ f, DifferentiableOn ℝ f (Set.Icc (-1) 1) ∧ HasDerivWithinAt f 0 (Set.Ioo (-1) 1) 0 ∧ ¬IsLocalMaxOn f (Set.Icc (-1) 1) 0 ∧ ¬IsLocalMinOn f (Set.Icc (-1) 1) 0 All goals completed! 🐙

Exercise 10.2.6

theorem declaration uses `sorry`lipschitz_bound {M a b:ℝ} (hM: M > 0) (hab: a < b) {f:ℝ → ℝ} (hcont: ContinuousOn f (.Icc a b)) (hderiv: DifferentiableOn ℝ f (.Ioo a b)) (hlip: ∀ x ∈ Set.Ioo a b, |derivWithin f (.Ioo a b) x| ≤ M) {x y:ℝ} (hx: x ∈ Set.Icc a b) (hy: y ∈ Set.Icc a b) : |f x - f y| ≤ M * |x - y| := M:ℝa:ℝb:ℝhM:M > 0hab:a < bf:ℝ → ℝhcont:ContinuousOn f (Set.Icc a b)hderiv:DifferentiableOn ℝ f (Set.Ioo a b)hlip:∀ x ∈ Set.Ioo a b, |derivWithin f (Set.Ioo a b) x| ≤ Mx:ℝy:ℝhx:x ∈ Set.Icc a bhy:y ∈ Set.Icc a b⊢ |f x - f y| ≤ M * |x - y| All goals completed! 🐙

Exercise 10.2.7

theorem declaration uses `sorry`_root_.UniformContinuousOn.of_lipschitz {f:ℝ → ℝ} (hcont: ContinuousOn f .univ) (hderiv: DifferentiableOn ℝ f .univ) (hlip: BddOn (deriv f) .univ) : UniformContinuousOn f (.univ) := f:ℝ → ℝhcont:ContinuousOn f Set.univhderiv:DifferentiableOn ℝ f Set.univhlip:BddOn (deriv f) Set.univ⊢ UniformContinuousOn f Set.univ All goals completed! 🐙
end Chapter10