Multiplicative functions with a common prime-power recurrence

A Hecke eigensystem is multiplicative and satisfies, at every prime p, the recurrence

a (p ^ (r + 2)) = a p * a (p ^ (r + 1)) - w p * a (p ^ r),

whose weight w p depends on the level and weight but not on the eigenform. This file records what that shared recurrence buys: such a function is determined by its values at the primes alone, so two of them that agree at every prime are equal.

Distinct such functions are therefore linearly independent. That is the arithmetic half of multiplicity one for Hecke eigenforms: eigenforms with different eigenvalue systems cannot cancel each other, whatever the coefficients. It is stated twice, because the two forms suit different consumers: pointwise, as "a relation ∑ᵢ cᵢ · Gᵢ n = 0 holding for every n ≥ 1 forces every coefficient to vanish", and as LinearIndependent R G. The two agree because an ArithmeticFunction vanishes at 0 by definition, so a module relation is exactly a pointwise relation at every n ≥ 1.

Main results

• ArithmeticFunction.eq_on_prime_pow_of_eq_on_primes_of_rec: the recurrence alone — no multiplicativity — propagates agreement from the primes to the prime powers.
• ArithmeticFunction.IsMultiplicative.eq_of_eq_on_primes_of_rec: two multiplicative functions obeying the same recurrence and agreeing at every prime are equal.
• ArithmeticFunction.IsMultiplicative.exists_prime_ne_of_ne_of_rec: contrapositively, two distinct such functions differ at some prime.
• ArithmeticFunction.IsMultiplicative.sum_mul_prime_eq_zero: multiplying a vanishing relation by the value at a prime leaves it vanishing.
• ArithmeticFunction.IsMultiplicative.eq_zero_of_sum_mul_eq_zero: the independence theorem, in its finite-support form, which is the elimination engine.
• ArithmeticFunction.IsMultiplicative.linearIndependent_of_rec: the same as LinearIndependent R G.

References

Ported from AINTLIB's LeanModularForms project (github.com/CBirkbeck/AINTLIB, commit 6d87d596a5372d5b122c47b7082d4c3afa9b7c3b, Apache 2.0), projects/LeanModularForms/LeanModularForms/HeckeRIngs/GL2/Newforms/MainLemmaProof.lean (eq_prime_powers_of_eq_primes_of_rec, support_eq_empty_of_pairwise_distinct_rec). That project works over a bare ℕ → ℂ with its own multiplicativity predicate; here the statements are over Mathlib's ArithmeticFunction.IsMultiplicative and an arbitrary commutative ring, with the independence results asking only that it have no zero divisors.

• F. Diamond and J. Shurman, A first course in modular forms, Theorem 5.8.2.
• Miyake, Modular forms, Theorem 4.6.12.

def ArithmeticFunction.HasPrimePowerRec {R : Type u_1} [CommRing R] (f : ArithmeticFunction R) (w : ℕ → R) : Prop

A common prime-power recurrence: f (p ^ (r + 2)) = f p * f (p ^ (r + 1)) - w p * f (p ^ r) at every prime p, with the weight w a function of the prime alone. For Hecke eigensystems w p = χ p * p ^ (k - 1), which is why the weight is shared by every eigenform of a given level and weight — and that sharing is what the results here need.

Equations

• f.HasPrimePowerRec w = ∀ (p : ℕ), Nat.Prime p → ∀ (r : ℕ), f (p ^ (r + 2)) = f p * f (p ^ (r + 1)) - w p * f (p ^ r)

theorem ArithmeticFunction.eq_on_prime_pow_of_eq_on_primes_of_rec {R : Type u_1} [CommRing R] {f g : ArithmeticFunction R} {w : ℕ → R} (h1 : f 1 = g 1) (hfr : f.HasPrimePowerRec w) (hgr : g.HasPrimePowerRec w) (hp : ∀ (p : ℕ), Nat.Prime p → f p = g p) {p : ℕ} (hprime : Nat.Prime p) (a : ℕ) : f (p ^ a) = g (p ^ a)

Prime values determine prime-power values, given a shared recurrence. Two functions obeying the same recurrence, agreeing at 1 and at every prime, agree at every prime power: the recurrence propagates the agreement upward from r = 0, 1. Multiplicativity is not needed — only the value at 1, which is where the induction starts.

theorem ArithmeticFunction.IsMultiplicative.eq_of_eq_on_primes_of_rec {R : Type u_1} [CommRing R] {f g : ArithmeticFunction R} {w : ℕ → R} (hf : f.IsMultiplicative) (hg : g.IsMultiplicative) (hfr : f.HasPrimePowerRec w) (hgr : g.HasPrimePowerRec w) (hp : ∀ (p : ℕ), Nat.Prime p → f p = g p) : f = g

Two multiplicative functions with a common recurrence agreeing at the primes are equal. ArithmeticFunction.IsMultiplicative.eq_iff_eq_on_prime_powers reduces equality to the prime powers, and eq_on_prime_pow_of_eq_on_primes_of_rec supplies those.

theorem ArithmeticFunction.IsMultiplicative.exists_prime_ne_of_ne_of_rec {R : Type u_1} [CommRing R] {f g : ArithmeticFunction R} {w : ℕ → R} (hf : f.IsMultiplicative) (hg : g.IsMultiplicative) (hfr : f.HasPrimePowerRec w) (hgr : g.HasPrimePowerRec w) (hne : f ≠ g) : ∃ (p : ℕ), Nat.Prime p ∧ f p ≠ g p

Distinct multiplicative functions with a common recurrence differ at a prime. The contrapositive of eq_of_eq_on_primes_of_rec, and the form the independence argument uses: it is what lets a minimal relation be cut down at a single prime.

theorem ArithmeticFunction.IsMultiplicative.sum_mul_prime_eq_zero {R : Type u_1} [CommRing R] {ι : Type u_2} {w : ℕ → R} {s : Finset ι} {G : ι → ArithmeticFunction R} (hmul : ∀ i ∈ s, (G i).IsMultiplicative) (hrec : ∀ i ∈ s, (G i).HasPrimePowerRec w) {c : ι → R} (hrel : ∀ (n : ℕ), 1 ≤ n → ∑ i ∈ s, c i * (G i) n = 0) {p : ℕ} (hp : Nat.Prime p) {n : ℕ} (hn : 1 ≤ n) : ∑ i ∈ s, c i * ((G i) p * (G i) n) = 0

Multiplying a vanishing relation by the value at a prime keeps it vanishing. If ∑ᵢ cᵢ · Gᵢ n = 0 for every n ≥ 1 then so is ∑ᵢ cᵢ · Gᵢ p · Gᵢ n: splitting n = p ^ a · m with p ∤ m, the shared recurrence rewrites Gᵢ p · Gᵢ (p ^ a) as Gᵢ (p ^ (a+1)) + w p · Gᵢ (p ^ (a-1)), and both resulting sums are instances of the original relation. This is the step that needs the weight to be shared by every i — otherwise w p could not be pulled out of the sum.

theorem ArithmeticFunction.IsMultiplicative.eq_zero_of_sum_mul_eq_zero {R : Type u_1} [CommRing R] {ι : Type u_2} [NoZeroDivisors R] {w : ℕ → R} {s : Finset ι} {G : ι → ArithmeticFunction R} (hmul : ∀ i ∈ s, (G i).IsMultiplicative) (hrec : ∀ i ∈ s, (G i).HasPrimePowerRec w) (hdist : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → G i ≠ G j) {c : ι → R} (hrel : ∀ (n : ℕ), 1 ≤ n → ∑ i ∈ s, c i * (G i) n = 0) (i : ι) : i ∈ s → c i = 0

Distinct multiplicative functions with a common prime-power recurrence are independent. If ∑ᵢ cᵢ · Gᵢ n = 0 for every n ≥ 1, where the Gᵢ are pairwise distinct, multiplicative and share the recurrence, then every cᵢ vanishes.

The textbook minimal-relation argument (Diamond–Shurman Theorem 5.8.2, Miyake Theorem 4.6.12). Take a relation whose support is as small as possible and pick r in it. If the support is {r} the relation at n = 1 reads c r = 0. Otherwise pick another i₀ in it and, by exists_prime_ne_of_ne_of_rec, a prime p₀ where G r and G i₀ differ; then cᵢ' := cᵢ · (Gᵢ p₀ − G r p₀) satisfies the same vanishing relation by sum_mul_prime_eq_zero, has c' r = 0 and c' i₀ ≠ 0, and so has strictly smaller nonempty support — contradicting minimality.

theorem ArithmeticFunction.IsMultiplicative.linearIndependent_of_rec {R : Type u_1} [CommRing R] {ι : Type u_2} [NoZeroDivisors R] {w : ℕ → R} {G : ι → ArithmeticFunction R} (hmul : ∀ (i : ι), (G i).IsMultiplicative) (hrec : ∀ (i : ι), (G i).HasPrimePowerRec w) (hdist : Function.Injective G) : LinearIndependent R G

Distinct multiplicative functions with a common prime-power recurrence are linearly independent, in Mathlib's sense: the family G is LinearIndependent R.

This is eq_zero_of_sum_mul_eq_zero read through linearIndependent_iff'. The two say the same thing, because an ArithmeticFunction vanishes at 0 by definition: a module relation ∑ᵢ gᵢ • Gᵢ = 0 is exactly a pointwise relation at every n ≥ 1. Which form is convenient depends on the consumer — the finite-support statement is the elimination engine, this one is what plugs into the linear-algebra API.