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

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:

• API for Mathlib's HasDerivWithinAt, derivWithin, and DifferentiableWithinAt.

Note that the Mathlib conventions differ slightly from that in the text, in that differentiability is defined even at points that are not limit points of the domain; derivatives in such cases may not be unique, but derivWithin still selects one such derivative in such cases (or 0, if no derivative exists).

theorem HasDerivWithinAt.iff (X : Set ℝ) (x₀ : ℝ) (f : ℝ → ℝ) (L : ℝ) : HasDerivWithinAt f L X x₀ ↔ Filter.Tendsto (fun (x : ℝ) => (f x - f x₀) / (x - x₀)) (nhds x₀ ⊓ Filter.principal (X \ {x₀})) (nhds L)

Визначення 10.1.1 (Differentiability at a point). For the Mathlib notion HasDerivWithinAt, the hypothesis that x₀ is a limit point is not needed.

theorem DifferentiableWithinAt.iff (X : Set ℝ) (x₀ : ℝ) (f : ℝ → ℝ) : DifferentiableWithinAt ℝ f X x₀ ↔ ∃ (L : ℝ), HasDerivWithinAt f L X x₀

theorem DifferentiableWithinAt.of_hasDeriv {X : Set ℝ} {x₀ : ℝ} {f : ℝ → ℝ} {L : ℝ} (hL : HasDerivWithinAt f L X x₀) : DifferentiableWithinAt ℝ f X x₀

theorem Chapter10.derivative_unique {X : Set ℝ} {x₀ : ℝ} (hx₀ : ClusterPt x₀ (Filter.principal (X \ {x₀}))) {f : ℝ → ℝ} {L L' : ℝ} (hL : HasDerivWithinAt f L X x₀) (hL' : HasDerivWithinAt f L' X x₀) : L = L'

theorem Chapter10.derivative_unique' (X : Set ℝ) {x₀ : ℝ} (hx₀ : ClusterPt x₀ (Filter.principal (X \ {x₀}))) {f : ℝ → ℝ} {L : ℝ} (hL : HasDerivWithinAt f L X x₀) (hdiff : DifferentiableWithinAt ℝ f X x₀) : L = derivWithin f X x₀

@[reducible, inline]

abbrev Chapter10.f_10_1_6 : ℝ → ℝ

Приклад 10.1.6

Equations

• Chapter10.f_10_1_6 = abs

theorem HasDerivWithinAt.iff_approx_linear (X : Set ℝ) (x₀ : ℝ) (f : ℝ → ℝ) (L : ℝ) : HasDerivWithinAt f L X x₀ ↔ ∀ ε > 0, ∃ δ > 0, ∀ x ∈ X, |x - x₀| < δ → |f x - f x₀ - L * (x - x₀)| ≤ ε * |x - x₀|

Твердження 10.1.7 (Newton's approximation) / Вправа 10.1.2

theorem ContinuousWithinAt.of_differentiableWithinAt {X : Set ℝ} {x₀ : ℝ} {f : ℝ → ℝ} (h : DifferentiableWithinAt ℝ f X x₀) : ContinuousWithinAt f X x₀

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

theorem ContinuousOn.of_differentiableOn {X : Set ℝ} {f : ℝ → ℝ} (h : DifferentiableOn ℝ f X) : ContinuousOn f X

Наслідок 10.1.12

theorem HasDerivWithinAt.of_const (X : Set ℝ) (x₀ c : ℝ) : HasDerivWithinAt (fun (x : ℝ) => c) 0 X x₀

Теорема 10.1.13 (a) (Differential calculus) / Вправа 10.1.4

theorem HasDerivWithinAt.of_id (X : Set ℝ) (x₀ : ℝ) : HasDerivWithinAt (fun (x : ℝ) => x) 1 X x₀

Теорема 10.1.13 (b) (Differential calculus) / Вправа 10.1.4

theorem HasDerivWithinAt.of_add {X : Set ℝ} {x₀ f'x₀ g'x₀ : ℝ} {f g : ℝ → ℝ} (hf : HasDerivWithinAt f f'x₀ X x₀) (hg : HasDerivWithinAt g g'x₀ X x₀) : HasDerivWithinAt (f + g) (f'x₀ + g'x₀) X x₀

Теорема 10.1.13 (c) (Sum rule) / Вправа 10.1.4

theorem HasDerivWithinAt.of_mul {X : Set ℝ} {x₀ f'x₀ g'x₀ : ℝ} {f g : ℝ → ℝ} (hf : HasDerivWithinAt f f'x₀ X x₀) (hg : HasDerivWithinAt g g'x₀ X x₀) : HasDerivWithinAt (f * g) (f'x₀ * g x₀ + f x₀ * g'x₀) X x₀

Теорема 10.1.13 (d) (Product rule) / Вправа 10.1.4

theorem HasDerivWithinAt.of_smul {X : Set ℝ} {x₀ f'x₀ : ℝ} (c : ℝ) {f : ℝ → ℝ} (hf : HasDerivWithinAt f f'x₀ X x₀) : HasDerivWithinAt (c • f) (c * f'x₀) X x₀

Теорема 10.1.13 (e) (Differential calculus) / Вправа 10.1.4

theorem HasDerivWithinAt.of_sub {X : Set ℝ} {x₀ f'x₀ g'x₀ : ℝ} {f g : ℝ → ℝ} (hf : HasDerivWithinAt f f'x₀ X x₀) (hg : HasDerivWithinAt g g'x₀ X x₀) : HasDerivWithinAt (f - g) (f'x₀ - g'x₀) X x₀

Теорема 10.1.13 (f) (Difference rule) / Вправа 10.1.4

theorem HasDerivWithinAt.of_inv {X : Set ℝ} {x₀ g'x₀ : ℝ} {g : ℝ → ℝ} (hgx₀ : g x₀ ≠ 0) (hg : HasDerivWithinAt g g'x₀ X x₀) : HasDerivWithinAt (1 / g) (-g'x₀ / g x₀ ^ 2) X x₀

Теорема 10.1.13 (g) (Differential calculus) / Вправа 10.1.4

theorem HasDerivWithinAt.of_div {X : Set ℝ} {x₀ f'x₀ g'x₀ : ℝ} {f g : ℝ → ℝ} (hgx₀ : g x₀ ≠ 0) (hf : HasDerivWithinAt f f'x₀ X x₀) (hg : HasDerivWithinAt g g'x₀ X x₀) : HasDerivWithinAt (f / g) ((f'x₀ * g x₀ - f x₀ * g'x₀) / g x₀ ^ 2) X x₀

Теорема 10.1.13 (h) (Quotient rule) / Вправа 10.1.4

theorem HasDerivWithinAt.of_comp {X Y : Set ℝ} {x₀ y₀ f'x₀ g'y₀ : ℝ} {f g : ℝ → ℝ} (hfx₀ : f x₀ = y₀) (hfX : ∀ x ∈ X, f x ∈ Y) (hf : HasDerivWithinAt f f'x₀ X x₀) (hg : HasDerivWithinAt g g'y₀ Y y₀) : HasDerivWithinAt (g ∘ f) (g'y₀ * f'x₀) X x₀

Теорема 10.1.15 (Chain rule) / Вправа 10.1.7

theorem HasDerivWithinAt.of_pow (n : ℕ) (x₀ : ℝ) : HasDerivWithinAt (fun (x : ℝ) => x ^ n) (↑n * x₀ ^ (↑n - 1)) Set.univ x₀

Вправа 10.1.5

theorem HasDerivWithinAt.of_zpow (n : ℤ) (x₀ : ℝ) (hx₀ : x₀ ≠ 0) : HasDerivWithinAt (fun (x : ℝ) => x ^ n) (↑n * x₀ ^ (n - 1)) (Set.univ \ {0}) x₀

Вправа 10.1.6