From b860c2101d57c53ac63a2b71715705e4c7c08adc Mon Sep 17 00:00:00 2001 From: Eric P Date: Sun, 8 Sep 2024 12:31:16 -0700 Subject: [PATCH] Add large difference definition to blueprint --- OrderedSemigroups/Archimedean.lean | 6 +-- blueprint/lean_decls | 4 +- blueprint/src/content.tex | 24 ++++++--- blueprint/src/web.paux | Bin 1962 -> 2056 bytes blueprint/web/dep_graph_document.html | 42 +++++++++++++-- blueprint/web/index.html | 74 +++++++++++++++++++++++++- 6 files changed, 133 insertions(+), 17 deletions(-) diff --git a/OrderedSemigroups/Archimedean.lean b/OrderedSemigroups/Archimedean.lean index 2dc2c47..a1a81fa 100644 --- a/OrderedSemigroups/Archimedean.lean +++ b/OrderedSemigroups/Archimedean.lean @@ -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 @@ -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 diff --git a/blueprint/lean_decls b/blueprint/lean_decls index 0d9cbb7..d963b6c 100644 --- a/blueprint/lean_decls +++ b/blueprint/lean_decls @@ -18,4 +18,6 @@ is_archimedean_wrt is_archimedean anomalous_pair non_archimedean_anomalous_pair -not_anomalous_comm_and_arch \ No newline at end of file +not_anomalous_comm_and_arch +has_large_differences +not_anomalous_iff_large_difference \ No newline at end of file diff --git a/blueprint/src/content.tex b/blueprint/src/content.tex index ce7b580..cab0470 100644 --- a/blueprint/src/content.tex +++ b/blueprint/src/content.tex @@ -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 $aUX{kl2dC958Q);JZWXSa} r85&N>P{`oOP|TQ}p`5|jqmr4Il3JmcQIeaZj9YW-l*TEgrNw#x{h2Bt delta 17 YcmeAWSjErMz%q6IMwZ3w%%#P805ZY_h5!Hn diff --git a/blueprint/web/dep_graph_document.html b/blueprint/web/dep_graph_document.html index 4516207..2980a1a 100644 --- a/blueprint/web/dep_graph_document.html +++ b/blueprint/web/dep_graph_document.html @@ -73,13 +73,13 @@

Dependencies

Theorem 5 -

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\).

+

In a linear ordered cancel semigroup \(S\), there are no anomalous pairs if and only if there are large differences.

LaTeX - + Lean @@ -179,6 +179,42 @@

Dependencies

+
+ + + + + + +
+
+ + +
@@ -659,7 +695,7 @@

Dependencies

.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) { diff --git a/blueprint/web/index.html b/blueprint/web/index.html index a20752d..9b9c5b0 100644 --- a/blueprint/web/index.html +++ b/blueprint/web/index.html @@ -1197,6 +1197,55 @@

Lean declarations

+
+
+ + Definition + + 11 +
+ + + ✓ +
+
+ + # + + + + +
+
+
+

Lean declarations

+ +
+ + + +
+
+ + +
+
+
+

An ordered semigroup \(S\) has large differences if for all \(a,b\in S\), the two following implications hold

+
    +

  • 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\)

    +
    • +

  • 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\)

    +
    • +
+ +
+
@@ -1230,6 +1279,8 @@

Uses

  • Definition 10
    • +
  • Definition 11
    • +
    @@ -1237,10 +1288,29 @@

    Uses

    + +
    +
    +
    +

    Lean declarations

    + +
    + + + +
    +
    + +
    -

    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\).

    +

    In a linear ordered cancel semigroup \(S\), there are no anomalous pairs if and only if there are large differences.

    @@ -1264,7 +1334,7 @@

    Uses

    \[ c^n * (a^m)^n \le (a^m*c)^n \le (b^m)^n \]

    holds.

    -

    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

    +

    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

    \[ a^{mn + 1} \le b^{mn} \]