Direct proof of the global submean property for $\log |f|$

Question

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.

Answer 1

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.

Answer 2

Let me try to propose something:

As I understand from your post you say you're fine with functions without zeroes since for them we have equality. So let us try to reduce to this case. For an analytic function in any disc, in any smaller disc we have finitely many zeroes (not sure how hard is it to formalize? But it's a nice fact to have nontheless, and the prove is just Cauchy sequences). So, taking them with multiplicities we have $f(z) = g(z) \prod_{k=1}^n (z-a_k)$, where $g$ has no zeroes.

Logarithm of a product is a sum of logarithms, and for $g(z)$ we have equality, so it remains to deal with $(z-a_k)$, which is an explicit computation. For example, go to the polar coordinates with center at your point $c$ and on each concentric circle consider an appropriate Blaschke product which doesn't change the absolute value on the circle but increases the values inside (this is sort of a poor man's version of Jensen's formula).