The mean-value $L^2$ bound for holomorphic functions on a polydisc

The Axiom of Countable Choice ${\mathrm{A}\mathrm{C}}_{\omega }$ is the principle defined by The Axiom of Countable Choice (${\mathrm{A}\mathrm{C}}_{\omega }$). It is the only choice assumption below; the polar-measure and product-Lebesgue suppliers used here state it explicitly.

If $g$ is holomorphic on $D(b,R)$ and $0<s<R$, then $g(b)=(2\pi {)}^{-1}{\int }_0^{2\pi }g(b+s{e}^{i\theta })d\theta$ (A holomorphic function equals its average on every circle inside a larger concentric holomorphy disc).

The chart surface measure of $S^1$ agrees with its polar surface measure; under the angular chart $\omega =e^{i\theta }$ its density is $d\theta$, so $\sigma (S^1)=2\pi$ (Surface integration on compact C1 hypersurfaces, Agreement with the existing polar sphere measure).

For every nonnegative Borel $h$ on ${\mathbb{R}}^2$, polar coordinates give $\int hd{\lambda }_2={\int }_0^{\mathrm{\infty }}{\int }_{S^1}h(s\omega )sd\sigma (\omega )ds$ (The polar surface set function on the unit sphere, Polar coordinates decompose Lebesgue measure into r^{n-1} dr d sigma).

Lebesgue measure is translation invariant on measurable sets (Lebesgue outer measure, Lebesgue measurability and Lebesgue measure are unchanged by translation).

Every nonnegative measurable function is the increasing limit of nonnegative simple functions, and increasing limits pass through the Lebesgue integral; thus the setwise translation invariance in [F4] extends from indicators and simple functions to nonnegative Borel integrals (Every nonnegative measurable function admits an explicit increasing sequence of simple approximations, Monotone convergence for the integral).

Borel sets in a finite Euclidean product are product-measurable; Tonelli permits iterated integration of nonnegative product-measurable functions, and the finite product of planar Lebesgue measures agrees with Euclidean Lebesgue measure under ${\mathbb{R}}^{2m}\cong ({\mathbb{R}}^2{)}^m$ (The Borel product of R^m and R^n is the Borel sigma-algebra of R^{m+n}, Tonelli's theorem for nonnegative measurable functions on a sigma-finite product, On Borel subsets of R^{m+n}, the product lambda_m times lambda_n agrees with lambda_{m+n}).

A holomorphic function is continuous, hence $\mathrm{\mid }f{\mathrm{\mid }}^2$ is Borel (A holomorphic function of several variables is continuous and separately holomorphic); the one-variable case is also supplied by Complex differentiability at a point implies continuity there.

Restricting the complex linear derivative in the definition of holomorphy to a coordinate line shows that every coordinate slice of a holomorphic function is holomorphic (Holomorphic functions on an open subset of ${\mathbb{C}}^m$).

A polydisc is the product of its coordinate discs, and ${\mathbb{C}}^m$ is identified with ${\mathbb{R}}^{2m}$ with the corresponding Lebesgue convention (Balls, polydiscs and the distinguished boundary in ${\mathbb{C}}^m$, Complex $m$-space and its real coordinate dictionary).