Lemma 5.37.72FA053FE56D9

Proof. Work in product coordinates $(z,\zeta )$ with $p(z,\zeta )=z$. Write $\alpha $ for a multi-index in the fiber variables and $\mathrm{d}\lambda _\zeta $ for their Euclidean volume. A germ in the ideal on the right is a finite sum of bounded holomorphic multiples of pullbacks of germs that are square integrable against $\mathrm{e}^{-tu(z)}$. Fubini's theorem shows that it is weighted-integrable on a sufficiently small product neighborhood.

Conversely, let $F(z,\zeta )$ be a weighted-integrable holomorphic germ and expand it in the fiber variables,

The coefficient estimate for a holomorphic function on a polydisk gives, on smaller product neighborhoods,

Multiplying by $\mathrm{e}^{-tu(z)}$ and integrating in $z$ shows that each coefficient germ $f_\alpha $ belongs to $\mathcal I(tu)$. Let $J$ be the extension of this ideal to the local ring $R$ of holomorphic germs on the product. Every finite Taylor sum of $F$ belongs to $J$, and the remainder of total fiber degree at least $N$ belongs to $(\zeta )^ N$. Thus the class of $F$ in $R/J$ lies in $(\zeta )^ N(R/J)$ for every $N$. By the Krull intersection theorem for the finitely generated module $R/J$ over the Noetherian local ring $R$, the intersection of these submodules is zero. Hence $F\in J$. Smooth corrections and smooth positive volume densities do not change the integrability conditions. $\square$