42 43/-! ### §2. Complex carrier certificate -/ 44 45/-- A certificate packaging the complex-analytic properties of the Euler carrier 46`C(s) = det₂(I − A(s))²` on a disk inside the strip. 47 48The real-axis versions of convergence, nonvanishing, and log-derivative bounds 49are already proved in `EulerInstantiation.lean`. This structure lifts them to 50the complex setting by recording the disk center, radius, and the analytic 51properties on that disk. 52 53The `differentiableOn` field is the one that requires genuine Mathlib complex 54analysis infrastructure (locally uniform convergence of holomorphic series). 55It is stated as a field rather than proved from scratch. -/
used by (2)
From the project-wide theorem graph. These declarations reference this one in their body.