Mahler coefficients of an even function

If G = ∑_{i ≤ N} c_i C(x, i) (x : ℤ, values in a commutative ring) is even, then for odd k ≤ N, 2 c_k = ∑_{k < i ≤ N} (−1)^i C(i − 1, i − k) c_i: compare coefficients in G(−x) = G(x), using C(−x, i) = (−1)^i ∑_k C(i − 1, i − k) C(x, k) (Vandermonde).

Main results

• LemaP2.choose_neg_vandermonde: the expansion of C(−x, i).
• LemaP2.mahler_unique: Mahler coefficients are determined by the values on ℕ.
• LemaP2.lemP_two: the statement above.

References

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

mahlerZ N c x = ∑_{i ≤ N} c_i C(x, i) for x : ℤ is ConjeturaC.mahlerZ.

theorem LemaP2.choose_neg_vandermonde (x i : ℕ) : Ring.choose (-↑x) i = (-1) ^ i * ∑ k ∈ Finset.range (i + 1), ↑((i - 1).choose (i - k) * x.choose k)

Vandermonde, as in the proof of lem:P(2). For x ∈ ℕ: C(-x, i) = (-1)^i ∑_{k ≤ i} C(i-1, i-k) C(x, k).

theorem LemaP2.mahler_unique {R : Type u_1} [CommRing R] (N : ℕ) (e : ℕ → R) (h : ∀ (x : ℕ), ∑ k ∈ Finset.range (N + 1), e k * ↑(x.choose k) = 0) (k : ℕ) : k ≤ N → e k = 0

Mahler coefficients are unique: if ∑_{k ≤ N} e_k C(x, k) = 0 for every x ∈ ℕ, then e_k = 0 for k ≤ N.

theorem LemaP2.mahlerZ_neg {R : Type u_1} [CommRing R] (N : ℕ) (c : ℕ → R) (x : ℕ) : ConjeturaC.mahlerZ N c (-↑x) = ∑ k ∈ Finset.range (N + 1), (∑ i ∈ Finset.Icc k N, (-1) ^ i * ↑((i - 1).choose (i - k)) * c i) * ↑(x.choose k)

G(-x) in Mahler form: its k-th coefficient is ∑_{k ≤ i ≤ N} (-1)^i C(i-1, i-k) c_i.

theorem LemaP2.lemP_two {R : Type u_1} [CommRing R] (N : ℕ) (c : ℕ → R) (heven : ∀ (x : ℤ), ConjeturaC.mahlerZ N c (-x) = ConjeturaC.mahlerZ N c x) {k : ℕ} (hk : Odd k) (hkN : k ≤ N) : 2 * c k = ∑ i ∈ Finset.Ioc k N, (-1) ^ i * ↑((i - 1).choose (i - k)) * c i

lem:P(2). If G = ∑_{i ≤ N} c_i C(x, i) is even on ℤ, then for every odd k ≤ N, 2 c_k = ∑_{k < i ≤ N} (-1)^i C(i-1, i-k) c_i. Valid over any commutative ring.

Controls