Skip to content

Commit

Permalink
Add large difference definition to blueprint
Browse files Browse the repository at this point in the history
  • Loading branch information
@ericluap
ericluap committed Sep 8, 2024
1 parent 0fcbe82 commit b860c21
Show file tree
Hide file tree
Showing 6 changed files with 133 additions and 17 deletions.
6 changes: 3 additions & 3 deletions OrderedSemigroups/Archimedean.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -33,6 +33,9 @@ abbrev has_anomalous_pair := ∃a b : α, anomalous_pair a b
`a` is one, `b` is one, or if `a` and `b` have the same sign, then `a` is Archimedean with respect to `b`.-/
def is_archimedean := ∀a b : α, is_one a ∨ is_one b ∨ (same_sign a b → is_archimedean_wrt a b)

abbrev has_large_differences := ∀a b : α, (is_positive a → a < b → ∃(c : α) (n : ℕ+), is_archimedean_wrt c a ∧ a^n*c ≤ b^n) ∧
(is_negative a → b < a → ∃(c : α) (n : ℕ+), is_archimedean_wrt c a ∧ a^n*c ≥ b^n)

theorem not_anomalous_pair_self (a : α) : ¬anomalous_pair a a := by
simp

Expand Down Expand Up @@ -415,9 +418,6 @@ theorem arch_wrt_self {a : α} (not_one : ¬is_one a) : is_archimedean_wrt a a :
· exact lt_of_le_of_lt (neg_ppow_le_ppow 2 n neg_a hn) (neg_one_lt_squared neg_a)
· contradiction

abbrev has_large_differences := ∀a b : α, (is_positive a → a < b → ∃(c : α) (n : ℕ+), is_archimedean_wrt c a ∧ a^n*c ≤ b^n) ∧
(is_negative a → b < a → ∃(c : α) (n : ℕ+), is_archimedean_wrt c a ∧ a^n*c ≥ b^n)

theorem not_anomalous_large_difference (not_anomalous : ¬has_anomalous_pair (α := α)) :
has_large_differences (α := α) := by
intro a b
Expand Down
4 changes: 3 additions & 1 deletion blueprint/lean_decls
View file
Original file line number Diff line number Diff line change
Expand Up @@ -18,4 +18,6 @@ is_archimedean_wrt
is_archimedean
anomalous_pair
non_archimedean_anomalous_pair
not_anomalous_comm_and_arch
not_anomalous_comm_and_arch
has_large_differences
not_anomalous_iff_large_difference
24 changes: 16 additions & 8 deletions blueprint/src/content.tex
View file
Original file line number Diff line number Diff line change
Expand Up @@ -244,15 +244,23 @@ \section{Content}
The case where $b$ is negative and $a$ is positive is symmetric.
\end{proof}

\begin{theorem}
\uses{def:arch_wrt, def:anomalous_pair}
\begin{definition}\label{def:has_large_differences}\lean{has_large_differences}\leanok
An ordered semigroup $S$ has \textbf{large differences} if
for all $a,b\in S$, the two following implications hold
\begin{itemize}
\item if $a$ is positive and $a<b$, then there exists $c\in S$
and $n\in \mathbb{N}^+$ such that $c$ is Archimedean with respect to $a$
and $a^n*c \le b^n$
\item if $a$ is negative and $b < a$, then there exists $c\in S$
and $n\in \mathbb{N}^+$ such that $c$ is Archimedean with respect to $a$
and $a^n*c \ge b^n$
\end{itemize}
\end{definition}

\begin{theorem}\lean{not_anomalous_iff_large_difference}\leanok
\uses{def:arch_wrt, def:anomalous_pair, def:has_large_differences}
In a linear ordered cancel semigroup $S$, there are no anomalous pairs
if and only if
for any two elements $a,b\in S$,
if $a$ and $b$ are positive and $a < b$, then there exists an $n \in \mathbb{N}^+$ and
a $c\in S$ that is Archimedean with respect to $a$ such that $a^n * c \le b^n$,
and if $a$ and $b$ are negative and $b < a$, then there exists an $n\in \mathbb{N}^+$ and
a $c\in S$ that is Archimedean with respect to $a$ such that $a^n *c \ge b^n$.
if and only if there are large differences.
\end{theorem}
\begin{proof}
($\Rightarrow$)
Expand Down
Binary file modified blueprint/src/web.paux
View file
Binary file not shown.
42 changes: 39 additions & 3 deletions blueprint/web/dep_graph_document.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -73,13 +73,13 @@ <h1 id="doc_title">Dependencies</h1>
Theorem
</span>
<span class="theorem_thmlabel">5</span></div>
<div class="thm_thmcontent"><p> In a linear ordered cancel semigroup \(S\), there are no anomalous pairs if and only if for any two elements \(a,b\in S\), if \(a\) and \(b\) are positive and \(a {\lt} b\), then there exists an \(n \in \mathbb {N}^+\) and a \(c\in S\) that is Archimedean with respect to \(a\) such that \(a^n * c \le b^n\), or if \(a\) and \(b\) are negative and \(b {\lt} a\), then there exists an \(n\in \mathbb {N}^+\) and a \(c\in S\) that is Archimedean with respect to \(a\) such that \(a^n *c \ge b^n\). </p>
<div class="thm_thmcontent"><p> In a linear ordered cancel semigroup \(S\), there are no anomalous pairs if and only if there are large differences. </p>
</div>

<a class="latex_link" href="index.html#a0000000019">LaTeX</a>



<a class="lean_link lean_decl" href="https://ericluap.github.io/OrderedSemigroups/docs/find/#doc/not_anomalous_iff_large_difference">Lean</a>



Expand Down Expand Up @@ -179,6 +179,42 @@ <h1 id="doc_title">Dependencies</h1>



</div>

</div>
</div>



<div class="dep-modal-container" id="def:has_large_differences_modal">
<div class="dep-modal-content">
<button class="dep-closebtn">
<svg class="icon icon-cross "><use xlink:href="symbol-defs.svg#icon-cross"></use></svg>
</button>

<div class="thm" id="def:has_large_differences" style="display: none">
<div class="thm_thmheading">
<span class="definition_thmcaption">
Definition
</span>
<span class="definition_thmlabel">11</span></div>
<div class="thm_thmcontent"><p>An ordered semigroup \(S\) has <b class="bfseries">large differences</b> if for all \(a,b\in S\), the two following implications hold </p>
<ul class="itemize">
<li><p>if \(a\) is positive and \(a{\lt}b\), then there exists \(c\in S\) and \(n\in \mathbb {N}^+\) such that \(c\) is Archimedean with respect to \(a\) and \(a^n*c \le b^n\) </p>
</li>
<li><p>if \(a\) is negative and \(b {\lt} a\), then there exists \(c\in S\) and \(n\in \mathbb {N}^+\) such that \(c\) is Archimedean with respect to \(a\) and \(a^n*c \ge b^n\) </p>
</li>
</ul>
</div>

<a class="latex_link" href="index.html#def:has_large_differences">LaTeX</a>


<a class="lean_link lean_decl" href="https://ericluap.github.io/OrderedSemigroups/docs/find/#doc/has_large_differences">Lean</a>




</div>

</div>
Expand Down Expand Up @@ -659,7 +695,7 @@ <h1 id="doc_title">Dependencies</h1>
.width(width)
.height(height)
.fit(true)
.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]; non_anomalous_comm_and_arch [color=green, fillcolor="#A3D6FF", label=non_anomalous_comm_and_arch, 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]; a0000000019 [color=blue, fillcolor="#A3D6FF", label=a0000000019, shape=ellipse, style=filled]; "def:arch_wrt" -> a0000000019 [style=dashed]; "def:arch" -> non_arch_anomalous [style=dashed]; "def:arch" -> non_anomalous_comm_and_arch [style=dashed]; "def:anomalous_pair" [color=green, fillcolor="#B0ECA3", label=anomalous_pair, shape=box, style=filled]; "def:anomalous_pair" -> non_arch_anomalous [style=dashed]; "def:anomalous_pair" -> non_anomalous_comm_and_arch [style=dashed]; "def:anomalous_pair" -> a0000000019 [style=dashed];}`)
.renderDot(`strict digraph "" { graph [bgcolor=transparent]; node [label="\N", penwidth=1.8 ]; edge [arrowhead=vee]; "thm:comm_ineq" [color=green, fillcolor="#A3D6FF", label=comm_ineq, shape=ellipse, style=filled]; non_anomalous_comm_and_arch [color=green, fillcolor="#A3D6FF", label=non_anomalous_comm_and_arch, shape=ellipse, style=filled]; "def:OrderedSemigroup" [color=green, fillcolor="#B0ECA3", label=OrderedSemigroup, shape=box, style=filled]; "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:one" [color=green, fillcolor="#B0ECA3", label=one, shape=box, style=filled]; "def:OrderedSemigroup" -> "def:one" [style=dashed]; "def:OrderedCancelSemigroup" [color=green, fillcolor="#B0ECA3", label=OrderedCancelSemigroup, shape=box, style=filled]; "def:OrderedSemigroup" -> "def:OrderedCancelSemigroup" [style=dashed]; "def:negative" [color=green, fillcolor="#B0ECA3", label=negative, shape=box, style=filled]; "def:OrderedSemigroup" -> "def:negative" [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]; "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:arch_wrt" [color=green, fillcolor="#B0ECA3", label=arch_wrt, shape=box, style=filled]; "def:positive" -> "def:arch_wrt" [style=dashed]; "lem:right_forall" [color=green, label=right_forall, shape=ellipse]; "def:positive" -> "lem:right_forall" [style=dashed]; "def:one" -> "thm:pos_neg_or_one" [style=dashed]; "def:one" -> "lem:right_forall" [style=dashed]; "def:arch" [color=green, fillcolor="#B0ECA3", label=arch, shape=box, style=filled]; "def:one" -> "def:arch" [style=dashed]; "def:LinearOrderedCancelSemigroup" [color=green, fillcolor="#B0ECA3", label=LinearOrderedCancelSemigroup, shape=box, style=filled]; "def:OrderedCancelSemigroup" -> "def:LinearOrderedCancelSemigroup" [style=dashed]; "def:negative" -> "thm:pos_neg_or_one" [style=dashed]; "def:negative" -> "thm:neg_lt_pos" [style=dashed]; "def:negative" -> "def:arch_wrt" [style=dashed]; "def:negative" -> "lem:right_forall" [style=dashed]; "def:arch_wrt" -> "def:arch" [style=dashed]; a0000000019 [color=green, fillcolor="#A3D6FF", label=a0000000019, shape=ellipse, style=filled]; "def:arch_wrt" -> a0000000019 [style=dashed]; "def:arch" -> non_anomalous_comm_and_arch [style=dashed]; non_arch_anomalous [color=green, fillcolor="#A3D6FF", label=non_arch_anomalous, shape=ellipse, style=filled]; "def:arch" -> non_arch_anomalous [style=dashed]; "def:LinearOrderedCancelSemigroup" -> "thm:pos_neg_or_one" [style=dashed]; "def:anomalous_pair" [color=green, fillcolor="#B0ECA3", label=anomalous_pair, shape=box, style=filled]; "def:anomalous_pair" -> non_anomalous_comm_and_arch [style=dashed]; "def:anomalous_pair" -> a0000000019 [style=dashed]; "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]; "def:has_large_differences" [color=green, fillcolor="#B0ECA3", label=has_large_differences, shape=box, style=filled]; "def:has_large_differences" -> a0000000019 [style=dashed];}`)
.on("end", interactive);

latexLabelEscaper = function(label) {
Expand Down
74 changes: 72 additions & 2 deletions blueprint/web/index.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1197,6 +1197,55 @@ <h1>Lean declarations</h1>

</div>
</div>
<div class="definition_thmwrapper theorem-style-definition" id="def:has_large_differences">
<div class="definition_thmheading">
<span class="definition_thmcaption">
Definition
</span>
<span class="definition_thmlabel">11</span>
<div class="thm_header_extras">


✓
</div>
<div class="thm_header_hidden_extras">

<a class="icon proof" href="index.html#def:has_large_differences">#</a>



<button class="modal lean">L∃∀N</button>
<div class="modal-container">
<div class="modal-content">
<header>
<h1>Lean declarations</h1>
<button class="closebtn"><svg class="icon icon-cross "><use xlink:href="symbol-defs.svg#icon-cross"></use></svg>
</button>
</header>

<ul class="uses">

<li><a href="https://ericluap.github.io/OrderedSemigroups/docs/find/#doc/has_large_differences" class="lean_decl">has_large_differences</a></li>

</ul>

</div>
</div>


</div>
</div>
<div class="definition_thmcontent">
<p>An ordered semigroup \(S\) has <b class="bfseries">large differences</b> if for all \(a,b\in S\), the two following implications hold </p>
<ul class="itemize">
<li><p>if \(a\) is positive and \(a{\lt}b\), then there exists \(c\in S\) and \(n\in \mathbb {N}^+\) such that \(c\) is Archimedean with respect to \(a\) and \(a^n*c \le b^n\) </p>
</li>
<li><p>if \(a\) is negative and \(b {\lt} a\), then there exists \(c\in S\) and \(n\in \mathbb {N}^+\) such that \(c\) is Archimedean with respect to \(a\) and \(a^n*c \ge b^n\) </p>
</li>
</ul>

</div>
</div>
<div class="theorem_thmwrapper theorem-style-plain" id="a0000000019">
<div class="theorem_thmheading">
<span class="theorem_thmcaption">
Expand Down Expand Up @@ -1230,17 +1279,38 @@ <h1>Uses</h1>

<li><a href="index.html#def:anomalous_pair">Definition 10</a></li>

<li><a href="index.html#def:has_large_differences">Definition 11</a></li>

</ul>

</div>
</div>



<button class="modal lean">L∃∀N</button>
<div class="modal-container">
<div class="modal-content">
<header>
<h1>Lean declarations</h1>
<button class="closebtn"><svg class="icon icon-cross "><use xlink:href="symbol-defs.svg#icon-cross"></use></svg>
</button>
</header>

<ul class="uses">

<li><a href="https://ericluap.github.io/OrderedSemigroups/docs/find/#doc/not_anomalous_iff_large_difference" class="lean_decl">not_anomalous_iff_large_difference</a></li>

</ul>

</div>
</div>


</div>
</div>
<div class="theorem_thmcontent">
<p> In a linear ordered cancel semigroup \(S\), there are no anomalous pairs if and only if for any two elements \(a,b\in S\), if \(a\) and \(b\) are positive and \(a {\lt} b\), then there exists an \(n \in \mathbb {N}^+\) and a \(c\in S\) that is Archimedean with respect to \(a\) such that \(a^n * c \le b^n\), or if \(a\) and \(b\) are negative and \(b {\lt} a\), then there exists an \(n\in \mathbb {N}^+\) and a \(c\in S\) that is Archimedean with respect to \(a\) such that \(a^n *c \ge b^n\). </p>
<p> In a linear ordered cancel semigroup \(S\), there are no anomalous pairs if and only if there are large differences. </p>

</div>
</div>
Expand All @@ -1264,7 +1334,7 @@ <h1>Uses</h1>
\[ c^n * (a^m)^n \le (a^m*c)^n \le (b^m)^n \]
</div>
<p> holds. </p>
<p>Since \(c\) is Archimedean with respect to \(a\), there exists an \(N\) such that for all \(n {\gt} N\), \(a {\lt} c^n\). Thus, for any \(n \ge N\), we get from the previous relations that </p>
<p>Since \(c\) is Archimedean with respect to \(a\), there exists an \(N\) such that for all \(n \ge N\), \(a {\lt} c^n\). Thus, for any \(n \ge N\), we get from the previous relations that </p>
<div class="displaymath" id="a0000000023">
\[ a^{mn + 1} \le b^{mn} \]
</div>
Expand Down

0 comments on commit b860c21

Please sign in to comment.