Documentation

Analysis.Section_10_2

Аналіз I, Розділ 10.2: Локальні максимуми, локальні мінімуми та похідні #

Я (прим. перекл. Терренс Тао) намагався зробити переклад якомога точнішим перефразуванням оригінального тексту. Коли є вибір між більш ідіоматичним підходом Lean та більш точним перекладом, я зазвичай обирав останній. Зокрема, будуть місця, де код Lean можна було б "підправити", щоб зробити його більш елегантним та ідіоматичним, але я свідомо уникав цього вибору.

Основні конструкції та результати цього розділу:

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

Визначення 10.2.1 (Локальні максимуми та мінімуми). Тут ми використовуємо тип IsLocalMaxOn з Mathlib.

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 :
ℝ → ℝ

Приклад 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₀

    Зауваження 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

    Твердження 10.2.6 (Локальні екстремуми стаціонарні) / Вправа 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

    Твердження 10.2.6 (Local extrema are stationary) / Вправа 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

    Теорема 10.2.7 (Теорема Ролля) / Вправа 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

    Наслідок 10.2.9 (Теорема середнього значення) / Вправа 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|

    Вправа 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

    Вправа 10.2.7