Self-intersection of a twist of powers

For $L$ ample on $S$, a line bundle $J$, and $a,b\in\mathbb N$: $(L^a\otimes J^b)^2=a^2L^2+2ab\,(L\cdot J)+b^2J^2$, with $L\cdot J$ the mixed Euler number.

Notation. $L^2$ is selfIntersection, namely $\chi(L^2)-2\chi(L)+\chi(\mathcal O_S)$. $L\cdot M$ is mixedEuler, namely $\chi(L\otimes M)-\chi(L)-\chi(M)+\chi(\mathcal O_S)$. 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$.

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.