Ostrowski's theorem — flashcards
Every card the map can derive about Ostrowski's theorem — definitions, statements, attribution, and the edges it sits on.
Definitions 2
Define: The p-adic absolute value.
|x|_p = p^−v_p(x) for x ≠ 0, and |0|_p = 0. Divisibility by a high power of p is what it means to be small.
derived from st/def-absolute-value by the statement rule
Define: The absolute value axioms.
An absolute value on a field satisfies |x| = 0 exactly when x = 0, |xy| = |x||y|, and |x + y| ≤ |x| + |y|. Ostrowski's theorem is the statement that on ℚ these three conditions have far fewer solutions than one would guess.
derived from st/def-abs-axioms by the statement rule
Theorems 3
State: Ostrowski's theorem.
Every nontrivial absolute value on ℚ is equivalent either to the ordinary absolute value or to a p-adic one for exactly one prime p.
derived from st/ostrowski by the statement rule
State: The product formula.
For nonzero rational x, the ordinary absolute value times the product of all p-adic ones equals 1. Every place is accounted for, and no single one is privileged.
derived from st/product-formula by the statement rule
State: The places of ℚ do not compare.
Nearness in |·|_p and nearness in |·|_∞ are unrelated: by Ostrowski the absolute values are inequivalent, so neither induces any information about the other. Asking whether a p-adic number is larger than a real one has no content.
derived from st/incomparable-places by the statement rule
Names and dates 5
Ostrowski's theorem — who, and when?
Alexander Ostrowski, 1916.
derived from st/ostrowski by the attribution rule
The product formula — who, and when?
Artin and Whaples, 1945.
derived from st/product-formula by the attribution rule
The p-adic absolute value — who, and when?
Kurt Hensel, 1897.
derived from st/def-absolute-value by the attribution rule
The absolute value axioms — who, and when?
József Kürschák, 1912.
derived from st/def-abs-axioms by the attribution rule
The places of ℚ do not compare — who, and when?
Alexander Ostrowski, 1916.
derived from st/incomparable-places by the attribution rule
Formalisation 2
What is Ostrowski's theorem called in Mathlib?
Rat.AbsoluteValue.equiv_real_or_padic — Mathlib.NumberTheory.Ostrowski
derived from st/ostrowski by the binding rule
What is The p-adic absolute value called in Mathlib?
padicNorm — Mathlib.NumberTheory.Padics.PadicNorm
derived from st/def-absolute-value by the binding rule
Connections 6
Under the Degeneracy lens, how do Ostrowski's theorem and Peano arithmetic relate? [Degeneracy]
Being an integer is what survives every valuation at once — a condition imposed on a larger object, not a starting point that everything else is built up from.
derived from degeneracy:ostrowski→peano by the connection rule
Under the Degeneracy lens, how do Ostrowski's theorem and Differentiation & integration relate? [Degeneracy]
The reals are the completion at the infinite place. Being the ambient number system you happened to grow up with is a fact about pedagogy, not about ℝ.
derived from degeneracy:ostrowski→elementary-calculus by the connection rule
Ostrowski's theorem and p-adic numbers look like one thing. What separates them? [Forks]
Ostrowski's theorem says the branches are exactly ℝ and one ℚₚ per prime. This is the cleanest fork in mathematics: infinitely many consistent completions of the same starting object, and no principled reason to privilege the real one.
derived from forks:ostrowski→p-adic-numbers by the connection rule
Ostrowski's theorem and Differentiation & integration look like one thing. What separates them? [Forks]
Ordinary analysis is what you get by taking the one branch we happen to live on. Naming it a branch rather than the default is the whole point of the lens.
derived from forks:ostrowski→elementary-calculus by the connection rule
In Mathlib, what is the import relation between Ostrowski's theorem and Differentiation & integration? [Dependency (Mathlib)]
`Mathlib.NumberTheory.Ostrowski` imports `Mathlib.Analysis.AbsoluteValue.Equivalence`, `Mathlib.Analysis.SpecialFunctions.Log.Base`, `Mathlib.Analysis.SpecialFunctions.Pow.Continuity`. Read off Mathlib/NumberTheory/Ostrowski.html. No human asserted this edge.
derived from dependency:ostrowski→elementary-calculus by the connection rule
In Mathlib, what is the import relation between Ostrowski's theorem and p-adic numbers? [Dependency (Mathlib)]
`Mathlib.NumberTheory.Ostrowski` imports `Mathlib.NumberTheory.Padics.PadicNorm`. Read off Mathlib/NumberTheory/Ostrowski.html. No human asserted this edge.
derived from dependency:ostrowski→p-adic-numbers by the connection rule
Concepts 1
What is Ostrowski's theorem, in one sentence?
Every absolute value on ℚ is equivalent to the ordinary one or to a p-adic one. This is the fork itself: it says exactly what the branches are and that there are no others.
derived from ostrowski by the concept rule