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