Unique implicit roots on closed balls and analytic local inverses in Banach spaces.

theorem KamProject.Arnold1963.existsUnique_add_eq_on_closedBall {E : Type u_1} [NormedAddCommGroup E] [CompleteSpace E] {a : E → E} {Q : E} {r κ : NNReal} {ε : ℝ} (hb : NormBoundOn a (Metric.closedBall Q ↑r) ε) (hε : ε ≤ ↑r) (hκ : κ < 1) (hLip : LipschitzOnWith κ a (Metric.closedBall Q ↑r)) : ∃! q : E, q ∈ Metric.closedBall Q ↑r ∧ q + a q = Q

theorem KamProject.Arnold1963.norm_sub_le_of_add_eq {E : Type u_1} [NormedAddCommGroup E] {a : E → E} {q Q : E} {ε : ℝ} (he : q + a q = Q) (hb : ‖a q‖ ≤ ε) : ‖q - Q‖ ≤ ε

theorem KamProject.Arnold1963.exists_analytic_local_inverse_of_isUnit {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {f : E → E} {x : E} (hf : AnalyticAt ℂ f x) (hu : IsUnit (fderiv ℂ f x)) : ∃ (g : E → E), AnalyticAt ℂ g (f x) ∧ g (f x) = x ∧ ∀ᶠ (y : E) in nhds (f x), f (g y) = y

theorem KamProject.Arnold1963.exists_analytic_local_inverse {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {f : E → E} {x : E} (hf : AnalyticAt ℂ f x) (hn : ‖fderiv ℂ f x - ContinuousLinearMap.id ℂ E‖ < 1) : ∃ (g : E → E), AnalyticAt ℂ g (f x) ∧ g (f x) = x ∧ ∀ᶠ (y : E) in nhds (f x), f (g y) = y