Analyticity of local inverses #
theorem
AnalyticAt.analyticAt_localInverse
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{f : 𝕜 → 𝕜}
{x : 𝕜}
[CompleteSpace 𝕜]
[CharZero 𝕜]
(hf : AnalyticAt 𝕜 f x)
(hf' : deriv f x ≠ 0)
:
AnalyticAt 𝕜 (HasStrictDerivAt.localInverse f (deriv f x) x ⋯ hf') (f x)
The local inverse of an analytic function (at a point where its derivative does not vanish) is itself analytic.
theorem
analyticAt_comp_iff_of_deriv_ne_zero
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{f : 𝕜 → 𝕜}
{x : 𝕜}
[CompleteSpace 𝕜]
[CharZero 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{g : 𝕜 → E}
(hf : AnalyticAt 𝕜 f x)
(hf' : deriv f x ≠ 0)
: