Given an entire function $f : \mathbb{C} \to \mathbb{C}$, $\log |f|$ is subharmonic. Globally, this means that for any disk $D_r(c)$ we have the submean property
$$\log |f(c)| \le \frac{1}{\mu(D_r(c))} \int_{D_r(c)} \log |f(z)|~dz$$
If there are no zeros in a disk, this follows from Cauchy's theorem applied to the analytic function $\log f$, as $\log |f| = \Re \log f$, and indeed we have equality. Exactly at a zero, the inequality is trivial as $\log |f| = \log 0 = -\infty$. In the general case, if there are zeros, the inequality follows immediately from Jensen's formula.
Alternatively, one can use the first two facts to prove subharmonicity locally (away from zeros, and exactly at zeros), and then prove that local subharmonicity implies global subharmonicity.
Question: Is there is a more direct proof of the global submean property, without using Jensen's formula or that local subharmonicity implies global?
Motivation: I am playing with complex analysis in Lean and Mathlib, and want the global submean property (including around zeros) without having to prove Jensen's theorem or local-to-global. It feels like there is a chance that a direct trick involving Jensen's inequality (as opposed to Jensen's formula) or other properties of subharmonic functions would suffice, but I haven't found one yet.
Best Answer
One way to derive the global inequality is the Principle of Harmonic Majorant: If $D$ is a bounded region, $u$ is harmonic in $\overline{D}$, $f$ is analytic in $\overline{D}$, then the inequality $\log|f(z)|\leq u(z),\, z\in\partial D$ implies the same in $D$. To prove this, just apply the Maximum principle to the harmonic function $\log|f|-u$ in the region $D$ minus small neighborhoods of zeros of $f$; that the inequality holds on the boundaries of these small neighborhoods is clear since $\log|z|\to-\infty$ when $z\to$ a zero of $f$.
Now to prove your global inequality, use as $u$ the solution of the Dirichlet problem with the boundary values $\log|f|$.
The solution of the Dirichlet problem for a disk is completely elementary, and the value at the center is just the average of the values on the circumference.
So we only used the Maximum Principle for harmonic functions and solvability of the Dirichlet problem for a disk.