The change of variable z ↦ ((1+p)^z − 1)/p is unitriangular in the Mahler basis

Let p be an odd prime, F(z) = ((1+p)^z − 1)/p and L = F⁻¹, as maps of ℤ/p^t. On functions ℤ/p^t → k with char k = p, the maps q ↦ q ∘ F and q ↦ q ∘ L are unitriangular in the Mahler basis C(z, i): C(F(z), i) and C(L(z), i) have Mahler degree i and leading coefficient 1. The proof uses (1+X)^{λ y + 1} = (1+X)((1+X)^λ)^y with λ = 1 + p, (1+X)^λ − 1 ≡ X + X^p + X^{p+1} (mod p), and F(z+1) = λ F(z) + 1; the statement for L comes from inverting the unitriangular relation.

Main results

• LemaLog.choose_F_nat, LemaLog.choose_Ft, LemaLog.choose_Lt: the Mahler expansions.
• LemaLog.Ft_bijective: F is a bijection of ℤ/p^t.
• LemaLog.lem_log_F, LemaLog.lem_log_L: the matrices of q ↦ q ∘ F and q ↦ q ∘ L in the basis ConjeturaC.chooseBasis are upper unitriangular.

References

• C. Marín, Reading Iwasawa λ-invariants from Mahler matrices modulo p: programs, data and Lean files, Zenodo (2026), doi:10.5281/zenodo.23085315.

Mahler-type combinations on any domain

def LemaLog.Low {α : Type u_1} {R : Type u_2} [CommRing R] (e : α → ℕ) (m : ℕ) (g : α → R) : Prop

g is a combination of C(e x, j), j < m (Mahler degree < m through e).

Equations

• LemaLog.Low e m g = ∃ (a : ℕ → R), ∀ (x : α), g x = ∑ j ∈ Finset.range m, a j * ↑((e x).choose j)

theorem LemaLog.Low.zero {α : Type u_1} {R : Type u_2} [CommRing R] {e : α → ℕ} (m : ℕ) : Low e m fun (x : α) => 0

theorem LemaLog.Low.add {α : Type u_1} {R : Type u_2} [CommRing R] {e : α → ℕ} {m : ℕ} {f g : α → R} (hf : Low e m f) (hg : Low e m g) : Low e m fun (x : α) => f x + g x

theorem LemaLog.Low.smul {α : Type u_1} {R : Type u_2} [CommRing R] {e : α → ℕ} {m : ℕ} (c : R) {f : α → R} (hf : Low e m f) : Low e m fun (x : α) => c * f x

theorem LemaLog.Low.neg {α : Type u_1} {R : Type u_2} [CommRing R] {e : α → ℕ} {m : ℕ} {f : α → R} (hf : Low e m f) : Low e m fun (x : α) => -f x

theorem LemaLog.Low.mono {α : Type u_1} {R : Type u_2} [CommRing R] {e : α → ℕ} {m m' : ℕ} (h : m ≤ m') {f : α → R} (hf : Low e m f) : Low e m' f

theorem LemaLog.Low.choose {α : Type u_1} {R : Type u_2} [CommRing R] {e : α → ℕ} {m j : ℕ} (h : j < m) : Low e m fun (x : α) => ↑((e x).choose j)

theorem LemaLog.Low.sum {α : Type u_1} {R : Type u_2} [CommRing R] {e : α → ℕ} {m n : ℕ} (c : ℕ → R) {g : ℕ → α → R} (hg : ∀ j < n, Low e m (g j)) : Low e m fun (x : α) => ∑ j ∈ Finset.range n, c j * g j x

The forward difference: an antidifference raises the degree by one

theorem LemaLog.low_of_diff {R : Type u_1} [CommRing R] {m : ℕ} (g : ℕ → R) (h0 : g 0 = 0) (hd : Low id m fun (z : ℕ) => g (z + 1) - g z) : Low id (m + 1) g

F on ℕ

def LemaLog.Fn (p : ℕ) : ℕ → ℕ

F on ℕ through its recursion F(0) = 0, F(z+1) = (1+p)F(z) + 1 (the identity F(z+1) = λF(z) + 1 of the proof).

Equations

• LemaLog.Fn p 0 = 0
• LemaLog.Fn p z.succ = (1 + p) * LemaLog.Fn p z + 1

theorem LemaLog.p_mul_Fn (p z : ℕ) : p * Fn p z + 1 = (1 + p) ^ z

F(z) = ((1+p)^z − 1)/p: p F(z) + 1 = (1+p)^z.

The generating-function step, modulo p

noncomputable def LemaLog.V (p : ℕ) : Polynomial (ZMod p)

V = X^{p−3} + X^{p−2}.

Equations

• LemaLog.V p = Polynomial.X ^ (p - 3) + Polynomial.X ^ (p - 2)

noncomputable def LemaLog.W (p : ℕ) : Polynomial (ZMod p)

W = 1 + X^{p−1} + X^p = 1 + X²V (for p ≥ 3).

Equations

• LemaLog.W p = 1 + Polynomial.X ^ 2 * LemaLog.V p

theorem LemaLog.X_add_one_pow_lam (p : ℕ) [hp : Fact (Nat.Prime p)] (hp3 : 3 ≤ p) : (Polynomial.X + 1) ^ (1 + p) = Polynomial.X * W p + 1

(1+X)^λ − 1 ≡ X + X^p + X^{p+1} = X·W (mod p), λ = 1 + p.

theorem LemaLog.W_pow (p k : ℕ) : ∃ (Q : Polynomial (ZMod p)), (Polynomial.X + 1) * W p ^ k = Polynomial.X + 1 + Polynomial.X ^ 2 * Q

(1+X)W^k = 1 + X + X²Q: the coefficients of X⁰ and X¹ are 1 (uses p − 1 ≥ 2).

theorem LemaLog.coeff_W_pow_zero (p k : ℕ) : ((Polynomial.X + 1) * W p ^ k).coeff 0 = 1

theorem LemaLog.coeff_W_pow_one (p k : ℕ) : ((Polynomial.X + 1) * W p ^ k).coeff 1 = 1

theorem LemaLog.stepA (p : ℕ) [hp : Fact (Nat.Prime p)] (hp3 : 3 ≤ p) (n : ℕ) : Low id n fun (y : ℕ) => ↑(((1 + p) * y + 1).choose (n + 1)) - ↑(y.choose (n + 1)) - ↑(y.choose n)

Step of the proof: C(λy+1, i) − C(y, i) ≡ C(y, i−1) + (lower degree) (mod p), with i = n + 1; the coefficients are c_j = [X^i](1+X)((1+X)^λ − 1)^j.

theorem LemaLog.Low.congr {α : Type u_1} {R : Type u_2} [CommRing R] {e : α → ℕ} {m : ℕ} {f g : α → R} (h : ∀ (x : α), f x = g x) (hf : Low e m f) : Low e m g

C(F(z), i) has Mahler degree i and leading coefficient 1 (on ℕ, mod p)

theorem LemaLog.choose_F_nat (p : ℕ) [Fact (Nat.Prime p)] (hp3 : 3 ≤ p) (i : ℕ) : Low id i fun (z : ℕ) => ↑((Fn p z).choose i) - ↑(z.choose i)

The induction of the proof: C(F(z), i) − C(z, i) is a combination of C(z, j), j < i, modulo p.

Transfer to ℤ/p^t: Lucas

theorem LemaLog.choose_mod_pow (p : ℕ) [Fact (Nat.Prime p)] {t k : ℕ} (hk : k < p ^ t) (n : ℕ) : ↑((n % p ^ t).choose k) = ↑(n.choose k)

C(n mod p^t, k) ≡ C(n, k) (mod p) for k < p^t (Lucas).

instance LemaLog.neZero_pow (p t : ℕ) [Fact (Nat.Prime p)] : NeZero (p ^ t)

NeZero (p^t).

def LemaLog.Ft (p t : ℕ) (z : ZMod (p ^ t)) : ZMod (p ^ t)

F on ℤ/p^t: z ↦ F(z̃) mod p^t with z̃ ∈ [0, p^t) the representative of z.

Equations

• LemaLog.Ft p t z = ↑(LemaLog.Fn p z.val)

theorem LemaLog.choose_Ft (p : ℕ) [Fact (Nat.Prime p)] (hp3 : 3 ≤ p) (t : ℕ) {i : ℕ} (hi : i < p ^ t) : Low ZMod.val i fun (z : ZMod (p ^ t)) => ↑((Ft p t z).val.choose i) - ↑(z.val.choose i)

C(F(z), i) − C(z, i), z ∈ ℤ/p^t, i < p^t, is a combination of C(z, j), j < i.

theorem LemaLog.Ft_bijective (p : ℕ) [Fact (Nat.Prime p)] (hp3 : 3 ≤ p) (t : ℕ) : Function.Bijective (Ft p t)

F is a bijection of ℤ/p^t (here deduced from the unitriangularity).

noncomputable def LemaLog.Lt (p : ℕ) [Fact (Nat.Prime p)] (hp3 : 3 ≤ p) (t : ℕ) : ZMod (p ^ t) → ZMod (p ^ t)

L = F⁻¹ on ℤ/p^t.

Equations

• LemaLog.Lt p hp3 t = ⇑(Equiv.ofBijective (LemaLog.Ft p t) ⋯).symm

theorem LemaLog.Ft_Lt (p : ℕ) [Fact (Nat.Prime p)] (hp3 : 3 ≤ p) (t : ℕ) (z : ZMod (p ^ t)) : Ft p t (Lt p hp3 t z) = z

theorem LemaLog.Lt_Ft (p : ℕ) [Fact (Nat.Prime p)] (hp3 : 3 ≤ p) (t : ℕ) (z : ZMod (p ^ t)) : Lt p hp3 t (Ft p t z) = z

theorem LemaLog.choose_Lt (p : ℕ) [Fact (Nat.Prime p)] (hp3 : 3 ≤ p) (t : ℕ) {i : ℕ} (hi : i < p ^ t) : Low ZMod.val i fun (z : ZMod (p ^ t)) => ↑((Lt p hp3 t z).val.choose i) - ↑(z.val.choose i)

C(L(z), i) − C(z, i), i < p^t, is a combination of C(z, j), j < i ("by inverting the unitriangular matrix").

The Mahler basis of ℤ/N → k (ConjeturaC.chooseBasis) and the matrices of q ↦ q∘F,

q ↦ q∘L

theorem LemaLog.column_unitri {p N : ℕ} [NeZero N] (k : Type u_1) [Field k] [CharP k p] (G : ZMod N → ZMod N) (i : Fin N) (h : Low ZMod.val ↑i fun (z : ZMod N) => ↑((G z).val.choose ↑i) - ↑(z.val.choose ↑i)) : ((ConjeturaC.chooseBasis N k).repr (ConjeturaC.chooseFun N k i ∘ G)) i = 1 ∧ ∀ (j : Fin N), i < j → ((ConjeturaC.chooseBasis N k).repr (ConjeturaC.chooseFun N k i ∘ G)) j = 0

If C(G(z), i) − C(z, i) is a combination of C(z, j), j < i (mod p), the column i of the matrix of q ↦ q∘G in the Mahler basis has 1 on the diagonal and 0 below it.

theorem LemaLog.lem_log_F (p : ℕ) [Fact (Nat.Prime p)] (hp3 : 3 ≤ p) (t : ℕ) (k : Type u_1) [Field k] [CharP k p] (i j : Fin (p ^ t)) : (LinearMap.toMatrix (ConjeturaC.chooseBasis (p ^ t) k) (ConjeturaC.chooseBasis (p ^ t) k)) (LinearMap.funLeft k k (Ft p t)) i i = 1 ∧ (i < j → (LinearMap.toMatrix (ConjeturaC.chooseBasis (p ^ t) k) (ConjeturaC.chooseBasis (p ^ t) k)) (LinearMap.funLeft k k (Ft p t)) j i = 0)

lem:log 2.1, map F. For every t, the matrix of q ↦ q∘F on functions ℤ/p^t → k (k a field of characteristic p, p ≥ 3) in the Mahler basis is unitriangular: its column i (the coordinates of C(F(z), i)) has 1 in row i and 0 in every row j > i.

theorem LemaLog.lem_log_L (p : ℕ) [Fact (Nat.Prime p)] (hp3 : 3 ≤ p) (t : ℕ) (k : Type u_1) [Field k] [CharP k p] (i j : Fin (p ^ t)) : (LinearMap.toMatrix (ConjeturaC.chooseBasis (p ^ t) k) (ConjeturaC.chooseBasis (p ^ t) k)) (LinearMap.funLeft k k (Lt p hp3 t)) i i = 1 ∧ (i < j → (LinearMap.toMatrix (ConjeturaC.chooseBasis (p ^ t) k) (ConjeturaC.chooseBasis (p ^ t) k)) (LinearMap.funLeft k k (Lt p hp3 t)) j i = 0)

lem:log 2.1, map L = F⁻¹. Same statement for q ↦ q∘L.

Controls