Аналіз I, Глава 10.2

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

Визначення 10.2.1 (Local maxima and minima). Here we use Mathlib's IsLocalMaxOn.{u, v} {α : Type u} {β : Type v} [TopologicalSpace α] [Preorder β] (f : α → β) (s : Set α) (a : α) : PropIsLocalMaxOn type.

theorem IsLocalMaxOn.iff (X:Set ℝ) (f:ℝ → ℝ) (x₀:ℝ) :
  IsLocalMaxOn f X x₀ ↔
  ∃ δ > 0, IsMaxOn f (X ∩ Set.Ioo (x₀ - δ) (x₀ + δ)) x₀ := byX:Set ℝf:ℝ → ℝx₀:ℝ⊢ IsLocalMaxOn f X x₀ ↔ ∃ δ > 0, IsMaxOn f (X ∩ Set.Ioo (x₀ - δ) (x₀ + δ)) x₀
  simp [isMaxOn_iff, IsLocalMaxOn, IsMaxFilter, nhdsWithin.eq_1, Filter.eventually_inf_principal,
        Metric.eventually_nhds_iff, Real.dist_eq, abs_sub_lt_iff ]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₀
  apply exists_congrhX:Set ℝf:ℝ → ℝx₀:ℝ⊢ ∀ (a : ℝ),
  (0 < a ∧ ∀ ⦃y : ℝ⦄, y - x₀ < a → x₀ - y < a → y ∈ X → f y ≤ f x₀) ↔
    0 < a ∧ ∀ x ∈ X, x₀ - a < x → x < x₀ + a → f x ≤ f x₀; intro εhX: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₀
  apply and_congr_righth.hX:Set ℝf:ℝ → ℝx₀:ℝε:ℝ⊢ 0 < ε → ((∀ ⦃y : ℝ⦄, y - x₀ < ε → x₀ - y < ε → y ∈ X → f y ≤ f x₀) ↔ ∀ x ∈ X, x₀ - ε < x → x < x₀ + ε → f x ≤ f x₀); intro hεh.hX:Set ℝf:ℝ → ℝx₀:ℝε:ℝhε:0 < ε⊢ (∀ ⦃y : ℝ⦄, y - x₀ < ε → x₀ - y < ε → y ∈ X → f y ≤ f x₀) ↔ ∀ x ∈ X, x₀ - ε < x → x < x₀ + ε → f x ≤ f x₀
  apply forall_congr'h.h.hX:Set ℝf:ℝ → ℝx₀:ℝε:ℝhε:0 < ε⊢ ∀ (a : ℝ), a - x₀ < ε → x₀ - a < ε → a ∈ X → f a ≤ f x₀ ↔ a ∈ X → x₀ - ε < a → a < x₀ + ε → f a ≤ f x₀; intro xh.h.hX:Set ℝf:ℝ → ℝx₀:ℝε:ℝhε:0 < εx:ℝ⊢ x - x₀ < ε → x₀ - x < ε → x ∈ X → f x ≤ f x₀ ↔ x ∈ X → x₀ - ε < x → x < x₀ + ε → f x ≤ f x₀
  constructorh.h.h.mpX:Set ℝf:ℝ → ℝx₀:ℝε:ℝhε:0 < εx:ℝ⊢ (x - x₀ < ε → x₀ - x < ε → x ∈ X → f x ≤ f x₀) → x ∈ X → x₀ - ε < x → x < x₀ + ε → f x ≤ f x₀h.h.h.mprX:Set ℝf:ℝ → ℝx₀:ℝε:ℝhε:0 < εx:ℝ⊢ (x ∈ X → x₀ - ε < x → x < x₀ + ε → f x ≤ f x₀) → x - x₀ < ε → x₀ - x < ε → x ∈ X → f x ≤ f x₀
  .h.h.h.mpX:Set ℝf:ℝ → ℝx₀:ℝε:ℝhε:0 < εx:ℝ⊢ (x - x₀ < ε → x₀ - x < ε → x ∈ X → f x ≤ f x₀) → x ∈ X → x₀ - ε < x → x < x₀ + ε → f x ≤ f x₀ intro h hx hxm hxph.h.h.mpX:Set ℝf:ℝ → ℝx₀:ℝε:ℝhε:0 < εx:ℝh:x - x₀ < ε → x₀ - x < ε → x ∈ X → f x ≤ f x₀hx:x ∈ Xhxm:x₀ - ε < xhxp:x < x₀ + ε⊢ f x ≤ f x₀
    exact h (byX:Set ℝf:ℝ → ℝx₀:ℝε:ℝhε:0 < εx:ℝh:x - x₀ < ε → x₀ - x < ε → x ∈ X → f x ≤ f x₀hx:x ∈ Xhxm:x₀ - ε < xhxp:x < x₀ + ε⊢ x - x₀ < ε linarithAll goals completed! 🐙) (byX:Set ℝf:ℝ → ℝx₀:ℝε:ℝhε:0 < εx:ℝh:x - x₀ < ε → x₀ - x < ε → x ∈ X → f x ≤ f x₀hx:x ∈ Xhxm:x₀ - ε < xhxp:x < x₀ + ε⊢ x₀ - x < ε linarithAll goals completed! 🐙) hx
  intro h hxm hxp hxh.h.h.mprX:Set ℝf:ℝ → ℝx₀:ℝε:ℝhε:0 < εx:ℝh:x ∈ X → x₀ - ε < x → x < x₀ + ε → f x ≤ f x₀hxm:x - x₀ < εhxp:x₀ - x < εhx:x ∈ X⊢ f x ≤ f x₀
  exact h hx (byX:Set ℝf:ℝ → ℝx₀:ℝε:ℝhε:0 < εx:ℝh:x ∈ X → x₀ - ε < x → x < x₀ + ε → f x ≤ f x₀hxm:x - x₀ < εhxp:x₀ - x < εhx:x ∈ X⊢ x₀ - ε < x linarithAll goals completed! 🐙) (byX:Set ℝf:ℝ → ℝx₀:ℝε:ℝhε:0 < εx:ℝh:x ∈ X → x₀ - ε < x → x < x₀ + ε → f x ≤ f x₀hxm:x - x₀ < εhxp:x₀ - x < εhx:x ∈ X⊢ x < x₀ + ε linarithAll goals completed! 🐙)

theorem IsLocalMinOn.iff (X:Set ℝ) (f:ℝ → ℝ) (x₀:ℝ) :
  IsLocalMinOn f X x₀ ↔
  ∃ δ > 0, IsMinOn f (X ∩ Set.Ioo (x₀ - δ) (x₀ + δ)) x₀ := byX:Set ℝf:ℝ → ℝx₀:ℝ⊢ IsLocalMinOn f X x₀ ↔ ∃ δ > 0, IsMinOn f (X ∩ Set.Ioo (x₀ - δ) (x₀ + δ)) x₀
  simp [isMinOn_iff, IsLocalMinOn, IsMinFilter, nhdsWithin.eq_1, Filter.eventually_inf_principal,
        Metric.eventually_nhds_iff, Real.dist_eq, abs_sub_lt_iff ]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
  apply exists_congrhX:Set ℝf:ℝ → ℝx₀:ℝ⊢ ∀ (a : ℝ),
  (0 < a ∧ ∀ ⦃y : ℝ⦄, y - x₀ < a → x₀ - y < a → y ∈ X → f x₀ ≤ f y) ↔
    0 < a ∧ ∀ x ∈ X, x₀ - a < x → x < x₀ + a → f x₀ ≤ f x; intro εhX: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
  apply and_congr_righth.hX:Set ℝf:ℝ → ℝx₀:ℝε:ℝ⊢ 0 < ε → ((∀ ⦃y : ℝ⦄, y - x₀ < ε → x₀ - y < ε → y ∈ X → f x₀ ≤ f y) ↔ ∀ x ∈ X, x₀ - ε < x → x < x₀ + ε → f x₀ ≤ f x); intro hεh.hX:Set ℝf:ℝ → ℝx₀:ℝε:ℝhε:0 < ε⊢ (∀ ⦃y : ℝ⦄, y - x₀ < ε → x₀ - y < ε → y ∈ X → f x₀ ≤ f y) ↔ ∀ x ∈ X, x₀ - ε < x → x < x₀ + ε → f x₀ ≤ f x
  apply forall_congr'h.h.hX:Set ℝf:ℝ → ℝx₀:ℝε:ℝhε:0 < ε⊢ ∀ (a : ℝ), a - x₀ < ε → x₀ - a < ε → a ∈ X → f x₀ ≤ f a ↔ a ∈ X → x₀ - ε < a → a < x₀ + ε → f x₀ ≤ f a; intro xh.h.hX:Set ℝf:ℝ → ℝx₀:ℝε:ℝhε:0 < εx:ℝ⊢ x - x₀ < ε → x₀ - x < ε → x ∈ X → f x₀ ≤ f x ↔ x ∈ X → x₀ - ε < x → x < x₀ + ε → f x₀ ≤ f x
  constructorh.h.h.mpX:Set ℝf:ℝ → ℝx₀:ℝε:ℝhε:0 < εx:ℝ⊢ (x - x₀ < ε → x₀ - x < ε → x ∈ X → f x₀ ≤ f x) → x ∈ X → x₀ - ε < x → x < x₀ + ε → f x₀ ≤ f xh.h.h.mprX:Set ℝf:ℝ → ℝx₀:ℝε:ℝhε:0 < εx:ℝ⊢ (x ∈ X → x₀ - ε < x → x < x₀ + ε → f x₀ ≤ f x) → x - x₀ < ε → x₀ - x < ε → x ∈ X → f x₀ ≤ f x
  .h.h.h.mpX:Set ℝf:ℝ → ℝx₀:ℝε:ℝhε:0 < εx:ℝ⊢ (x - x₀ < ε → x₀ - x < ε → x ∈ X → f x₀ ≤ f x) → x ∈ X → x₀ - ε < x → x < x₀ + ε → f x₀ ≤ f x intro h hx hxm hxph.h.h.mpX:Set ℝf:ℝ → ℝx₀:ℝε:ℝhε:0 < εx:ℝh:x - x₀ < ε → x₀ - x < ε → x ∈ X → f x₀ ≤ f xhx:x ∈ Xhxm:x₀ - ε < xhxp:x < x₀ + ε⊢ f x₀ ≤ f x
    exact h (byX:Set ℝf:ℝ → ℝx₀:ℝε:ℝhε:0 < εx:ℝh:x - x₀ < ε → x₀ - x < ε → x ∈ X → f x₀ ≤ f xhx:x ∈ Xhxm:x₀ - ε < xhxp:x < x₀ + ε⊢ x - x₀ < ε linarithAll goals completed! 🐙) (byX:Set ℝf:ℝ → ℝx₀:ℝε:ℝhε:0 < εx:ℝh:x - x₀ < ε → x₀ - x < ε → x ∈ X → f x₀ ≤ f xhx:x ∈ Xhxm:x₀ - ε < xhxp:x < x₀ + ε⊢ x₀ - x < ε linarithAll goals completed! 🐙) hx
  intro h hxm hxp hxh.h.h.mprX:Set ℝf:ℝ → ℝx₀:ℝε:ℝhε:0 < εx:ℝh:x ∈ X → x₀ - ε < x → x < x₀ + ε → f x₀ ≤ f xhxm:x - x₀ < εhxp:x₀ - x < εhx:x ∈ X⊢ f x₀ ≤ f x
  exact h hx (byX:Set ℝf:ℝ → ℝx₀:ℝε:ℝhε:0 < εx:ℝh:x ∈ X → x₀ - ε < x → x < x₀ + ε → f x₀ ≤ f xhxm:x - x₀ < εhxp:x₀ - x < εhx:x ∈ X⊢ x₀ - ε < x linarithAll goals completed! 🐙) (byX:Set ℝf:ℝ → ℝx₀:ℝε:ℝhε:0 < εx:ℝh:x ∈ X → x₀ - ε < x → x < x₀ + ε → f x₀ ≤ f xhxm:x - x₀ < εhxp:x₀ - x < εhx:x ∈ X⊢ x < x₀ + ε linarithAll goals completed! 🐙)

Приклад 10.2.3

abbrev f_10_2_3 : ℝ → ℝ := fun x ↦ x^2 - x^4

declaration uses 'sorry'example : ¬ IsMinOn f_10_2_3 Set.univ 0 := by⊢ ¬IsMinOn f_10_2_3 Set.univ 0 sorryAll goals completed! 🐙

declaration uses 'sorry'example : IsMinOn f_10_2_3 (Set.Ioo (-1) 1) 0 := by⊢ IsMinOn f_10_2_3 (Set.Ioo (-1) 1) 0 sorryAll goals completed! 🐙

declaration uses 'sorry'example : IsLocalMaxOn f_10_2_3 Set.univ 0 := by⊢ IsLocalMaxOn f_10_2_3 Set.univ 0 sorryAll goals completed! 🐙

Приклад 10.2.4

declaration uses 'sorry'example : ¬ ∃ x, IsMaxOn (· : ℝ → ℝ)  ((↑· : ℤ → ℝ) '' Set.univ) x := by⊢ ¬∃ x, IsMaxOn (fun x => x) ((fun x => ↑x) '' Set.univ) x sorryAll goals completed! 🐙

declaration uses 'sorry'example : ¬ ∃ x, IsMinOn (· : ℝ → ℝ)  ((↑· : ℤ → ℝ) '' Set.univ) x := by⊢ ¬∃ x, IsMinOn (fun x => x) ((fun x => ↑x) '' Set.univ) x sorryAll goals completed! 🐙

declaration uses 'sorry'example (n:ℤ) : IsMaxOn (· : ℝ → ℝ)  ((↑· : ℤ → ℝ) '' Set.univ) n := byn:ℤ⊢ IsMaxOn (fun x => x) ((fun x => ↑x) '' Set.univ) ↑n sorryAll goals completed! 🐙

declaration uses 'sorry'example (n:ℤ) : IsMinOn (· : ℝ → ℝ)  ((↑· : ℤ → ℝ) '' Set.univ) n := byn:ℤ⊢ IsMinOn (fun x => x) ((fun x => ↑x) '' Set.univ) ↑n sorryAll goals completed! 🐙

Ремарка 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₀ := byX:Set ℝY:Set ℝhXY:Y ⊆ Xf:ℝ → ℝx₀:ℝh:IsLocalMaxOn f X x₀⊢ IsLocalMaxOn f Y x₀
  sorryAll 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₀ := byX:Set ℝY:Set ℝhXY:Y ⊆ Xf:ℝ → ℝx₀:ℝh:IsLocalMinOn f X x₀⊢ IsLocalMinOn f Y x₀
  sorryAll goals completed! 🐙

Твердження 10.2.6 (Local extrema are stationary) / Вправа 10.2.1

theorem declaration uses 'sorry'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 := bya:ℝb:ℝhab:a < bf:ℝ → ℝ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
  sorryAll goals completed! 🐙

Твердження 10.2.6 (Local extrema are stationary) / Вправа 10.2.1

theorem declaration uses 'sorry'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 := bya:ℝb:ℝhab:a < bf:ℝ → ℝ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
  sorryAll goals completed! 🐙

theorem declaration uses 'sorry'IsMaxOn.deriv_eq_zero_counter : ∃ (a b:ℝ) (hab: a < b) (f:ℝ → ℝ)
  (x₀:ℝ) (hx₀: x₀ ∈ Set.Icc a b) (h: IsMaxOn f (Set.Icc a b) x₀) (L:ℝ)
  (hderiv: HasDerivWithinAt f L (Set.Icc a b) x₀), L ≠ 0 := by⊢ ∃ 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
  sorryAll goals completed! 🐙

Теорема 10.2.7 (Rolle's theorem) / Вправа 10.2.4

theorem declaration uses 'sorry'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 := bya:ℝ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
  sorryAll goals completed! 🐙

Наслідок 10.2.9 (Mean value theorem ) / Вправа 10.2.5

theorem declaration uses 'sorry'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 := bya:ℝ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
  sorryAll goals completed! 🐙

Вправа 10.2.2

declaration uses 'sorry'example : ∃ f:ℝ → ℝ, ContinuousOn f (Set.Icc (-1) 1) ∧
  IsMaxOn f (Set.Icc (-1) 1) 0 ∧ ¬ DifferentiableWithinAt ℝ f (Set.Icc (-1) 1) 0 := by⊢ ∃ f, ContinuousOn f (Set.Icc (-1) 1) ∧ IsMaxOn f (Set.Icc (-1) 1) 0 ∧ ¬DifferentiableWithinAt ℝ f (Set.Icc (-1) 1) 0
  sorryAll goals completed! 🐙

Вправа 10.2.3

declaration uses 'sorry'example : ∃ 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 := by⊢ ∃ 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
  sorryAll goals completed! 🐙

Вправа 10.2.6

theorem declaration uses 'sorry'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| := byM:ℝ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.Ioo a bhy:y ∈ Set.Ioo a b⊢ |f x - f y| ≤ M * |x - y|
  sorryAll goals completed! 🐙

Вправа 10.2.7

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

end Chapter10