From 554b3cec07c5b4413202ee022ceea56fd385b8cb Mon Sep 17 00:00:00 2001
From: Luke Naylor <l.naylor@sms.ed.ac.uk>
Date: Wed, 10 Jan 2024 18:13:48 +0000
Subject: [PATCH] Add main lemmas around bounds in problem 1
---
main.tex | 42 +++++++++++++++++++++++++++++++++++++++++-
other_P_choice.ipynb | 40 +++++++++++++++++++++++++++++++++++++++-
2 files changed, 80 insertions(+), 2 deletions(-)
diff --git a/main.tex b/main.tex
index 51ee9e3..d54c4f1 100644
--- a/main.tex
+++ b/main.tex
@@ -1340,7 +1340,47 @@ A generic example of this is plotted in figure
\label{fig:problem1:d_bounds_xmpl_gnrc_q}
\end{figure}
-\subsection{Bounds on Semistabilizer Rank \texorpdfstring{$r$}{r} in Problem
+\subsection{Bounds on Semistabilizer Rank \texorpdfstring{$r$}{} in Problem
+\ref{problem:problem-statement-1}}
+
+As discussed at the end of subsection \ref{subsubsect:all-bounds-on-d-prob1}
+(and illustrated in figure \ref{fig:problem1:d_bounds_xmpl_gnrc_q}),
+there are no solutions $u$ to problem \ref{problem:problem-statement-1}
+with large $r=\chern_0(u)$, since the lower bound on $d=\chern_2(u)$ is larger
+than the upper bounds.
+Therefore, we can calculate upper bounds on $r$ by calculating for which values,
+the lower bound on $d$ is equal to one of the upper bounds on $d$
+(i.e. finding certain intersection points of the graph in figure
+\ref{fig:problem1:d_bounds_xmpl_gnrc_q}).
+
+\begin{lemma}[Problem \ref{problem:problem-statement-1} upper Bound on $r$]
+ Let $u$ be a solution to problem \ref{problem:problem-statement-1}
+ and $q\coloneqq\chern_1^{\beta}(u)$.
+ Then $r\coloneqq\chern_0(u)$ is bounded above by the following expression:
+ \begin{equation}
+ \sage{problem1.r_bound_expression}
+ \end{equation}
+\end{lemma}
+
+\begin{proof}
+ qed
+
+\end{proof}
+
+\begin{lemma}
+ Let $u$ be a solution to problem \ref{problem:problem-statement-1}.
+ Then $r\coloneqq\chern_0(u)$ is bounded above by the following expression:
+ \begin{equation}
+ \sage{problem1.r_max}
+ \end{equation}
+\end{lemma}
+
+\begin{proof}
+ qed
+
+\end{proof}
+
+\subsection{Bounds on Semistabilizer Rank \texorpdfstring{$r$}{} in Problem
\ref{problem:problem-statement-2}}
Now, the inequalities from the above subsubsection
diff --git a/other_P_choice.ipynb b/other_P_choice.ipynb
index 9ad201e..a59bbfe 100644
--- a/other_P_choice.ipynb
+++ b/other_P_choice.ipynb
@@ -907,7 +907,9 @@
"cell_type": "code",
"execution_count": 33,
"id": "e4fb002a",
- "metadata": {},
+ "metadata": {
+ "scrolled": true
+ },
"outputs": [
{
"data": {
@@ -933,6 +935,42 @@
").factor()"
]
},
+ {
+ "cell_type": "code",
+ "execution_count": 55,
+ "id": "0347bc71",
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/html": [
+ "<html>\\(\\displaystyle \\frac{\\sqrt{2} \\sqrt{R} \\min\\left(q, \\sqrt{2} \\sqrt{R} \\sqrt{{\\mathrm{ch}_2^B(v)}} - q + {\\mathrm{ch}_1^B(v)}\\right)}{2 \\, \\sqrt{{\\mathrm{ch}_2^B(v)}}}\\)</html>"
+ ],
+ "text/latex": [
+ "$\\displaystyle \\frac{\\sqrt{2} \\sqrt{R} \\min\\left(q, \\sqrt{2} \\sqrt{R} \\sqrt{{\\mathrm{ch}_2^B(v)}} - q + {\\mathrm{ch}_1^B(v)}\\right)}{2 \\, \\sqrt{{\\mathrm{ch}_2^B(v)}}}$"
+ ],
+ "text/plain": [
+ "1/2*sqrt(2)*sqrt(R)*min(q, sqrt(2)*sqrt(R)*sqrt(twisted_v2) - q + twisted_v1)/sqrt(twisted_v2)"
+ ]
+ },
+ "execution_count": 55,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "_common_factor = sqrt(R)/sqrt(twisted_v2)/sqrt(2)\n",
+ "( r_bound_expression :=\n",
+ " min_symbolic(\n",
+ " positive_intersection_bgmlv2 / _common_factor,\n",
+ " positive_intersection_bgmlv3 / _common_factor\n",
+ " )\n",
+ " .__mul__(_common_factor)\n",
+ " .expand()\n",
+ " .simplify()\n",
+ ")"
+ ]
+ },
{
"cell_type": "markdown",
"id": "6acd7233",
--
GitLab