LSeries.term

Stream: PrimeNumberTheorem+

[Vincent Beffara]

Hi, I was trying to bump mathlib to get access to Fourier inversion and new lemmas about Fourier transform, but mathlib commit #ba66cf768d is breaking things because it says

noncomputable
def term (f : ℕ → ℂ) (s : ℂ) (n : ℕ) : ℂ :=
  if n = 0 then 0 else f n / n ^ s

while EulerProducts says

def LSeriesHasSum (f : ArithmeticFunction ℂ) (s a : ℂ) : Prop :=
  HasSum (fun (n : ℕ) => f n / n ^ s) a

which does not match. We should probably use LSeriesHasSum from mathlib, but that might be a bit painful. @Michael Stoll is the if n = 0 then 0 else really useful in your definition?

[Vincent Beffara]

Ah, should have updated all packages together, sorry.

[Vincent Beffara]

first_fourier in PNT does need to be updated though

[Michael Stoll]

I do my best to keep EulerProducts in sync with Mathlib, so in general it should work if you use the current version of EulerProducts. It is a moving target, though, as I'm in the process of getting a large part of it into Mathlib.

[Vincent Beffara]

Ok so I’m in the process of rewriting Wiener.lean to use LSeries.term and it is mostly working out well. The main issue is that you only define it for arithmetic functions with values in C but we need it with values in R sometimes.

[Michael Stoll]

I'm going to define notation

/-- We introduce notation `↗f` for `f` interpreted as a function `ℕ → ℂ`. -/
scoped[LSeries.notation] notation:max "↗" f:max => fun n : ℕ ↦ (f n : ℂ)

then you can write ↗fas an argument when f : ℕ → ℝ. This notation is already in EulerProducts.LSeries.

[Vincent Beffara]

Done here https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/pull/110