Several-complex-variables infrastructure

This umbrella imports finite-dimensional complex analyticity, polydisc Cauchy formulas and series, locally bounded Osgood, coordinate derivatives and Cauchy–Riemann equations, locally uniform limits and their derivatives, compact-open holomorphic function spaces, Montel's theorem, and analytic parameter-dependent integrals. Taylor coefficients, convergence and remainder estimates allow separate radii in each coordinate. The modules are independent of the simplex-measure and Carlson developments. Their public statements give the precise hypotheses of the infrastructure listed above; selected Mathlib-based statement counterparts are proved in LeanPool.CarlsonFunctions.Solution. The pinned upstream audit guide distinguishes these supporting results from its selected Carlson and Dirichlet-average claims.