From e10c2cc2dd37605d9d7cd7a62de3ea488eeebb80 Mon Sep 17 00:00:00 2001
From: Spencer Killen <sjkillen@ualberta.ca>
Date: Mon, 9 Dec 2024 08:23:54 -0700
Subject: [PATCH] .

---
 betastable/report.tex                 |  2 +
 betastable/sections/preliminaries.tex | 54 ++++++++++++++++++++++-----
 notation.tex                          |  9 +++--
 3 files changed, 52 insertions(+), 13 deletions(-)

diff --git a/betastable/report.tex b/betastable/report.tex
index cb96ec1..807e5fd 100644
--- a/betastable/report.tex
+++ b/betastable/report.tex
@@ -9,8 +9,10 @@
 \usepackage[english]{babel}
 \usepackage{amsthm}
 \usepackage{amsmath}
+\usepackage{amssymb}
 \usepackage{mathtools}
 \usepackage{hyperref}
+\usepackage[block]{calculation}
 \hypersetup{
 colorlinks=true,
 linkcolor=black,
diff --git a/betastable/sections/preliminaries.tex b/betastable/sections/preliminaries.tex
index ced708d..5b23277 100644
--- a/betastable/sections/preliminaries.tex
+++ b/betastable/sections/preliminaries.tex
@@ -56,11 +56,6 @@ So naturally, \Definition{deterministicstablerevisionoperator} applied to \BetaA
 For our purposes, we adapt their definition to fit \Approximators and \BetaApproximators.
 \begin{definitionOf}{deterministicbetastablerevisionoperator}
     Given \AnApproximator $o: \LL^2 \rightarrow \LL^2$
-    \begin{align*}
-        \Sdetbeta(o)(x, y)_1 \define \minLattice_{\lte} \big( \fixpointsOf(o(\partialApp, y)_1)  \setminus ((x \upclosure) \setminus (y \downclosure)) \big)
-        \\
-        \Sdetbeta(o)(x, y)_2 \define \minLattice_{\lte} \big( \fixpointsOf(o(x, \partialApp)_2) \setminus ((y \downclosure) \setminus (x \upclosure)) \big)
-    \end{align*}
 \end{definitionOf}
 
 The symmetric version
@@ -68,17 +63,56 @@ The symmetric version
 \begin{definitionOf}{deterministicbetastablerevisionoperator}
     Given \AnApproximator $o: \LL^2 \rightarrow \LL^2$
     \begin{align*}
-        \Sdetbeta(o)(x, y)_1 &\define \minLattice_{\lte} \Bigg( \fixpointsOf(o(\partialApp, y)_1)  \setminus \bigg( 
-            \Big( ((x \glbBinary y) \upclosure) \union ((x \lubBinary y) \downclosure) \Big)
-            \setminus
-            \Big( ((x \glbBinary y) \upclosure) \intersect ((x \lubBinary y) \downclosure) \Big)
-        \bigg) \Bigg)
+        \Sdetbeta(o)(x, y)_1 \define \glb_{\lte} \big( \fixpointsOf(o(\partialApp, y)_1)  \setminus ((x \upclosure) \setminus (y \downclosure)) \big)
         \\
+        \Sdetbeta(o)(x, y)_2 \define \glb_{\lte} \big( \fixpointsOf(o(x, \partialApp)_2) \setminus ((y \downclosure) \setminus (x \upclosure)) \big)
+    \end{align*}
+
+    % This symmetric version likely only works on so-called "A-prudent" pairs
+    \begin{align*}
+        \Sdetbeta(o)(x, y)_1 \} &\define \glb ( 
+            \fixpointsOf(o(\partialApp, y)_1) \setminus
+            \Big( ((x \glbBinary y) \upclosure) \symmetricdifference ((x \lubBinary y) \downclosure) \Big)
+         )\\
         \Sdetbeta(o)(x, y)_2 &\define \Sdetbeta(o)(y, x)_1
     \end{align*}
 \end{definitionOf}
 
 
+\begin{theorem}
+    For \AnApproximator $o: \LL^2 \rightarrow \LL^2$ s.t.\ $o\image{\LL^c} \subseteq \LL^c$, we have that
+    $\Sdet(o\restriction_{\LL^c})$ and $\Sdetbeta(o)$ are equivalent.
+\end{theorem}
+\begin{proof}
+    First we simplify $\Sdetbeta(o)(x, y)_1$
+    \begin{calculation}[=]
+        \minLattice_{\lte} ( 
+            \fixpointsOf(o(\partialApp, y)_1) \setminus
+            \Big( ((x \glbBinary y) \upclosure) \symmetricdifference ((x \lubBinary y) \downclosure) \Big)
+        \step{inside: 
+        \begin{subcalculation}[=]
+            ((x \glbBinary y) \upclosure) \symmetricdifference ((x \lubBinary y) \downclosure)
+            \step{Applying $x \lte y$}
+            (x \upclosure) \symmetricdifference (y \downclosure)
+            \step{Expand $\symmetricdifference$}
+            (x \upclosure \union~ y \downclosure) \setminus (x \upclosure \intersect~ y \downclosure)
+            \step{Using $\fixpointsOf(o(\partialApp, y)_1) \subseteq (y \downclosure)$ we don't quite have this yet tho}
+            \LL \setminus (x \upclosure \intersect~ y \downclosure)
+        \end{subcalculation}}
+        \step[]{Aside \begin{subcalculation}
+            \step[]{By Assumption}
+            \forall x \in [\bot, y],~ o(\partialApp, y)_1 \in [\bot, y]
+            \step[\implies]{Follows}
+            \fixpointsOf(o)
+        \end{subcalculation}}
+        \step{Leverage $\fixpointsOf(o(\partialApp, y)_1) \subseteq [\bot, y]$}
+        BNy bye
+        \step*{sdshds}
+        jdskdjsk
+    \end{calculation}
+\end{proof}
+
+
 \begin{propositionOf}{deterministicstablerevisionoperatorsymmetry}
     Given an \Approximator $o: \LL^2 \rightarrow \LL^2$ that is \Symmetric, its \BetaStableRevisionOperator $S(o)$ is also \Symmetric.
     Under symmetry the two are equivalent for consistent partition
diff --git a/notation.tex b/notation.tex
index c856ada..1289f9c 100644
--- a/notation.tex
+++ b/notation.tex
@@ -4,8 +4,9 @@
 \newcommand{\lteSub}[1]{\lteNoLink_{#1}}
 \newcommand{\image}[1]{[#1]}
 \newcommand{\define}{\coloneqq}
-\newcommand{\union}{\cup}
-\newcommand{\intersect}{\cap}
+\newcommand{\union}{\mathbin{\cup}}
+\newcommand{\intersect}{\mathbin{\cap}}
+\newcommand{\symmetricdifference}{\mathbin{\Delta}}
 \newcommand{\glb}{\bigwedge}
 \newcommand{\lub}{\bigvee}
 \newcommand{\glbBinary}{\land}
@@ -19,4 +20,6 @@
 \newcommand{\latticeinterval}[2]{[#1, #2]}
 
 \newcommand{\Sdet}{S}
-\newcommand{\Sdetbeta}{S^{\beta}}
\ No newline at end of file
+\newcommand{\Sdetbeta}{S^{\beta}}
+\let\restrictionWithSpaces\restriction
+\renewcommand{\restriction}{{\restrictionWithSpaces}}
\ No newline at end of file