feat(NumberTheory/ArithmeticFunction/LFunction): arithmetic functions from power series (#36642)

This PR constructs arithmetic functions from power series. See #36189 for how this will ultimately be used to construct L-functions.

Co-authored-by: tb65536 <thomas.l.browning@gmail.com>

Author: tb65536

Mathlib/NumberTheory/ArithmeticFunction/Defs.lean

@@ -338,6 +338,11 @@ instance {S : Type*} [CommSemiring R] [Semiring S] [Algebra R S] :
   .ofModule (fun x f g ↦ ext fun n ↦ by simp [Finset.smul_sum])
     fun x f g ↦ ext fun n ↦ by simp [Finset.smul_sum]
 
+@[simp]
+theorem algebraMap_apply_one {S : Type*} [CommSemiring R] [Semiring S] [Algebra R S] (x : R) :
+    algebraMap R (ArithmeticFunction S) x 1 = algebraMap R S x := by
+  simp [Algebra.algebraMap_eq_smul_one]
+
 instance {M : Type*} [Semiring R] [AddCommMonoid M] [Module R M] :
     Module (ArithmeticFunction R) (ArithmeticFunction M) where
   one_smul := one_smul'

Mathlib/NumberTheory/ArithmeticFunction/LFunction.lean

@@ -6,6 +6,7 @@ Authors: Thomas Browning
 module
 
 public import Mathlib.NumberTheory.ArithmeticFunction.Defs
+public import Mathlib.RingTheory.PowerSeries.Basic
 public import Mathlib.RingTheory.PowerSeries.PiTopology
 public import Mathlib.RingTheory.PowerSeries.Substitution
 
@@ -16,13 +17,139 @@ This file constructs L-functions as formal Dirichlet series.
 
 ## Main definitions
 
+* `ArithmeticFunction.ofPowerSeries q f`: L-function `f(q⁻ˢ)` obtained from a power series `f(T)`.
 * `ArithmeticFunction.eulerProduct f`: the Euler product of a family `f i` of Dirichlet series.
+
+## Implementation notes
+
+We take the following route from polynomials to L-functions:
+* Starting from a polynomial in `T`, `PowerSeries.invOfUnit` gives the reciporical power series.
+* `ofPowerSeries` gives the local Euler factor as a formal Dirichlet series on powers of `q`.
+* `eulerProduct` gives the L-function as the formal product of these local Euler factors.
+* `LSeries` gives the L-function as an analytic function on the right half-plane of convergence.
+
+For example, the Riemann zeta function `ζ(s)` corresponds to taking `1 - T` at each prime `p`.
+
+For context, here is a diagram of the possible routes from polynomials to L-functions:
+
+                   T=q⁻ˢ                     s ∈ ℂ
+[polynomials in T] ----> [polynomials in q⁻ˢ] ----> [analytic function in s]
+          |                           |                           |
+          | (reciprocal)              | (reciprocal)              | (reciprocal)
+          v         T=q⁻ˢ             V          s ∈ ℂ            V
+[power series in T] ----> [power series in q⁻ˢ] ----> [analytic function in s] (the Euler factor)
+          |                           |                           |
+          | (product)                 | (product)                 | (product)
+          v                 T=q⁻ˢ     V               s ∈ ℂ       V
+[multivariate power series] ----> [Dirichlet series] ----> [L-function in s] (the Euler product)
+
+## TODO
+
+* If each `q` is a prime power, then `ArithmeticFunction.ofPowerSeries q f` is multiplicative.
 -/
 
 @[expose] public section
 
 namespace ArithmeticFunction
 
+section PowerSeries
+
+variable {R : Type*} [CommSemiring R]
+
+set_option backward.isDefEq.respectTransparency false in
+/-- The arithmetic function corresponding to the Dirichlet series `f(q⁻ˢ)`.
+For example, if `f = 1 + X + X² + ...` and `q = p`, then `f(q⁻ˢ) = 1 + p⁻ˢ + p⁻²ˢ + ...`.
+
+If `q ≤ 1` then `k ↦ q ^ k` is not injective, so we use the junk value `f.constantCoeff`. -/
+noncomputable def ofPowerSeries (q : ℕ) : PowerSeries R →ₐ[R] ArithmeticFunction R where
+  toFun f := if hq : 1 < q then
+    ⟨Function.extend (q ^ ·) (f.coeff ·) 0, by simp [Nat.ne_zero_of_lt hq]⟩ else
+      algebraMap R (ArithmeticFunction R) f.constantCoeff
+  map_zero' := by ext; split_ifs <;> simp [Function.extend]
+  -- note that `ofPowerSeries.map_one'` relies on the junk value `f.constantCoeff`.
+  map_one' := by
+    ext n
+    split_ifs with hq
+    · by_cases hn : ∃ k, q ^ k = n
+      · obtain ⟨a, rfl⟩ := hn
+        simp [(Nat.pow_right_injective hq).extend_apply, one_apply, hq.ne']
+      · simp [hn, one_apply_ne (fun H ↦ hn ⟨0, H.symm⟩)]
+    · simp
+  map_add' f g := by
+    ext n
+    split_ifs with hq
+    · by_cases h : ∃ a, q ^ a = n
+      · obtain ⟨a, rfl⟩ := h
+        simp [(Nat.pow_right_injective hq).extend_apply]
+      · simp [h]
+    · by_cases hn : n = 1 <;> simp [hn]
+  map_mul' f g := by
+    ext n
+    split_ifs with hq
+    · simp_rw [mul_apply, coe_mk]
+      by_cases hn : ∃ a, q ^ a = n
+      · obtain ⟨k, rfl⟩ := hn
+        rw [(Nat.pow_right_injective hq).extend_apply]
+        have hs : (Finset.antidiagonal k).map (.prodMap ⟨fun k ↦ q ^ k, Nat.pow_right_injective hq⟩
+            ⟨fun k ↦ q ^ k, Nat.pow_right_injective hq⟩) ⊆ (q ^ k).divisorsAntidiagonal :=
+          Nat.antidiagonal_map_subset_divisorsAntidiagonal_pow hq k
+        rw [PowerSeries.coeff_mul k f g, ← Finset.sum_subset hs]
+        · simp [(Nat.pow_right_injective hq).extend_apply]
+        · intro (a, b) hab h
+          by_cases ha : ∃ i, q ^ i = a
+          · by_cases hb : ∃ j, q ^ j = b
+            · obtain ⟨i, rfl⟩ := ha
+              obtain ⟨j, rfl⟩ := hb
+              rw [Nat.mem_divisorsAntidiagonal, ← pow_add, Nat.pow_right_inj hq] at hab
+              simp_rw [Finset.mem_map, not_exists, not_and, Finset.mem_antidiagonal] at h
+              simpa using h (i, j) hab.1
+            · rwa [mul_comm, Function.extend_apply', Pi.zero_apply, zero_mul]
+          · rwa [Function.extend_apply', Pi.zero_apply, zero_mul]
+      · rw [Function.extend_apply' _ _ _ hn, Pi.zero_apply, Finset.sum_eq_zero]
+        intro (a, b) hk
+        obtain ⟨hab, -⟩ := Nat.mem_divisorsAntidiagonal.mp hk
+        by_cases ha : ∃ i, q ^ i = a
+        · by_cases hb : ∃ j, q ^ j = b
+          · obtain ⟨i, rfl⟩ := ha
+            obtain ⟨j, rfl⟩ := hb
+            rw [← pow_add] at hab
+            exact (hn ⟨i + j, hab⟩).elim
+          · rwa [mul_comm, Function.extend_apply', Pi.zero_apply, zero_mul]
+        · rwa [Function.extend_apply', Pi.zero_apply, zero_mul]
+    · simp
+  commutes' x := by
+    ext n
+    split_ifs with hq
+    · simp only [Algebra.algebraMap_eq_smul_one, coe_mk]
+      by_cases hn : ∃ k, q ^ k = n
+      · obtain ⟨k, rfl⟩ := hn
+        simp [(Nat.pow_right_injective hq).extend_apply, one_apply, hq.ne']
+      · rw [Function.extend_apply' _ _ _ hn, Pi.zero_apply, smul_map, one_apply_ne, smul_zero]
+        contrapose! hn
+        exact ⟨0, by simp [hn]⟩
+    · simp
+
+theorem ofPowerSeries_apply {q : ℕ} (hq : 1 < q) (f : PowerSeries R) (n : ℕ) :
+    ofPowerSeries q f n = Function.extend (q ^ ·) (f.coeff ·) 0 n := by
+  simp [ofPowerSeries, dif_pos hq]
+
+theorem ofPowerSeries_apply_pow {q : ℕ} (hq : 1 < q) (f : PowerSeries R) (k : ℕ) :
+    ofPowerSeries q f (q ^ k) = f.coeff k := by
+  rw [ofPowerSeries_apply hq, (Nat.pow_right_injective hq).extend_apply]
+
+theorem ofPowerSeries_apply_zero (q : ℕ) (f : PowerSeries R) : ofPowerSeries q f 0 = 0 := by
+  simp
+
+@[simp]
+-- note that `ofPowerSeries_apply_one` relies on the junk value `f.constantCoeff`.
+theorem ofPowerSeries_apply_one (q : ℕ) (f : PowerSeries R) :
+    ofPowerSeries q f 1 = f.constantCoeff := by
+  by_cases hq : 1 < q
+  · rw [← pow_zero q, ofPowerSeries_apply_pow hq, PowerSeries.coeff_zero_eq_constantCoeff]
+  · simp [ofPowerSeries, dif_neg hq]
+
+end PowerSeries
+
 section EulerProduct
 
 open Filter

Mathlib/NumberTheory/Divisors.lean

@@ -10,6 +10,7 @@ public import Mathlib.Algebra.Order.BigOperators.Group.Finset
 public import Mathlib.Algebra.Order.Interval.Finset.SuccPred
 public import Mathlib.Algebra.Order.Ring.Int
 public import Mathlib.Algebra.Ring.CharZero
+public import Mathlib.Data.Finset.NatAntidiagonal
 public import Mathlib.Data.Nat.Cast.Order.Ring
 public import Mathlib.Data.Nat.PrimeFin
 public import Mathlib.Data.Nat.SuccPred
@@ -605,6 +606,14 @@ lemma divisorsAntidiagonal_eq_prod_filter_of_le {n N : ℕ} (n_ne_zero : n ≠ 0
   · intro ⟨⟨hn1, hn2⟩, hn3⟩
     exact ⟨hn3, n_ne_zero⟩
 
+/-- `Finset.antidiagonal k` embeds as a subset of `Nat.divisorsAntidiagonal (q ^ k)`. -/
+theorem antidiagonal_map_subset_divisorsAntidiagonal_pow {q : ℕ} (hq : 1 < q) (k : ℕ) :
+    letI ι : ℕ ↪ ℕ :=  ⟨fun k ↦ q ^ k, Nat.pow_right_injective hq⟩
+    (Finset.antidiagonal k).map (.prodMap ι ι) ⊆ (q ^ k).divisorsAntidiagonal := by
+  intro k hk
+  obtain ⟨i, hi, rfl⟩ := Finset.mem_map.mp hk
+  simp [Nat.mem_divisorsAntidiagonal, ← Finset.mem_antidiagonal.mp hi, pow_add, ne_zero_of_lt hq]
+
 end Nat
 
 namespace Int