commit e4d1a5f6d708c34f2fd24b0bd6efc7a93a0c6e8b
parent 55177fdde1b807b42418f2d3be76a117af5a5200
Author: Alex Balgavy <alex@balgavy.eu>
Date: Thu, 10 Dec 2020 13:12:31 +0100
Update logical verification notes
Diffstat:
2 files changed, 26 insertions(+), 0 deletions(-)
diff --git a/content/logical-verification/Formalizing the p-adic numbers.md b/content/logical-verification/Formalizing the p-adic numbers.md
@@ -0,0 +1,25 @@
++++
+title = 'Formalizing the p-adic numbers'
++++
+# Formalizing the p-adic numbers
+The rational numbers Q are incomplete: the sets `{x ∈ Q | x² < 2}` and `{x ∈ Q | x² > 2}` partition Q, but both are open.
+
+A sequence is Cauchy if its entries eventually become arbitrarily close.
+
+Two sequences are equivalent if they eventually become arbitrarily close to each other: `s ∼ t` if for every positive `ε ∈ Q`, there exists and N such that for all `k ≥ N`, `|s_k - t_k| < ε`.
+
+equivalence relation: binary relation that is reflexive, symmetric, and transitive
+
+equivalence class: for `≈` as equivalence relation on S, the equivalence class of `a ∈ S` is `⟦a⟧ = {x ∈ S | a ≈ x}.`
+
+quotient: based on the above equivalence class, is the set `{⟦a⟧ | a ∈ S}` (so set of all equivalence classes)
+
+The set of real numbers is the set `{s : N → Q | s is Cauchy}`. It is the quotient of set of rational Cauchy sequences, with respect to equivalence. This is the completion of Q.
+
+## The p-adic norm
+An alternate absolute value.
+
+If `q ≠ 0`, the p-adic norm of rational `q` is `p ^ (-(padic_val_rat p q))`.
+If `q = 0`, p-adic norm of `q` is 0.
+
+The p-adic numbers are the Cauchy completion of Q with respect to the p-adic norm.
diff --git a/content/logical-verification/_index.md b/content/logical-verification/_index.md
@@ -20,3 +20,4 @@ There is a [Git repository](https://github.com/blanchette/logical_verification_2
- [Logical foundations of mathematics](logical-foundations-of-mathematics/)
- [Basic mathematical structures](basic-mathematical-structures/)
- [Rational and real numbers](rational-and-real-numbers/)
+- [Formalizing the p-adic numbers](formalizing-the-p-adic-numbers/)
