From 79f9d3fa1f2f5c0babba8f96f7a262293a49279c Mon Sep 17 00:00:00 2001
From: Luke Naylor <l.naylor@sms.ed.ac.uk>
Date: Mon, 29 May 2023 17:40:19 +0100
Subject: [PATCH] Simplify expression in proof of theorem 6.1

---
 main.tex | 43 +++++++++++++++++++++++--------------------
 1 file changed, 23 insertions(+), 20 deletions(-)

diff --git a/main.tex b/main.tex
index 6bbe39e..44b5f6d 100644
--- a/main.tex
+++ b/main.tex
@@ -919,15 +919,18 @@ radius of the pseudo-wall being positive
 \begin{sagesilent}
 var("Delta", domain="real") # placeholder for the specific values of 1/epsilon
 
+assymptote_gap_condition1 = (1/Delta < bgmlv2_d_upperbound_exp_term)
+assymptote_gap_condition2 = (1/Delta < bgmlv3_d_upperbound_exp_term_alt2)
+
 r_upper_bound1 = (
-	(1/Delta < bgmlv2_d_upperbound_exp_term)
+	assymptote_gap_condition1
 	* r * Delta
 )
 
 assert r_upper_bound1.lhs() == r
 
 r_upper_bound2 = (
-	(1/Delta < bgmlv3_d_upperbound_exp_term_alt2)
+	assymptote_gap_condition2
 	* (r-R) * Delta + R
 )
 
@@ -951,7 +954,6 @@ assert r_upper_bound2.lhs() == r
 			\sage{r_upper_bound2.rhs()}
 		\right)
 	\end{align*}
-	\egroup
 
 	Taking the maximum of this expression over
 	$q \in [0, \chern_1^{\beta}(F)]\cap \frac{1}{n}\ZZ$
@@ -967,12 +969,14 @@ are elements of $\frac{1}{\lcm(m,2n^2)}\ZZ$.
 So, if any of the two upper bounds on $d$ come to within
 $\frac{1}{\lcm(m,2n^2)}$ of this lower bound, then there are no solutions for
 $d$.
+Hence any corresponding $r$ cannot be a rank of a
+pseudo-semistabilizer for $v$.
 
-Considering equations
+To avoid this, we must have,
+considering equations
 \ref{eqn:bgmlv2_d_bound_betamin},
 \ref{eqn:bgmlv3_d_bound_betamin},
-\ref{eqn:positive_rad_d_bound_betamin},
-this happens when:
+\ref{eqn:positive_rad_d_bound_betamin}.
 
 \bgroup
 
@@ -995,13 +999,16 @@ bounds_too_tight_condition2 = (
 )
 \end{sagesilent}
 
+\bgroup
+\def\psi{\chern_1^{\beta}(F)}
 \begin{equation}
 	\min\left(
 		\sage{bgmlv2_d_upperbound_exp_term},
-		\sage{bgmlv3_d_upperbound_exp_term_alt.subs(chbv==0)}
+		\sage{bgmlv3_d_upperbound_exp_term_alt2}
 	\right)
-	< \epsilon := \frac{1}{\lcm(m,2n^2)}
+	\geq \epsilon := \frac{1}{\lcm(m,2n^2)}
 \end{equation}
+\egroup
 
 \begin{sagesilent}
 # rearrange the "tightness" conditions in terms of r
@@ -1023,26 +1030,22 @@ assert bounds_too_tight_condition2.rhs() == r
 \noindent
 This is equivalent to:
 
+\bgroup
+\def\psi{\chern_1^{\beta}(F)}
+\def\Delta{\lcm(m,2n^2)}
 \begin{equation}
-	r >
+	\label{eqn:thm-bound-for-r-impossible-cond-for-r}
+	r \leq
 	\min\left(
 		\sage{
-			bounds_too_tight_condition1.lhs()
-			.expand()
-			.factor()
+			r_upper_bound1.rhs()
 		} ,
 		\sage{
-			bounds_too_tight_condition2.lhs()
-			.expand()
-			.factor()
+			r_upper_bound2.rhs()
 		}
 	\right)
 \end{equation}
-
-If this condition holds for all $q$, then there are no solutions for $d$,
-and therefore $r$ cannot satisfy this condition for all $q$.
-Taking the maximum of all these expressions over $q$, and substituting the value
-for $\epsilon$ gives the result.
+\egroup
 
 \egroup % end scope where epsilon redefined
 
-- 
GitLab