Topological sums and complex powers

Stream: Is there code for X?

[Michael Stoll]

I'm trying to produce a proof of

import Mathlib

open LSeries Complex

open Filter in
lemma LSeries_limit {f : ℕ → ℂ} {n : ℕ} (h : ∀ m ≤ n, f m = 0) (ha : abscissaOfAbsConv f < ⊤):
    Tendsto (fun x : ℝ ↦ ((n + 1) ^ (x : ℂ)) * LSeries f x) atTop (nhds (f (n + 1))) := sorry

(which is the main ingredient to then prove

/-- The `LSeries` of `f` is zero if and only if either `f = 0`
or the L-series converges nowhere. -/
lemma LSeries_eq_zero_iff {f : ℕ → ℂ} (hf : f 0 = 0) :
    LSeries f = 0 ↔ f = 0 ∨ abscissaOfAbsConv f = ⊤ := sorry

from which it easily follows that a converging L-series determines its coefficients).

But I find it very painful.

One problem I managed to solve, but with a rather ugly proof, is

import Mathlib

example (m n : ℕ) (z : ℂ) (x : ℝ) :
    (n + 1) ^ (x : ℂ) * (z / m ^ (x : ℂ)) = z / (m / (n + 1)) ^ (x : ℂ) := by
  sorry

Am I missing something here?

Another thing that would be helpful is a version of docs#tendsto_tsum_of_dominated_convergence where the bound needs to hold only eventually instead of everywhere.

[Michael Stoll]

E.g., I can do this:

import Mathlib

open Filter in
lemma foo {f : ℝ → ℕ → ℂ} {x : ℝ} (hx : Summable (f x)) (hb : ∀ y ≥ x, ∀ n, ‖f y n‖ ≤ ‖f x n‖)
    (hc : ∀ n, Tendsto (f · n) atTop (nhds 0)) :
    Tendsto (fun x ↦ tsum (f x)) atTop (nhds 0) := by
  rw [show (0 : ℂ) = tsum (fun _ : ℕ ↦ 0) by simp]
  refine tendsto_tsum_of_dominated_convergence hx.norm hc fun y n ↦ hb y ?_ n
  -- stuck here, goal is `y ≥ x`
  sorry

[Terence Tao]

One can split the L-series in the regimes $m \leq (n+1)^2$ and $m > (n+1)^2$. The first regime is a finite sum and should be straightforward. For the tail, use $(n+1)^{x} / m^{x} \leq 1 / m^{x/2}$ to get domination once $x$ is non-negative and also at least twice the abscissa of convergence.

[Michael Stoll]

This does not solve the problem since the result that is in Mathlib requires to show the bound for all $x$. Your argument still imposes a lower bound on $x$.

[Michael Stoll]

I can probably work around that by using a piecewise defined function that is zero when y < x (using notation as in foo above) and equal to f otherwise, applying docs#tendsto_tsum_of_dominated_convergence to that, and using a suitable congruence lemma (that reduces to eventual equality). But this is a bit ugly...

[Anatole Dedecker]

Would #11236 solve your issues ?

[Eric Wieser]

(just sent that one to bors, since it had David's backing and the code looks fine)

[Michael Stoll]

Thanks! This is exeactly what I need for this part of the problem.