One step of Schwarz's lemma for Cartesian products: an entire function replaced by its Hermite interpolant in one variable, with bounds

Let $g$ be an entire function on $\mathbb{C}^\iota$ ($\iota$ finite) with $|g| \le K$ on the closed polydisc of radius $R$, let $i \in \iota$ and $S_0 \in \mathbb{N}$, and let $E$ be a finite set of complex numbers $\zeta$ with $|\zeta| \le r$, where $0 < r$ and $5r \le R$; put $p = |E|S_0$. There is an entire function $h$ on $\mathbb{C}^\iota$ such that:

• $|h| \le 3^{p}K$ on the closed polydisc of radius $R$;
• $|g - h| \le (2r)^{p}(3/R)^{p}K$ on the closed polydisc of radius $r$;
• for every point $\xi$ and all coordinate directions $v_0, \dots, v_{m-1}$ different from $i$: if, for every $\zeta \in E$ and every $k < S_0$, the derivative of $g$ of order $m + k$ along $e_{v_0}, \dots, e_{v_{m-1}}$ followed by $k$ times $e_i$ vanishes at $\xi[i := \zeta]$, then the derivative of $h$ of order $m$ along $e_{v_0}, \dots, e_{v_{m-1}}$ vanishes at $\xi$.

Here $\xi[i := \zeta]$ is $\xi$ with its coordinate $\xi_i$ replaced by $\zeta$, the polydiscs are centred at $0$, and the derivatives are values of iteratedFDeriv on the coordinate vectors $e_\nu$.

In the proof, $h$ is the Hermite interpolant of $g$ in the variable $z_i$ at the nodes of $E$, each with multiplicity $S_0$. Applied in each coordinate in turn, it proves Transcendence.cartesian_schwarz.

It is one step of the proof of Baker's theorem formalised in this mission, which follows Chapter 4 of Waldschmidt's book: Baker's theorem from the criterion of Schneider–Lang for Cartesian products, as observed by Bertrand and Masser (1980).

Novelty. None: a step of the proof of Proposition 4.7 of Waldschmidt's book (pp. 122–130). It does the work of Lemma 4.8 in the book's case $m = n$, with the bounds of Step 2.4, one coordinate at a time. The book's route goes through the ideal of Lemma 4.8 in all the variables at once, and its Step 2.1 uses Osgood's lemma and asserts the continuity of $f/P(z_n)$ without proof; here only the remainder has to be entire in all the variables, and the quotient is only bounded, slice by slice, so only one-variable complex analysis is used. The contribution of this node is the formal proof.