Аналіз I, Розділ 10.3: Монотонні функції та похідні

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

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

• Взаємозв'язки між монотонністю та диференційністю.

theorem Chapter10.derivative_of_monotone (X : Set ℝ) {x₀ : ℝ} (hx₀ : ClusterPt x₀ (Filter.principal (X \ {x₀}))) {f : ℝ → ℝ} (hmono : Monotone f) (hderiv : DifferentiableWithinAt ℝ f X x₀) : derivWithin f X x₀ ≥ 0

Твердження 10.3.1 / Вправа 10.3.1

theorem Chapter10.derivative_of_antitone (X : Set ℝ) {x₀ : ℝ} (hx₀ : ClusterPt x₀ (Filter.principal (X \ {x₀}))) {f : ℝ → ℝ} (hmono : Antitone f) (hderiv : DifferentiableWithinAt ℝ f X x₀) : derivWithin f X x₀ ≤ 0

theorem Chapter10.strictMono_of_positive_derivative {a b : ℝ} (hab : a < b) {f : ℝ → ℝ} (hderiv : DifferentiableOn ℝ f (Set.Icc a b)) (hpos : ∀ x ∈ Set.Ioo a b, derivWithin f (Set.Icc a b) x > 0) : StrictMonoOn f (Set.Icc a b)

Твердження 10.3.3 / Вправа 10.3.4

theorem Chapter10.strictAnti_of_negative_derivative {a b : ℝ} (hab : a < b) {f : ℝ → ℝ} (hderiv : DifferentiableOn ℝ f (Set.Icc a b)) (hneg : ∀ x ∈ Set.Ioo a b, derivWithin f (Set.Icc a b) x < 0) : StrictAntiOn f (Set.Icc a b)