Аналіз I, Глава 10.4 #
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:
- The inverse function theorem
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 (Inverse function theorem)