Documentation

Analysis.Section_10_2

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:

source
theorem Chapter10.IsLocalMaxOn.iff (X : Set ℝ) (f : ℝ → ℝ) (x₀ : ℝ) :
IsLocalMaxOn f X x₀ ↔ ∃ δ > 0, IsMaxOn f (X ∩ Set.Ioo (x₀ - δ) (x₀ + δ)) x₀

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

source
theorem Chapter10.IsLocalMinOn.iff (X : Set ℝ) (f : ℝ → ℝ) (x₀ : ℝ) :
IsLocalMinOn f X x₀ ↔ ∃ δ > 0, IsMinOn f (X ∩ Set.Ioo (x₀ - δ) (x₀ + δ)) x₀
source
@[reducible, inline]
abbrev Chapter10.f_10_2_3 :
ℝ → ℝ

Example 10.2.3

Equations
Instances For
    source
    theorem Chapter10.IsLocalMaxOn.of_restrict {X Y : Set ℝ} (hXY : Y ⊆ X) (f : ℝ → ℝ) (x₀ : ℝ) (h : IsLocalMaxOn f X x₀) :
    IsLocalMaxOn f Y x₀

    Remark 10.2.5

    source
    theorem Chapter10.IsLocalMinOn.of_restrict {X Y : Set ℝ} (hXY : Y ⊆ X) (f : ℝ → ℝ) (x₀ : ℝ) (h : IsLocalMinOn f X x₀) :
    IsLocalMinOn f Y x₀
    source
    theorem Chapter10.IsLocalMaxOn.deriv_eq_zero {a b : ℝ} (hab : a < b) {f : ℝ → ℝ} {x₀ : ℝ} (hx₀ : x₀ ∈ Set.Ioo a b) (h : IsLocalMaxOn f (Set.Ioo a b) x₀) {L : ℝ} (hderiv : HasDerivWithinAt f L (Set.Ioo a b) x₀) :
    L = 0

    Proposition 10.2.6 (Local extrema are stationary) / Exercise 10.2.1

    source
    theorem Chapter10.IsLocalMinOn.deriv_eq_zero {a b : ℝ} (hab : a < b) {f : ℝ → ℝ} {x₀ : ℝ} (hx₀ : x₀ ∈ Set.Ioo a b) (h : IsLocalMinOn f (Set.Ioo a b) x₀) {L : ℝ} (hderiv : HasDerivWithinAt f L (Set.Ioo a b) x₀) :
    L = 0

    Proposition 10.2.6 (Local extrema are stationary) / Exercise 10.2.1

    source
    theorem Chapter10.IsMaxOn.deriv_eq_zero_counter :
    ∃ (a : ℝ) (b : ℝ) (_ : 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
    source
    theorem HasDerivWithinAt.exist_zero {a b : ℝ} (hab : a < b) {g : ℝ → ℝ} (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

    Theorem 10.2.7 (Rolle's theorem) / Exercise 10.2.4

    source
    theorem HasDerivWithinAt.mean_value {a b : ℝ} (hab : a < b) {f : ℝ → ℝ} (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

    Corollary 10.2.9 (Mean value theorem ) / Exercise 10.2.5

    source
    theorem Chapter10.lipschitz_bound {M a b : ℝ} (hM : M > 0) (hab : a < b) {f : ℝ → ℝ} (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| ≤ M) {x y : ℝ} (hx : x ∈ Set.Ioo a b) (hy : y ∈ Set.Ioo a b) :
    |f x - f y| ≤ M * |x - y|

    Exercise 10.2.6

    source
    theorem UniformContinuousOn.of_lipschitz {f : ℝ → ℝ} (hcont : ContinuousOn f Set.univ) (hderiv : DifferentiableOn ℝ f Set.univ) (hlip : Chapter9.BddOn (deriv f) Set.univ) :
    UniformContinuousOn f Set.univ

    Exercise 10.2.7