From 4774b28ccbb14f1e99549cf3486c7fe7f59fe005 Mon Sep 17 00:00:00 2001
From: Luke Naylor <l.naylor@sms.ed.ac.uk>
Date: Thu, 15 Jun 2023 19:25:56 +0100
Subject: [PATCH] Prove corrolary

---
 main.tex | 31 ++++++++++++++++++++++++++++++-
 1 file changed, 30 insertions(+), 1 deletion(-)

diff --git a/main.tex b/main.tex
index 1c738d5..14d9cbb 100644
--- a/main.tex
+++ b/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
 
-- 
GitLab