Sections on the blow-up are bounded by curve bounds

Let $S$ be a surface with ample $L$, $p$ a configuration of $r$ points, $B$ a point blow-up of $S$ at $p$ with projection $f$, and $J,\iota$ presenting the pullback of the centre ideal. Let $w\ge0$ with $w\cdot\operatorname{mult}_p(C)\le\deg_C L$ for all integral curves $C$ on $S$. If $k,m\in\mathbb N$ and $q$ is a nonzero section of $J^{m}\otimes f^*L^{k}$ on $B$, then $w\,rm\le k\,L^2$.

Notation. $L^2$ is selfIntersection, namely $\chi(L^2)-2\chi(L)+\chi(\mathcal O_S)$. $\deg_CL$ is curveDegree, namely $\chi(L|_C)-\chi(\mathcal O_C)$. $\operatorname{mult}_p(C)$ is totalMultiplicity, the sum over the points of curveMultiplicity, the order of the kernel ideal of the local ring map of $C$ at the point. 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$. 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. A Surface is an integral scheme smooth of relative dimension 2 over $\operatorname{Spec}\mathbb C$ with a closed immersion into some complex projective space over $\mathbb C$. An IntegralCurve on a surface is an integral closed subscheme of topological Krull dimension one, given by a closed immersion. Configuration S r is the set of $r$-tuples of complex points with distinct images, with the Zariski topology induced from the product.

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.