Аналіз I, Розділ 10.1: Базові визначення

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

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

• API для HasDerivWithinAt, derivWithin і DifferentiableWithinAt з Mathlib.

Зауважте, що конвенції Mathlib дещо відрізняються від тих, що в тексті: диференційовність визначена навіть у точках, які не є точками границі домену; похідні у таких випадках можуть бути неунікальними, але derivWithin все одно вибирає одну з них (або 0, якщо похідної не існує).

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

Визначення 10.1.1 (Диференційовність у точці). Для поняття HasDerivWithinAt з Mathlib гіпотеза про те, що x₀ є граничною точкою, не потрібна.

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 (Ньютонівське наближення) / Вправа 10.1.2

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

Твердження 10.1.10 / Вправа 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) (Диференціальне числення) / Вправа 10.1.4

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

Теорема 10.1.13 (b) (Диференціальне числення) / Вправа 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) (Правило суми) / Вправа 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) (Правило добутку) / Вправа 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) (Диференціальне числення) / Вправа 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) (Правило різниці) / Вправа 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) (Диференціальне числення) / Вправа 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) (Правило частки) / Вправа 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 (Правило складання) / Вправа 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