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

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:

• Relations between monotonicity and differentiability

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)