English
The L-function of the function k ↦ e(j·k) equals expZeta on the circle determined by j, provided not both j = 0 and s = 1.
Русский
L-функция для k ↦ e(jk) равна expZeta на окружности, соответствующей j, при условии, что не выполняются одновременно j = 0 и s = 1.
LaTeX
$$$$L(\lambda_j, s) = \expZeta (ZMod.toAddCircle(j))\!\left(s\right)\quad\text{ for } j \neq 0 \text{ or } s \neq 1.$$$$
Lean4
/-- The `LFunction` of the function `x ↦ e (j * x)`, where `e : ZMod N → ℂ` is the standard additive
character, is `expZeta (j / N)`.
Note this is not at all obvious from the definitions, and we prove it by analytic continuation
from the convergence range.
-/
theorem LFunction_stdAddChar_eq_expZeta (j : ZMod N) (s : ℂ) (hjs : j ≠ 0 ∨ s ≠ 1) :
LFunction (fun k ↦ 𝕖 (j * k)) s = expZeta (ZMod.toAddCircle j) s :=
by
let U := if j = 0 then {z : ℂ | z ≠ 1} else univ
let V :=
{z : ℂ | 1 < re z} -- convergence region
have hUo : IsOpen U := by
by_cases h : j = 0
· simpa only [h, ↓reduceIte, U] using isOpen_compl_singleton
· simp only [h, ↓reduceIte, isOpen_univ, U]
let f := LFunction (fun k ↦ stdAddChar (j * k))
let g := expZeta (toAddCircle j)
have hU {u} : u ∈ U ↔ u ≠ 1 ∨ j ≠ 0 := by simp only [mem_ite_univ_right, U];
tauto
-- hypotheses for uniqueness of analytic continuation
have hf : AnalyticOnNhd ℂ f U :=
by
refine DifferentiableOn.analyticOnNhd (fun u hu ↦ ?_) hUo
refine (differentiableAt_LFunction _ _ ((hU.mp hu).imp_right fun h ↦ ?_)).differentiableWithinAt
simp only [mul_comm j, AddChar.sum_mulShift _ (isPrimitive_stdAddChar _), h, ↓reduceIte, CharP.cast_eq_zero]
have hg : AnalyticOnNhd ℂ g U :=
by
refine DifferentiableOn.analyticOnNhd (fun u hu ↦ ?_) hUo
refine (differentiableAt_expZeta _ _ ((hU.mp hu).imp_right fun h ↦ ?_)).differentiableWithinAt
rwa [ne_eq, toAddCircle_eq_zero]
have hUc : IsPreconnected U := by
by_cases h : j = 0
· simpa only [h, ↓reduceIte, U] using (isConnected_compl_singleton_of_one_lt_rank (by simp) _).isPreconnected
· simpa only [h, ↓reduceIte, U] using isPreconnected_univ
have hV : V ∈ 𝓝 2 := (continuous_re.isOpen_preimage _ isOpen_Ioi).mem_nhds (by simp)
have hUmem : 2 ∈ U := by simp [U]
have hUmem' : s ∈ U := hU.mpr hjs.symm
refine hf.eqOn_of_preconnected_of_eventuallyEq hg hUc hUmem ?_ hUmem'
filter_upwards [hV] with z using LFunction_stdAddChar_eq_expZeta_of_one_lt_re _
