The extended complex plane is a fundamental object in complex analysis, hyperbolic geometry, and mathematical physics. Its geometry is governed by Möbius transformations, with the cross ratio serving as a central invariant. We present a formalization of these concepts in the Lean4 theorem prover. The extended complex plane is represented using Mathlib's Option type over $\mathbb{C}$, where the additional element represents the point at infinity. On this foundation, we define Möbius transformations, their action on the extended complex plane, and the cross ratio. We formalize several basic properties of Möbius transformations, including their group structure, and identify them with a projective general linear group. We also prove the uniqueness of a Möbius transformation mapping any three distinct points to any other three distinct points, and the invariance of the cross ratio. All proofs are machine-checked in Lean 4. The complete development comprises approximately 6,000 lines of Lean code, including about 40 definitions and 150 lemmas and theorems. This work provides a verified foundation for future formalizations of conformal geometry, hyperbolic models, modular forms, and applications in mathematical physics.

In this paper, we study the Bloch and $\mathcal Q_p$--Carleson measure problems on the unit disc $\mathbb D$. In the Bloch case, for a positive Borel measure $μ$ on $\mathbb D$, we give a complete characterization of the boundedness and compactness of the embedding $$ \operatorname{id}:\mathcal B \longrightarrow L^2(μ) $$ in terms of the Bloch capacity $\mathfrak B_{\mathcal R}(μ)$ associated with an admissible dyadic resolution $\mathcal R$ of $\mathbb D$. The proof is based on the Bergman projection representation of Bloch functions, conditional expectations on admissible dyadic resolutions, and a finite-dimensional semidefinite programming argument. We also adapt this dyadic framework to the more general $\mathcal Q_p$--Carleson measure problem and obtain a corresponding complete boundedness and compactness characterization for $$ \operatorname{id}:\mathcal Q_p \longrightarrow L^2(μ), \qquad 0<p\le1. $$ This work further develops the dyadic approach introduced in our recent work on composition operators on $\mathcal Q_p$ spaces, but in a different setting where the embedding involves recovering function values from derivative information.

We prove a Littlewood-Paley formula for the Hardy space of Dirichlet series $\mathscr{H}^p$ with $1\leq p<\infty$ in terms of almost every vertical limit function. This significantly strengthens previous results, which hold either only as an average over the vertical limit functions or under additional assumptions of uniform convergence. As part of our approach, we obtain a Hardy-Stein identity for the derivative of the $p$-mean of almost every vertical limit. We further show that the mean counting function exists for any $f$ in $\mathscr{H}^p$ in terms of almost all of its vertical limit functions. This is done by establishing a version of Jensen's formula in this setting. In the process, we also deduce ergodic versions of Fatou's lemma and the monotone and dominated convergence theorems for the Kronecker flow.

Let $f$ be a transcendental entire function, $V$ be a simply connected Fatou component of $f,$ and $U$ be a Fatou component with $f(U)\subset V.$ There is a natural way to associate $f|_U$ to an inner function, namely a function $g_f:=ψ^{-1}\circ f\circφ,$ where $φ:\mathbb{D}\to U$ and $ψ:\mathbb{D}\to V$ are Riemann maps. Inner functions have been used as a tool in the study of the iterates of transcendental entire, and more recently meromorphic, functions. However, there are only a few examples where associated inner functions have been calculated explicitly, with the case where $f$ has infinite degree in $U$ being the least well understood and more complicated. In this paper, we introduce a general method for calculating associated inner functions to a wide class of entire functions arising as `lifts'. In particular, if $f$ is a lift of a transcendental entire function $h,$ we show that an inner function associated to $f|_U$ can be obtained by relating it to an inner function associated to $h|_G,$ where $G$ is the Fatou component that lifts to $U.$ This result significantly generalises the main part of a theorem by Evdoridou, Rempe and Sixmith, and can be applied to several functions that have been studied so far. In both finite- and infinite-degree settings, the results hold for forward-invariant Fatou components as well as for wandering domains.

We prove that the top wedge power of the Ricci form of a complete non-compact Kähler manifold with positive sectional curvature has finite integral. Using a result of Chen-Zhu, an immediate consequence is the quasiprojectivity of such manifolds under the assumption of bounded sectional curvature. A key new idea to prove Bézout estimates along with a Lipschitz weight with finite Monge-Ampère mass is used in the proof of the main result.

We study the Cauchy--Dirichlet problem for parabolic complex Hessian equations on Hermitian manifolds and on bounded strictly m-pseudoconvex domains. In the smooth setting, we prove global existence and uniqueness of classical solutions under the presence of an admissible parabolic subsolution, by establishing a priori estimates up to the parabolic boundary. The estimates combine parabolic boundary techniques for complex Hessian equations with interior second order estimates and a blow-up argument. We then develop a general pluripotential framework for degenerate right-hand sides with L^p densities, p>n/m, and bounded Cauchy--Dirichlet data. Since the usual automorphism and Walsh-type arguments do not directly apply in a variable Hermitian background, we use approximation by smooth data, balayage, parabolic Perron envelopes, and a continuous obstacle approximation based on Harvey--Lawson--Plis subequation theory. The resulting solution is continuous for positive time, locally uniformly Lipschitz and semi-concave in time, and continuous up to the initial slice when the initial datum is continuous. We also prove a parabolic comparison principle via time regularization, Riemann sum approximations, and mixed Hessian inequalities.

In 1829, Cauchy derived an upper bound for every root of a complex polynomial using the maximum of the absolute values of the coefficients. In 1931, Montel derived an upper bound using the sum of the absolute values of the coefficients. We derive noncommutative versions of the Cauchy and Montel bounds.

This paper shows that the concept of complex frequency, originally introduced to characterize the dynamics of signals with complex values, constitutes a generalization of eigenvalues when applied to the states of linear time-invariant (LTI) systems. Starting from the definition of geometric frequency, which provides a geometrical interpretation of frequency in electric circuits that admits a natural decomposition into symmetric and antisymmetric components associated with amplitude variation and rotational motion, respectively, we show that complex frequency arises as its restriction to the two-dimensional Euclidean plane. For LTI systems, it is shown that the complex frequencies computed from the system's states subject to a non-isometric transformation, coincide with the original system's eigenvalues. This equivalence is demonstrated for diagonalizable systems of any order. The paper provides a unified geometric interpretation of eigenvalues, bridging classical linear system theory with differential geometry of curves. The paper also highlights that this equivalence does not generally hold for nonlinear systems. On the other hand, the geometric frequency of the system can always be defined, providing a geometrical interpretation of the system flow. A variety of examples based on linear and nonlinear circuits illustrate the proposed framework.

The outlines of a "Galois theory" for bimeromorphic geometry is here developed, via the study of model-theoretic definable binding groups in the theory CCM of compact complex spaces. As an application, a structure theorem about principal meromorphic bundles with algebraic structure group, and admitting no horizontal subvarieties, is deduced. Examples of algebraic groups arising as binding groups are provided, as is a characterisation of when they are linear. Using binding groups in CCM it is shown that, in contrast to the situation in differentially closed fields, there are many algebraic groups which admit nontrivial definable torsors over acl-closed sets in the theory DCCM of existentially closed differential CCM-structures. A self-contained exposition of the binding group theorem in totally transcendental theories, that emphasises the bitorsorial nature of the construction, is also included.

In this paper we study the spectral analysis of Bochner-Kodaira Laplacians on an Abelian variety, complex projective space $\mathbb{P}^{n}$ and a Grassmannian with a holomorphic line bundle. By imitating the method of creation and annihilation operators in physics, we convert those eigensections (of the \textquotedblleft higher energy" level) into holomorphic sections (of the \textquotedblleft lowest energy" level). This enables us to endow these spectral bundles, which are defined over the dual Abelian variety, with natural holomorphic structure. Using this conversion expressed in a concrete way, all the higher eigensections are explicitly expressible using holomorphic sections formed by theta functions. Moreover, we give an explicit formula for the dimension of the space of higher-level eigensections on $\mathbb{P}^{n}$ through vanishing theorems and the Hirzebruch-Riemann-Roch theorem. These give a theoretical study related to some problems newly discussed by string theorists using numerical analysis. Some partial results on Grassmannians are proved and some directions for future research are indicated.

We define the eñe product for the multiplicative group of polynomials and formal power series with coefficients on a commutative ring and unitary constant coefficient. This defines a commutative ring structure where multiplication is the additive structure and the eñe product is the multiplicative one. For polynomials with complex coefficients, the eñe product acts as a multiplicative convolution of their divisor. We study its algebraic properties, its relation to symmetric functions on an infinite number of variables, to tensor products, and Hecke operators. The exponential linearizes also the eñe product. The eñe product extends to rational functions and formal meromorphic functions. We also study the analytic properties over the complex numbers, and for entire functions. The eñe product respects Hadamard-Weierstrass factorization and is related to the Hadamard product. The eñe product plays a central role in predicting the phenomenon of the "statistics on Riemann zeros" for Riemann zeta function and general Dirichlet $L$-functions discovered by the author. It also gives reasons to believe in the Riemann Hypothesis as explained in the survey "Notes on the Riemann Hypothesis".