From 231aa48e29cb77e7777e857876ec5a00998e49a1 Mon Sep 17 00:00:00 2001 From: Eric P Date: Wed, 21 Aug 2024 23:00:32 -0700 Subject: [PATCH] Fix exponents and bold definitions --- blueprint/src/content.tex | 26 +++++++++++++------------- blueprint/web/dep_graph_document.html | 16 ++++++++-------- blueprint/web/index.html | 22 +++++++++++----------- 3 files changed, 32 insertions(+), 32 deletions(-) diff --git a/blueprint/src/content.tex b/blueprint/src/content.tex index f164e59..cf92c55 100644 --- a/blueprint/src/content.tex +++ b/blueprint/src/content.tex @@ -99,13 +99,13 @@ \section{Content} \begin{lemma}\label{split_first_and_last}\lean{split_first_and_last_factor_of_product}\leanok Let $a$ and $b$ be elements of a semigroup $S$. -For all $n > 1$, $(a*b)^n = a * (b+a)^(n-1) * b$. +For all $n > 1$, $(a*b)^n = a * (b+a)^{n-1} * b$. \end{lemma} \begin{proof} -Let $n=2$. Then $(a+b)^2 = a * (b*a)^(2-1) * b$. +Let $n=2$. Then $(a+b)^2 = a * (b*a)^{2-1} * b$. Assume that the statement holds for $n$. -Then we have that $(a*b)^(n+1) = a * b * (a*b)^n = a * b * a * (b*a)^(n-1) * b = a * (b*a)^n * b$. +Then we have that $(a*b)^{n+1} = a * b * (a*b)^n = a * b * a * (b*a)^{n-1} * b = a * (b*a)^n * b$. \end{proof} \begin{lemma}\label{thm:comm_ineq}\lean{comm_factor_le, comm_swap_le, comm_dist_le}\leanok @@ -120,20 +120,20 @@ \section{Content} Assume that the statement holds for $n$. Then we have that \begin{align} -a^(n+1) + b^(n+1) &= a * a^n * b^n * b \\ +a^{n+1} + b^{n+1} &= a * a^n * b^n * b \\ \text{by the induction hypothesis}\\ &< a * (a * b)^n * b \\ \text{since $a*b < b*a$}\\ &< a * (b * a)^n * b \\ \text{by the previous lemma}\\ -&= (a * b)^(n+1) \\ -&< (b * a)^(n+1) \\ +&= (a * b)^{n+1} \\ +&< (b * a)^{n+1} \\ \text{by the previous lemma}\\ &= b * (a * b)^n * a \\ &< b * (b * a)^n * a \\ \text{by the induction hypothesis}\\ &< b * b^n * a^n * a \\ -&= b^(n+1) * a^(n+1) +&= b^{n+1} * a^{n+1} \end{align} \end{proof} @@ -141,7 +141,7 @@ \section{Content} \uses{def:positive, def:negative} Let $a$ and $b$ be elements of an ordered semigroup $S$ that are not one. -Then $a$ is said to be Archimedean with respect to $b$ +Then $a$ is said to be \textbf{Archimedean with respect to} $b$ if there exists an $N\in \mathbb{N}^+$ such that for $n > N$, the inequality $b < a^n$ holds if $b$ is positive, and the inequality $b > a^n$ holds if $b$ is negative. @@ -149,18 +149,18 @@ \section{Content} \begin{definition}\label{def:arch}\lean{is_archimedean}\leanok \uses{def:one, def:arch_wrt} -An ordered semigroup is Archimedean if any two of its elements +An ordered semigroup is \textbf{Archimedean} if any two of its elements of the same sign are mutually Archimedean. \end{definition} \begin{definition}\label{def:anomalous_pair}\lean{anomalous_pair}\leanok Let $a$ and $b$ be elements of an ordered semigroup $S$. -Then $a$ and $b$ are said to form an anomalous pair +Then $a$ and $b$ are said to form an \textbf{anomalous pair} if for all $n\in \mathbb{N}^+$, one of the following holds \begin{align} -a^n < b^n < a^(n+1) \\ -a^n > b^n > a^(n+1) +a^n < b^n < a^{n+1} \\ +a^n > b^n > a^{n+1} \end{align} \end{definition} @@ -183,7 +183,7 @@ \section{Content} \] which means that, since $a^n < b$, \[ -b^n < (a*b)^n < b^(n+1) +b^n < (a*b)^n < b^{n+1} \] And so $b$ and $a*b$ form an anomalous pair. diff --git a/blueprint/web/dep_graph_document.html b/blueprint/web/dep_graph_document.html index efedaed..705f570 100644 --- a/blueprint/web/dep_graph_document.html +++ b/blueprint/web/dep_graph_document.html @@ -104,9 +104,9 @@

Dependencies

10

Let \(a\) and \(b\) be elements of an ordered semigroup \(S\).

-

Then \(a\) and \(b\) are said to form an anomalous pair if for all \(n\in \mathbb {N}^+\), one of the following holds

+

Then \(a\) and \(b\) are said to form an anomalous pair if for all \(n\in \mathbb {N}^+\), one of the following holds

- \begin{align} a^n {\lt} b^n {\lt} a^(n+1) \\ a^n {\gt} b^n {\gt} a^(n+1) \end{align} + \begin{align} a^n {\lt} b^n {\lt} a^{n+1} \\ a^n {\gt} b^n {\gt} a^{n+1} \end{align}
@@ -137,7 +137,7 @@

Dependencies

Definition 9 -

An ordered semigroup is Archimedean if any two of its elements of the same sign are mutually Archimedean.

+

An ordered semigroup is Archimedean if any two of its elements of the same sign are mutually Archimedean.

LaTeX @@ -168,7 +168,7 @@

Dependencies

8

Let \(a\) and \(b\) be elements of an ordered semigroup \(S\) that are not one.

-

Then \(a\) is said to be Archimedean with respect to \(b\) if there exists an \(N\in \mathbb {N}^+\) such that for \(n {\gt} N\), the inequality \(b {\lt} a^n\) holds if \(b\) is positive, and the inequality \(b {\gt} a^n\) holds if \(b\) is negative.

+

Then \(a\) is said to be Archimedean with respect to \(b\) if there exists an \(N\in \mathbb {N}^+\) such that for \(n {\gt} N\), the inequality \(b {\lt} a^n\) holds if \(b\) is positive, and the inequality \(b {\gt} a^n\) holds if \(b\) is negative.

LaTeX @@ -258,7 +258,7 @@

Dependencies

Definition 6 -

An element \(a\) of an ordered semigroup \(S\) is negative if for all \(x\in S\), \(a*x \lt x\).

+

An element \(a\) of an ordered semigroup \(S\) is negative if for all \(x\in S\), \(a*x {\lt} x\).

LaTeX @@ -384,7 +384,7 @@

Dependencies

Definition 5
-

An element \(a\) of an ordered semigroup \(S\) is positive if for all \(x\in S\), \(a*x \gt x\).

+

An element \(a\) of an ordered semigroup \(S\) is positive if for all \(x\in S\), \(a*x {\gt} x\).

LaTeX @@ -489,7 +489,7 @@

Dependencies

1

Let \(a\) and \(b\) be elements of a semigroup \(S\).

-

For all \(n {\gt} 1\), \((a*b)^n = a * (b+a)^(n-1) * b\).

+

For all \(n {\gt} 1\), \((a*b)^n = a * (b+a)^{n-1} * b\).

LaTeX @@ -629,7 +629,7 @@

Dependencies

.width(width) .height(height) .fit(true) - .renderDot(`strict digraph "" { graph [bgcolor=transparent]; node [label="\N", penwidth=1.8 ]; edge [arrowhead=vee]; "thm:neg_lt_pos" [color=green, fillcolor="#A3D6FF", label=neg_lt_pos, shape=ellipse, style=filled]; "lem:right_forall" [color=green, label=right_forall, shape=ellipse]; non_arch_anomalous [color=green, fillcolor="#A3D6FF", label=non_arch_anomalous, shape=ellipse, style=filled]; "def:OrderedSemigroup" [color=green, fillcolor="#B0ECA3", label=OrderedSemigroup, shape=box, style=filled]; "def:positive" [color=green, fillcolor="#B0ECA3", label=positive, shape=box, style=filled]; "def:OrderedSemigroup" -> "def:positive" [style=dashed]; "def:OrderedCancelSemigroup" [color=green, fillcolor="#B0ECA3", label=OrderedCancelSemigroup, shape=box, style=filled]; "def:OrderedSemigroup" -> "def:OrderedCancelSemigroup" [style=dashed]; "def:LinearOrderedSemigroup" [color=green, fillcolor="#B0ECA3", label=LinearOrderedSemigroup, shape=box, style=filled]; "def:OrderedSemigroup" -> "def:LinearOrderedSemigroup" [style=dashed]; "def:negative" [color=green, fillcolor="#B0ECA3", label=negative, shape=box, style=filled]; "def:OrderedSemigroup" -> "def:negative" [style=dashed]; "def:one" [color=green, fillcolor="#B0ECA3", label=one, shape=box, style=filled]; "def:OrderedSemigroup" -> "def:one" [style=dashed]; "def:positive" -> "thm:neg_lt_pos" [style=dashed]; "def:positive" -> "lem:right_forall" [style=dashed]; "def:arch_wrt" [color=green, fillcolor="#B0ECA3", label=arch_wrt, shape=box, style=filled]; "def:positive" -> "def:arch_wrt" [style=dashed]; "thm:pos_neg_or_one" [color=green, fillcolor="#A3D6FF", label=pos_neg_or_one, shape=ellipse, style=filled]; "def:positive" -> "thm:pos_neg_or_one" [style=dashed]; "def:LinearOrderedCancelSemigroup" [color=green, fillcolor="#B0ECA3", label=LinearOrderedCancelSemigroup, shape=box, style=filled]; "def:OrderedCancelSemigroup" -> "def:LinearOrderedCancelSemigroup" [style=dashed]; "def:negative" -> "thm:neg_lt_pos" [style=dashed]; "def:negative" -> "lem:right_forall" [style=dashed]; "def:negative" -> "def:arch_wrt" [style=dashed]; "def:negative" -> "thm:pos_neg_or_one" [style=dashed]; "def:one" -> "lem:right_forall" [style=dashed]; "def:one" -> "thm:pos_neg_or_one" [style=dashed]; "def:arch" [color=green, fillcolor="#B0ECA3", label=arch, shape=box, style=filled]; "def:one" -> "def:arch" [style=dashed]; "def:arch_wrt" -> "def:arch" [style=dashed]; "def:LinearOrderedCancelSemigroup" -> "thm:pos_neg_or_one" [style=dashed]; "def:arch" -> non_arch_anomalous [style=dashed]; "def:anomalous_pair" [color=green, fillcolor="#B0ECA3", label=anomalous_pair, shape=box, style=filled]; "def:anomalous_pair" -> non_arch_anomalous [style=dashed]; split_first_and_last [color=green, fillcolor="#A3D6FF", label=split_first_and_last, shape=ellipse, style=filled]; a0000000014 [color=blue, fillcolor="#A3D6FF", label=a0000000014, shape=ellipse, style=filled]; "thm:comm_ineq" [color=green, fillcolor="#A3D6FF", label=comm_ineq, shape=ellipse, style=filled];}`) + .renderDot(`strict digraph "" { graph [bgcolor=transparent]; node [label="\N", penwidth=1.8 ]; edge [arrowhead=vee]; split_first_and_last [color=green, fillcolor="#A3D6FF", label=split_first_and_last, shape=ellipse, style=filled]; "lem:right_forall" [color=green, label=right_forall, shape=ellipse]; non_arch_anomalous [color=green, fillcolor="#A3D6FF", label=non_arch_anomalous, shape=ellipse, style=filled]; "thm:pos_neg_or_one" [color=green, fillcolor="#A3D6FF", label=pos_neg_or_one, shape=ellipse, style=filled]; "thm:comm_ineq" [color=green, fillcolor="#A3D6FF", label=comm_ineq, shape=ellipse, style=filled]; a0000000014 [color=blue, fillcolor="#A3D6FF", label=a0000000014, shape=ellipse, style=filled]; "def:OrderedSemigroup" [color=green, fillcolor="#B0ECA3", label=OrderedSemigroup, shape=box, style=filled]; "def:OrderedCancelSemigroup" [color=green, fillcolor="#B0ECA3", label=OrderedCancelSemigroup, shape=box, style=filled]; "def:OrderedSemigroup" -> "def:OrderedCancelSemigroup" [style=dashed]; "def:LinearOrderedSemigroup" [color=green, fillcolor="#B0ECA3", label=LinearOrderedSemigroup, shape=box, style=filled]; "def:OrderedSemigroup" -> "def:LinearOrderedSemigroup" [style=dashed]; "def:positive" [color=green, fillcolor="#B0ECA3", label=positive, shape=box, style=filled]; "def:OrderedSemigroup" -> "def:positive" [style=dashed]; "def:negative" [color=green, fillcolor="#B0ECA3", label=negative, shape=box, style=filled]; "def:OrderedSemigroup" -> "def:negative" [style=dashed]; "def:one" [color=green, fillcolor="#B0ECA3", label=one, shape=box, style=filled]; "def:OrderedSemigroup" -> "def:one" [style=dashed]; "def:LinearOrderedCancelSemigroup" [color=green, fillcolor="#B0ECA3", label=LinearOrderedCancelSemigroup, shape=box, style=filled]; "def:OrderedCancelSemigroup" -> "def:LinearOrderedCancelSemigroup" [style=dashed]; "def:positive" -> "lem:right_forall" [style=dashed]; "def:positive" -> "thm:pos_neg_or_one" [style=dashed]; "def:arch_wrt" [color=green, fillcolor="#B0ECA3", label=arch_wrt, shape=box, style=filled]; "def:positive" -> "def:arch_wrt" [style=dashed]; "thm:neg_lt_pos" [color=green, fillcolor="#A3D6FF", label=neg_lt_pos, shape=ellipse, style=filled]; "def:positive" -> "thm:neg_lt_pos" [style=dashed]; "def:negative" -> "lem:right_forall" [style=dashed]; "def:negative" -> "thm:pos_neg_or_one" [style=dashed]; "def:negative" -> "def:arch_wrt" [style=dashed]; "def:negative" -> "thm:neg_lt_pos" [style=dashed]; "def:one" -> "lem:right_forall" [style=dashed]; "def:one" -> "thm:pos_neg_or_one" [style=dashed]; "def:arch" [color=green, fillcolor="#B0ECA3", label=arch, shape=box, style=filled]; "def:one" -> "def:arch" [style=dashed]; "def:LinearOrderedCancelSemigroup" -> "thm:pos_neg_or_one" [style=dashed]; "def:arch_wrt" -> "def:arch" [style=dashed]; "def:arch" -> non_arch_anomalous [style=dashed]; "def:anomalous_pair" [color=green, fillcolor="#B0ECA3", label=anomalous_pair, shape=box, style=filled]; "def:anomalous_pair" -> non_arch_anomalous [style=dashed];}`) .on("end", interactive); latexLabelEscaper = function(label) { diff --git a/blueprint/web/index.html b/blueprint/web/index.html index a5296e6..15a9954 100644 --- a/blueprint/web/index.html +++ b/blueprint/web/index.html @@ -335,7 +335,7 @@

Lean declarations

-

An element \(a\) of an ordered semigroup \(S\) is positive if for all \(x\in S\), \(a*x \gt x\).

+

An element \(a\) of an ordered semigroup \(S\) is positive if for all \(x\in S\), \(a*x {\gt} x\).

@@ -398,7 +398,7 @@

Lean declarations

-

An element \(a\) of an ordered semigroup \(S\) is negative if for all \(x\in S\), \(a*x \lt x\).

+

An element \(a\) of an ordered semigroup \(S\) is negative if for all \(x\in S\), \(a*x {\lt} x\).

@@ -745,7 +745,7 @@

Lean declarations

Let \(a\) and \(b\) be elements of a semigroup \(S\).

-

For all \(n {\gt} 1\), \((a*b)^n = a * (b+a)^(n-1) * b\).

+

For all \(n {\gt} 1\), \((a*b)^n = a * (b+a)^{n-1} * b\).

@@ -757,8 +757,8 @@

Lean declarations

▶
-

Let \(n=2\). Then \((a+b)^2 = a * (b*a)^(2-1) * b\).

-

Assume that the statement holds for \(n\). Then we have that \((a*b)^(n+1) = a * b * (a*b)^n = a * b * a * (b*a)^(n-1) * b = a * (b*a)^n * b\).

+

Let \(n=2\). Then \((a+b)^2 = a * (b*a)^{2-1} * b\).

+

Assume that the statement holds for \(n\). Then we have that \((a*b)^{n+1} = a * b * (a*b)^n = a * b * a * (b*a)^{n-1} * b = a * (b*a)^n * b\).

@@ -825,7 +825,7 @@

Lean declarations

If \(n=1\), then we are done.

Assume that the statement holds for \(n\). Then we have that

- \begin{align} a^(n+1) + b^(n+1) & = a * a^n * b^n * b \\ \text{by the induction hypothesis}\\ & {\lt} a * (a * b)^n * b \\ \text{since $a*b {\lt} b*a$}\\ & {\lt} a * (b * a)^n * b \\ \text{by the previous lemma}\\ & = (a * b)^(n+1) \\ & {\lt} (b * a)^(n+1) \\ \text{by the previous lemma}\\ & = b * (a * b)^n * a \\ & {\lt} b * (b * a)^n * a \\ \text{by the induction hypothesis}\\ & {\lt} b * b^n * a^n * a \\ & = b^(n+1) * a^(n+1) \end{align} + \begin{align} a^{n+1} + b^{n+1} & = a * a^n * b^n * b \\ \text{by the induction hypothesis}\\ & {\lt} a * (a * b)^n * b \\ \text{since $a*b {\lt} b*a$}\\ & {\lt} a * (b * a)^n * b \\ \text{by the previous lemma}\\ & = (a * b)^{n+1} \\ & {\lt} (b * a)^{n+1} \\ \text{by the previous lemma}\\ & = b * (a * b)^n * a \\ & {\lt} b * (b * a)^n * a \\ \text{by the induction hypothesis}\\ & {\lt} b * b^n * a^n * a \\ & = b^{n+1} * a^{n+1} \end{align}
@@ -892,7 +892,7 @@

Lean declarations

Let \(a\) and \(b\) be elements of an ordered semigroup \(S\) that are not one.

-

Then \(a\) is said to be Archimedean with respect to \(b\) if there exists an \(N\in \mathbb {N}^+\) such that for \(n {\gt} N\), the inequality \(b {\lt} a^n\) holds if \(b\) is positive, and the inequality \(b {\gt} a^n\) holds if \(b\) is negative.

+

Then \(a\) is said to be Archimedean with respect to \(b\) if there exists an \(N\in \mathbb {N}^+\) such that for \(n {\gt} N\), the inequality \(b {\lt} a^n\) holds if \(b\) is positive, and the inequality \(b {\gt} a^n\) holds if \(b\) is negative.

@@ -957,7 +957,7 @@

Lean declarations

-

An ordered semigroup is Archimedean if any two of its elements of the same sign are mutually Archimedean.

+

An ordered semigroup is Archimedean if any two of its elements of the same sign are mutually Archimedean.

@@ -1001,9 +1001,9 @@

Lean declarations

Let \(a\) and \(b\) be elements of an ordered semigroup \(S\).

-

Then \(a\) and \(b\) are said to form an anomalous pair if for all \(n\in \mathbb {N}^+\), one of the following holds

+

Then \(a\) and \(b\) are said to form an anomalous pair if for all \(n\in \mathbb {N}^+\), one of the following holds

- \begin{align} a^n {\lt} b^n {\lt} a^(n+1) \\ a^n {\gt} b^n {\gt} a^(n+1) \end{align} + \begin{align} a^n {\lt} b^n {\lt} a^{n+1} \\ a^n {\gt} b^n {\gt} a^{n+1} \end{align}
@@ -1090,7 +1090,7 @@

Lean declarations

which means that, since \(a^n {\lt} b\),

- \[ b^n {\lt} (a*b)^n {\lt} b^(n+1) \] + \[ b^n {\lt} (a*b)^n {\lt} b^{n+1} \]

And so \(b\) and \(a*b\) form an anomalous pair.

The other cases follow similarly.