Section counts on the blow-up of a surface

Let $S,T$ be surfaces with $L$ ample on $S$ and $A$ ample on $T$, $p$ a configuration of $r$ points on $S$, $f:T\to S$ a blow-up of the centre ideal over $\mathbb C$, and $J,\iota$ presenting the pullback of the ideal. Then for a line bundle $M$ on $S$ and $n\in\mathbb N$, $h^0(T,J^n\otimes f^*M)\le h^0(S,M)$ and $2h^0(S,M)\le 2h^0(T,J^n\otimes f^*M)+rn(n+1)$.

Notation. $h^n$ is cohomologyDimension, the Module.finrank over $\mathbb C$ of $\operatorname{Ext}^n(\mathcal O,-)$, which is 0 for an infinite-dimensional space. 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. 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$. 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.