RadiiPolynomial

This blueprint presents a formalization in Lean 4 of the radii polynomial approach for proving existence of zeros of nonlinear functions on Banach spaces. The method combines the contraction mapping theorem with Newton-like operators, enabling computer-assisted proofs of existence and uniqueness of solutions.

The formalization covers both finite-dimensional and infinite-dimensional settings, with particular emphasis on the Banach Fixed Point Theorem (Contraction Mapping Theorem), Newton-like operators for zero-finding problems, radii polynomial approach in finite dimensions (Theorem 2.4.2), general radii polynomial approach on Banach spaces (Theorem 7.6.2), and Neumann series for operator invertibility.

The formalization extends classical results to maps between potentially different Banach spaces \(E\) and \(F\), requiring careful treatment of approximate inverses and approximate derivatives.