Let $D$ be a domain in $C^2$. Given $w\in C$, set $D_w=\left\{z\in C\mid \left(z,w\right)\in D\right\}$. If $f$ is a holomorphic and square-integrable function in $D$, then the set $E\left(D,f\right)$ of all $w$ such that $f(\cdot ,w)$ is not square-integrable in $D_w$ has measure zero. We call this set the exceptional set for $f$. In this Note we prove that whenever $0<r<1$ there exists a holomorphic square-integrable function $f$ in the unit ball $B$ in $C^2$ such that $E\left(B,f\right)$ is the circle $C\left(0,r\right)=\left\{z\in C\mid \left|z\right|=r\right\}$.

In this article, we prove the first mean value theorem for integrals [16]. The formalization of various theorems about the properties of the Lebesgue integral is also presented.MML identifier: MESFUNC7, version: 7.8.09 4.97.1001

In this article we prove the Monotone Convergence Theorem [16].MML identifier: MESFUNC9, version: 7.8.10 4.100.1011

In this article, the orthogonal projection and the Riesz representation theorem are mainly formalized. In the first section, we defined the norm of elements on real Hilbert spaces, and defined Mizar functor RUSp2RNSp, real normed spaces as real Hilbert spaces. By this definition, we regarded sequences of real Hilbert spaces as sequences of real normed spaces, and proved some properties of real Hilbert spaces. Furthermore, we defined the continuity and the Lipschitz the continuity of functionals...

We link together three themes which had remained separated so far: the Hilbert space properties of the Riemann zeros, the “dual Poisson formula” of Duffin-Weinberger (also named by us co-Poisson formula), and the “Sonine spaces” of entire functions defined and studied by de Branges. We determine in which (extended) Sonine spaces the zeros define a complete, or minimal, system. We obtain some general results dealing with the distribution of the zeros of the de-Branges-Sonine entire functions. We...