Ample twists of the pulled-back bundle on a blow-up

Let $f:Y\to X$ be a blow-up of an ideal sheaf $I$ with $Y$ integral and $X,Y$ compact, $L$ ample on $X$, and $J,\iota$ presenting the pullback of $I$. Then there are $a>0$ and $N$ such that for all $n\ge N$ the bundle $(f^*L)^{a(n+1)}\otimes J$ is ample on $Y$.

Notation. PresentsPullbackIdeal I f J ι says that $\iota:J\to\mathcal O_Y$ is a monomorphism whose image on affine opens is the extension of $I$ along $f$. IsBlowup I π says that $I$ pulls back to an invertible ideal along $\pi$ and that $\pi$ is universal with this property. IsAmple means that for each point $x$ and open $V\ni x$, some positive power has a global section with nonvanishing open containing $x$, inside $V$, and affine.

Formalization Note The statement is verbatim from OpenAI's Lean development, with Definitions files of this development imported in place of the upstream modules; these are supporting code for the statement.