Аналіз I, Розділ 10.4: Обернені функції та похідні #
Я (прим. перекл. Терренс Тао) намагався зробити переклад якомога точнішим перефразуванням оригінального тексту. Коли є вибір між більш ідіоматичним підходом Lean та більш точним перекладом, я зазвичай обирав останній. Зокрема, будуть місця, де код Lean можна було б "підправити", щоб зробити його більш елегантним та ідіоматичним, але я свідомо уникав цього вибору.
Основні конструкції та результати цього розділу:
- Теорема про обернену функцію.
theorem
HasDerivWithinAt.of_inverse
{X Y : Set ℝ}
{f g : ℝ → ℝ}
(hfXY : ∀ x ∈ X, f x ∈ Y)
(hgf : ∀ x ∈ X, g (f x) = x)
{x₀ y₀ f'x₀ g'y₀ : ℝ}
(hx₀ : x₀ ∈ X)
(hfx₀ : f x₀ = y₀)
(hcluster : ClusterPt x₀ (Filter.principal (X \ {x₀})))
(hf : HasDerivWithinAt f f'x₀ X x₀)
(hg : HasDerivWithinAt g g'y₀ Y y₀)
:
Лема 10.4.1
theorem
HasDerivWithinAt.of_inverse'
{X Y : Set ℝ}
{f g : ℝ → ℝ}
(hfXY : ∀ x ∈ X, f x ∈ Y)
(hgf : ∀ x ∈ X, g (f x) = x)
{x₀ y₀ f'x₀ g'y₀ : ℝ}
(hx₀ : x₀ ∈ X)
(hfx₀ : f x₀ = y₀)
(hcluster : ClusterPt x₀ (Filter.principal (X \ {x₀})))
(hf : HasDerivWithinAt f f'x₀ X x₀)
(hg : HasDerivWithinAt g g'y₀ Y y₀)
:
theorem
HasDerivWithinAt.of_inverse_of_zero_deriv
{X Y : Set ℝ}
{f g : ℝ → ℝ}
(hfXY : ∀ x ∈ X, f x ∈ Y)
(hgf : ∀ x ∈ X, g (f x) = x)
{x₀ y₀ : ℝ}
(hx₀ : x₀ ∈ X)
(hfx₀ : f x₀ = y₀)
(hcluster : ClusterPt x₀ (Filter.principal (X \ {x₀})))
(hf : HasDerivWithinAt f 0 X x₀)
:
¬DifferentiableWithinAt ℝ g Y y₀
theorem
Chapter10.inverse_function_theorem
{X Y : Set ℝ}
{f g : ℝ → ℝ}
(hfXY : ∀ x ∈ X, f x ∈ Y)
(hgYX : ∀ y ∈ Y, g y ∈ X)
(hgf : ∀ x ∈ X, g (f x) = x)
(hfg : ∀ y ∈ Y, f (g y) = y)
{x₀ y₀ f'x₀ : ℝ}
(hx₀ : x₀ ∈ X)
(hfx₀ : f x₀ = y₀)
(hne : f'x₀ ≠ 0)
(hcluster : ClusterPt x₀ (Filter.principal (X \ {x₀})))
(hf : HasDerivWithinAt f f'x₀ X x₀)
(hg : ContinuousWithinAt g Y y₀)
:
HasDerivWithinAt g (1 / f'x₀) Y y₀
Теорема 10.4.2 (Теорема про обернену функцію)