Injectivity of maps close to identity on possibly nonconvex domains, and consistent analytic inverses selected on a fixed source domain.

theorem KamProject.Arnold1963.injOn_add_of_local_lipschitz {E : Type u_1} [NormedAddCommGroup E] {a : E → E} {D : Set E} {r ε : ℝ} {κ : NNReal} (hb : ∀ x ∈ D, ‖a x‖ ≤ ε) (hε : 2 * ε ≤ r) (hκ : κ < 1) (hlip : ∀ x ∈ D, LipschitzOnWith κ a (Metric.closedBall x r)) : Set.InjOn (fun (x : E) => x + a x) D

theorem KamProject.Arnold1963.erosion_mem_nhds {E : Type u_1} [NormedAddCommGroup E] {D : Set E} {r s : NNReal} (hs : 0 < s) {x : E} (hx : x ∈ erosion D (r + s)) : erosion D r ∈ nhds x

theorem KamProject.Arnold1963.invFunOn_eventually_eq {E : Type u_1} [NormedAddCommGroup E] {f g : E → E} {D : Set E} {x : E} (hi : Set.InjOn f D) (hD : D ∈ nhds x) (hg : ContinuousAt g (f x)) (hgx : g (f x) = x) (he : ∀ᶠ (y : E) in nhds (f x), f (g y) = y) : ∀ᶠ (y : E) in nhds (f x), Function.invFunOn f D y = g y

theorem KamProject.Arnold1963.analytic_invFunOn {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {f : E → E} {D : Set E} {x : E} (hi : Set.InjOn f D) (hD : D ∈ nhds x) (hf : AnalyticAt ℂ f x) (hn : ‖fderiv ℂ f x - ContinuousLinearMap.id ℂ E‖ < 1) : AnalyticAt ℂ (Function.invFunOn f D) (f x) ∧ Function.invFunOn f D (f x) = x ∧ ∀ᶠ (y : E) in nhds (f x), f (Function.invFunOn f D y) = y