An integer combination of entire functions that is small on a polydisc, for given T, X and ℓ (Proposition 4.10 with the parameters left free)

Let $\iota$ and $\Lambda$ be finite sets, $n = |\iota|$ and $L = |\Lambda|$, and let $\varphi_\lambda$ ($\lambda \in \Lambda$) be entire functions on $\mathbb{C}^\iota$ with $|\varphi_\lambda| \le B_\lambda$ on the closed polydisc of radius $R$ about $0$ and $\sum_\lambda B_\lambda \le C$, where $C > 0$. Let $0 < r < R$, and let $T$, $X$ and $\ell \ge 1$ be integers with $\ell^{2T^n} < (X+1)^{L}$. Then there are integers $p_\lambda$, not all zero, with $|p_\lambda| \le X$, such that on the closed polydisc of radius $r$

With the parameters of Transcendence.siegel_small_values_parameters, it gives Proposition 4.10 (Transcendence.siegel_small_values).

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: the argument of §4.5 of Waldschmidt's book (Lemmas 4.11–4.13 and the proof of Proposition 4.10, pp. 132–136) with $T$, $X$ and $\ell$ left free. Thue–Siegel's lemma over $\mathbb{C}$ (the book's Lemma 4.12) is proved inside, as in the book from Lemma 4.11 applied to real and imaginary parts, with the factor $2$ in place of $\sqrt{2}$. In Lemma 4.13 the tail is bounded by Transcendence.taylor_tail_le. The contribution of this node is the formal proof.