p-adic expansions

DefinitionDigits of a p-adic integer#✓fully proved

Let \(p\) be a prime and \(a \in \mathbb{Z}_p\), and for each \(n \ge 0\) let \(a_n\) be the unique natural number with \(a_n < p^n\) and \(a \equiv a_n \pmod{p^n \mathbb{Z}_p}\). The \(n\)-th \(p\)-adic digit of \(a\) is the natural number \((a_{n+1} - a_n)/p^n\).

Since \(a_n \le a_{n+1}\) and \(p^n\) divides \(a_{n+1} - a_n\), this quotient is exact.

noncomputable def padicDigit (a : ℤ_[p]) (n : Nat) : Nat :=
  (a.appr (n + 1) - a.appr n) / p ^ n

Used by 10

Used byApproximations as sums of p-adic digits · One-step reconstruction from p-adic digits · \(p\)-adic digits determine a \(p\)-adic integer · Existence of a \(p\)-adic integer with prescribed digits · Existence and uniqueness of \(p\)-adic integers with prescribed digits · p-adic digits are less than p · p-adic digits measure the gaps between approximations · p-adic expansion · The \(p\)-adic expansion map is surjective · Terms of the p-adic expansion are the digits

Theoremp-adic digits are less than p#✓fully proved

Let \(p\) be a prime and \(a \in \mathbb{Z}_p\). For every \(n \ge 0\), the \(n\)-th \(p\)-adic digit of \(a\) is strictly less than \(p\).

theorem padicDigit_lt (a : ℤ_[p]) (n : Nat) : padicDigit a n < p

Uses 1 · Used by 1

Statement usesDigits of a p-adic integer

Used byp-adic expansion

Definitionp-adic expansion#✓fully proved

Let \(p\) be a prime and \(a \in \mathbb{Z}_p\). The \(p\)-adic expansion of \(a\) is the sequence whose \(n\)-th term is the \(n\)-th \(p\)-adic digit of \(a\), viewed as an element of \(\{0, 1, \dots, p - 1\}\).

noncomputable def padicExpansion (a : ℤ_[p]) (n : Nat) : Fin p :=
  ⟨padicDigit a n, padicDigit_lt a n⟩

Uses 2 · Used by 6

Statement usesDigits of a p-adic integer · p-adic digits are less than p

Used byApproximations as truncations of the p-adic expansion · One-step reconstruction from the p-adic expansion · The \(p\)-adic expansion map is bijective · The \(p\)-adic expansion map is injective · The \(p\)-adic expansion map is surjective · Terms of the p-adic expansion are the digits

TheoremTerms of the p-adic expansion are the digits#✓fully proved

Let \(p\) be a prime and \(a \in \mathbb{Z}_p\). For every \(n \ge 0\), the \(n\)-th term of the \(p\)-adic expansion of \(a\), read as a natural number, is the \(n\)-th \(p\)-adic digit of \(a\).

@[simp] theorem padicExpansion_val (a : ℤ_[p]) (n : Nat) :
    (padicExpansion a n).val = padicDigit a n

Uses 2

Statement usesDigits of a p-adic integer · p-adic expansion

Theoremp-adic digits measure the gaps between approximations#✓fully proved

Let \(p\) be a prime and \(a \in \mathbb{Z}_p\), and for each \(n \ge 0\) let \(a_n\) be the unique natural number with \(a_n < p^n\) and \(a \equiv a_n \pmod{p^n \mathbb{Z}_p}\). For every \(n \ge 0\), the \(n\)-th \(p\)-adic digit \(d_n\) of \(a\) satisfies \(d_n p^n = a_{n+1} - a_n\).

Here \(a_n \le a_{n+1}\), so the difference is an honest natural number.

theorem padicDigit_mul_pow (a : ℤ_[p]) (n : Nat) :
    padicDigit a n * p ^ n = a.appr (n + 1) - a.appr n

Uses 1 · Used by 1

Statement usesDigits of a p-adic integer

Used byOne-step reconstruction from p-adic digits

TheoremOne-step reconstruction from p-adic digits#✓fully proved

Let \(p\) be a prime and \(a \in \mathbb{Z}_p\), and for each \(n \ge 0\) let \(a_n\) be the unique natural number with \(a_n < p^n\) and \(a \equiv a_n \pmod{p^n \mathbb{Z}_p}\). For every \(n \ge 0\), the \(n\)-th \(p\)-adic digit \(d_n\) of \(a\) satisfies \(a_{n+1} = a_n + d_n p^n\).

theorem appr_succ_eq (a : ℤ_[p]) (n : Nat) :
    a.appr (n + 1) = a.appr n + padicDigit a n * p ^ n

Uses 2 · Used by 3

Statement usesDigits of a p-adic integer

Proof usesp-adic digits measure the gaps between approximations

Used byApproximations as sums of p-adic digits · One-step reconstruction from the p-adic expansion · \(p\)-adic digits determine a \(p\)-adic integer

TheoremOne-step reconstruction from the p-adic expansion#✓fully proved

Let \(p\) be a prime and \(a \in \mathbb{Z}_p\), and for each \(n \ge 0\) let \(a_n\) be the unique natural number with \(a_n < p^n\) and \(a \equiv a_n \pmod{p^n \mathbb{Z}_p}\). For every \(n \ge 0\), \(a_{n+1} = a_n + e_n p^n\), where \(e_n\) is the \(n\)-th term of the \(p\)-adic expansion of \(a\), read as a natural number.

theorem appr_succ_eq_val (a : ℤ_[p]) (n : Nat) :
    a.appr (n + 1) = a.appr n + (padicExpansion a n).val * p ^ n

Uses 2

Statement usesp-adic expansion

Proof usesOne-step reconstruction from p-adic digits

TheoremApproximations as sums of p-adic digits#✓fully proved

Let \(p\) be a prime and \(a \in \mathbb{Z}_p\), and for each \(n \ge 0\) let \(a_n\) be the unique natural number with \(a_n < p^n\) and \(a \equiv a_n \pmod{p^n \mathbb{Z}_p}\). For every \(n \ge 0\), \(a_n = \sum_{k=0}^{n-1} d_k p^k\), where \(d_k\) is the \(k\)-th \(p\)-adic digit of \(a\).

theorem appr_eq_sum_padicDigit (a : ℤ_[p]) (n : Nat) :
    a.appr n = ∑ k ∈ Finset.range n, padicDigit a k * p ^ k

Uses 2 · Used by 1

Statement usesDigits of a p-adic integer

Proof usesOne-step reconstruction from p-adic digits

Used byApproximations as truncations of the p-adic expansion

TheoremApproximations as truncations of the p-adic expansion#✓fully proved

Let \(p\) be a prime and \(a \in \mathbb{Z}_p\), and for each \(n \ge 0\) let \(a_n\) be the unique natural number with \(a_n < p^n\) and \(a \equiv a_n \pmod{p^n \mathbb{Z}_p}\). For every \(n \ge 0\), \(a_n = \sum_{k=0}^{n-1} e_k p^k\), where \(e_k\) is the \(k\)-th term of the \(p\)-adic expansion of \(a\), read as a natural number.

theorem appr_eq_sum_expansion_val (a : ℤ_[p]) (n : Nat) :
    a.appr n = ∑ k ∈ Finset.range n, (padicExpansion a k).val * p ^ k

Uses 2

Statement usesp-adic expansion

Proof usesApproximations as sums of p-adic digits

Theorem\(p\)-adic digits determine a \(p\)-adic integer#✓fully proved

Let \(p\) be a prime. If two \(p\)-adic integers \(a, a' \in \mathbb{Z}_p\) have the same \(n\)-th \(p\)-adic digit for every \(n \ge 0\), then \(a = a'\).

theorem eq_of_padicDigit_eq {a a' : ℤ_[p]}
    (h : ∀ n, padicDigit a n = padicDigit a' n) : a = a'

Uses 2 · Used by 2

Statement usesDigits of a p-adic integer

Proof usesOne-step reconstruction from p-adic digits

Used byExistence and uniqueness of \(p\)-adic integers with prescribed digits · The \(p\)-adic expansion map is injective

TheoremExistence of a \(p\)-adic integer with prescribed digits#✓fully proved

Let \(p\) be a prime. For every sequence \((b_n)_{n \ge 0}\) of natural numbers with \(b_n < p\) for all \(n\), there is a \(p\)-adic integer \(a \in \mathbb{Z}_p\) whose \(n\)-th \(p\)-adic digit is \(b_n\) for every \(n \ge 0\).

The witness is the \(p\)-adic limit of the partial sums \(\sum_{k=0}^{n-1} b_k p^k\), which are its approximations modulo \(p^n\).

theorem exists_padicDigit_eq (b : ℕ → ℕ) (hb : ∀ n, b n < p) :
    ∃ a : ℤ_[p], ∀ n, padicDigit a n = b n

Uses 1 · Used by 2

Statement usesDigits of a p-adic integer

Used byExistence and uniqueness of \(p\)-adic integers with prescribed digits · The \(p\)-adic expansion map is surjective

TheoremExistence and uniqueness of \(p\)-adic integers with prescribed digits#✓fully proved

Let \(p\) be a prime. For every sequence \((b_n)_{n \ge 0}\) of natural numbers with \(b_n < p\) for all \(n\), there is exactly one \(p\)-adic integer \(a \in \mathbb{Z}_p\) whose \(n\)-th \(p\)-adic digit is \(b_n\) for every \(n \ge 0\).

theorem existsUnique_padicDigit_eq (b : ℕ → ℕ) (hb : ∀ n, b n < p) :
    ∃! a : ℤ_[p], ∀ n, padicDigit a n = b n

Sources

• ATLAS NumberTheoryI, Proposition 8.17.

Uses 3

Statement usesDigits of a p-adic integer

Proof uses\(p\)-adic digits determine a \(p\)-adic integer · Existence of a \(p\)-adic integer with prescribed digits

TheoremThe \(p\)-adic expansion map is injective#✓fully proved

Let \(p\) be a prime. If two \(p\)-adic integers \(a, a' \in \mathbb{Z}_p\) have the same \(p\)-adic expansion, then \(a = a'\).

theorem padicExpansion_injective :
    Function.Injective (padicExpansion (p := p))

Uses 2 · Used by 1

Statement usesp-adic expansion

Proof uses\(p\)-adic digits determine a \(p\)-adic integer

Used byThe \(p\)-adic expansion map is bijective

TheoremThe \(p\)-adic expansion map is surjective#✓fully proved

Let \(p\) be a prime. Every sequence \((b_n)_{n \ge 0}\) with values in \(\{0, 1, \dots, p - 1\}\) is the \(p\)-adic expansion of some \(p\)-adic integer \(a \in \mathbb{Z}_p\).

theorem padicExpansion_surjective :
    Function.Surjective (padicExpansion (p := p))

Uses 3 · Used by 1

Statement usesp-adic expansion

Proof usesExistence of a \(p\)-adic integer with prescribed digits · Digits of a p-adic integer

Used byThe \(p\)-adic expansion map is bijective

TheoremThe \(p\)-adic expansion map is bijective#✓fully proved

Let \(p\) be a prime. The map sending a \(p\)-adic integer \(a \in \mathbb{Z}_p\) to its \(p\)-adic expansion is a bijection from \(\mathbb{Z}_p\) onto the set of all sequences \((b_n)_{n \ge 0}\) with values in \(\{0, 1, \dots, p - 1\}\).

theorem padicExpansion_bijective :
    Function.Bijective (padicExpansion (p := p))

Sources

• ATLAS NumberTheoryI, Proposition 8.17.

Uses 3

Statement usesp-adic expansion

Proof usesThe \(p\)-adic expansion map is injective · The \(p\)-adic expansion map is surjective

15 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.