Morita's p-adic gamma function

DefinitionMorita's p-adic gamma values at natural numbers#✓fully proved

For a prime \(p\) and a natural number \(n\), this is the \(p\)-adic integer \((-1)^n \prod_{0 < j < n,\ p \nmid j} j\): \((-1)^n\) times the product of the positive integers below \(n\) that are not divisible by \(p\). At \(n = 0\) the product is empty and the value is \(1\). These are the finite values that Morita's \(p\)-adic gamma function interpolates.

noncomputable def moritaGammaNat (p n : ℕ) [Fact p.Prime] : PadicInt p :=
  (-1 : PadicInt p) ^ n *
    ∏ k ∈ (Finset.range n).filter (fun k => ¬p ∣ k), (k : PadicInt p)

Used by 2

Used byExistence and uniqueness of Morita's p-adic gamma function · Morita's p-adic gamma function

DefinitionMorita's p-adic gamma function#✓fully proved

For a prime \(p\), a continuous function \(\Gamma : \mathbb{Z}_p \to \mathbb{Z}_p\) is a Morita \(p\)-adic gamma function when \(\Gamma(0) = 1\), \(\Gamma(n)\) equals Morita's finite value \((-1)^n \prod_{0 < j < n,\ p \nmid j} j\) for every positive integer \(n\), and \(\Gamma(x)\) is a unit of \(\mathbb{Z}_p\) for every \(x \in \mathbb{Z}_p\).

def IsMoritaPadicGamma (p : ℕ) [Fact p.Prime]
    (Γ : C(PadicInt p, PadicInt p)) : Prop :=
  Γ 0 = 1 ∧
    (∀ n : ℕ, 0 < n → Γ (n : PadicInt p) = moritaGammaNat p n) ∧
    ∀ x : PadicInt p, IsUnit (Γ x)

Uses 1 · Used by 1

Statement usesMorita's p-adic gamma values at natural numbers

Used byExistence and uniqueness of Morita's p-adic gamma function

TheoremExistence and uniqueness of Morita's p-adic gamma function#✓fully proved

For every odd prime \(p\) there is exactly one continuous function \(\Gamma : \mathbb{Z}_p \to \mathbb{Z}_p\) that is a Morita \(p\)-adic gamma function, that is, \(\Gamma(0) = 1\), \(\Gamma(n) = (-1)^n \prod_{0 < j < n,\ p \nmid j} j\) for every positive integer \(n\), and \(\Gamma(x)\) is a unit of \(\mathbb{Z}_p\) for every \(x \in \mathbb{Z}_p\).

theorem existsUnique_moritaPadicGamma (p : ℕ) [Fact p.Prime] (hp : p ≠ 2) :
    ∃! Γ : C(PadicInt p, PadicInt p), IsMoritaPadicGamma p Γ

Sources

• Y. Morita, "A p-adic analogue of the Γ-function", J. Fac. Sci. Univ. Tokyo Sect. IA Math. 22 (1975), 255–266. The definition and extension theorem are reproduced in arXiv:2307.08940, arXiv:2307.10000, arXiv:2307.11982, arXiv:2310.15207, and arXiv:2311.03259.

Uses 2

Statement usesMorita's p-adic gamma function

Proof usesMorita's p-adic gamma values at natural numbers

3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.