The fixed point of a C¹ family of contractions of a Banach space is a C¹ function of the parameter

Let $P$ and $B$ be real Banach spaces, let $U\subseteq P$ be open, and let $T:P\times B\to B$ be a map of class C¹. Assume that for every $p\in U$ the map $T_p=T(p,\cdot):B\to B$ is a contraction: there is $K_p<1$ with $\|T_p(b)-T_p(b')\|\le K_p\|b-b'\|$ for all $b,b'\in B$. Let $\mathrm{fp}:P\to B$ be a map such that $\mathrm{fp}(p)$ is the fixed point of $T_p$ for every $p\in U$. Then

In words: the fixed point of a C¹ family of contractions depends in a C¹ way on the parameter. The contraction constant may depend on $p$ and need not be uniformly smaller than 1 on $U$. A general fact of analysis, not stated in the paper. In this mission it is a step in the proof of the companion theorem exists_localFlow_contMDiff_of_isInteriorPoint. That theorem says that the local flow of a C¹ vector field at an interior point is jointly C¹ in the initial point and the time. The proof of Proposition 1.1 (Section 3.1 of arXiv v1) uses it tacitly. There $P=E\times\mathbb R$ is the space of initial points and time scales, $B$ is a space of continuous curves, and $T$ is the Picard operator.

Formalization Note $T$ is curried in Lean (T : P → B → B), and the C¹ hypothesis is on the uncurried map fun q : P × B => T q.1 q.2. The fixed-point map fp is an arbitrary function with T p (fp p) = fp p for p ∈ U; it is unique there because each T p is a contraction. C¹ on $U$ is Mathlib's ContDiffOn ℝ 1 fp U. The expected proof applies the C¹ implicit function theorem (ContDiffAt.implicitFunction in Mathlib) to $(p,b)\mapsto b-T(p,b)$; the partial derivative in $b$ is the identity minus an operator of norm at most $K_p<1$, which is invertible.