Prove corrolary

main.tex

@@ -1396,7 +1396,36 @@ r_upper_bound_all_q = (
 	\egroup
 \end{corrolary}
 
-%% TODO simplified expression for rmax by predicting which q gives rmax
+\begin{proof}
+\bgroup
+\def\psi{\chern_1^{\beta}(F)}
+\def\nu{\lcm(m,2n^2)}
+\let\originalDelta\Delta
+\renewcommand\Delta{{\psi^2}}
+The ranks of the pseudo-semistabilizers for $v$ are bounded above by the
+maximum over $q\in [0, \chern_1^{\beta}(F)]\cap \frac{1}{n}\ZZ$ of the
+expression in theorem \ref{thm:rmax_with_uniform_eps}.
+Noticing that the expression is a maximum of two quadratic functions in $q$:
+\begin{equation*}
+	f_1(q):=\sage{r_upper_bound1.rhs()} \qquad
+	f_2(q):=\sage{r_upper_bound2.rhs()}
+\end{equation*}
+These have their minimums at $q=0$ and $q=\chern_1^{\beta}(F)$ respectively.
+It suffices to find their intersection in
+$q\in [0, \chern_1^{\beta}(F)]$, if it exists,
+and evaluating on of the $f_i$ there.
+The intersection exists, provided that
+$f_1(\chern_1^{\beta}(F))>f_2(\chern_1^{\beta}(F))=R$,
+or equivalently,
+$R \leq \frac{1}{2}\lcm(m,2n^2){\chern_1^{\beta}(F)}^2$.
+Setting $f_1(q)=f_2(q)$ yields
+$q=\sage{q_sol.expand()}$.
+And evaluating $f_1$ at this $q$-value gives:
+$\sage{r_upper_bound_all_q.expand()}$.
+Finally, noting that $\originalDelta(v)=\psi^2$, we get the bound as
+stated in the corollary.
+\egroup
+\end{proof}
 
 %% refinements using specific values of q and beta