Derivative of series

Stream: Is there code for X?

[Michael Stoll]

I'm looking for a HasDerivAt version of docs#hasFDerivAt_tsum_of_isPreconnected, but cannot find anything.
I have tried to switch over to FDerivs using docs#hasDerivAt_iff_hasFDerivAt, but then I run into the problem that I need to prove that ContinuousLinearMap.smulRight 1 (∑' (n : α), f' n x) = ∑' (n : α), ContinuousLinearMap.smulRight 1 (f' n x), at which point I'm getting stuck...

[Yury G. Kudryashov]

What Summable assumptions do you have?

[Michael Stoll]

I want to prove this:

open Complex

lemma hasDerivAt_sum_primes_log {f : ℕ → ℂ} {s : ℂ} (hs : 1 < s.re) (hbd : ∀ n, ‖f n‖ ≤ 1) :
    HasDerivAt (fun z : ℂ ↦ (∑' p : Nat.Primes, log (1 - f p * p ^ (-z))⁻¹))
      (- ∑' p : Nat.Primes, f p * (log (p : ℂ)) * p ^ (-s) / (1 - f p * p ^ (-s))) s := ...

Basically, I have summability of f n * n^(-s) for 1 < s.re, from which I can derive summability of log (1 - f n * p^(-s))⁻¹ using results from #9270.

[Yury G. Kudryashov]

If you have enough Summable assumptions, then you can use docs#ContinuousLinearMap.map_tsum with docs#ContinuousLinearMap.smulRightL

[Yury G. Kudryashov]

Another approach is to use docs#tsum_apply and a combination of docs#HasDerivAt.hasFDerivAt with docs#HasFDerivAt.hasDerivAt

[Michael Stoll]

I can try that (tomorrow or so; it is getting late here). But why is there no HasDerivAt version?

[Yury G. Kudryashov]

Because nobody PRd it.

[Michael Stoll]

docs#tsum_apply didn't work inside the tsum, probably since the thing summed over is not a function, but some kind of homomorphism.

[Yury G. Kudryashov]

@Sebastien Gouezel wrote this file.

[Michael Stoll]

Generally speaking, I find it rather difficult to prove statements about concrete functions, series etc.

[Yury G. Kudryashov]

Yes, once you start specializing general theorems to specific functions, you find a lot of gaps in the library.

[Michael Stoll]

...and it is a bit tough to have to fill them when you are just a non-specialist "customer" and don't know that part of the library well.

[Michael Stoll]

BTW, docs#ContinuousLinearMap.map_tsum does not seem to fit the situation; I'd need something like ContinuousLinearMap.smulRight_tsum.

[Yury G. Kudryashov]

You can apply it to smulRightL 1

[Anatole Dedecker]

I'll open a PR either soon or tomorrow specializing to deriv

[Anatole Dedecker]

#9295
I didn't touch the "higher derivatives" section because I'm too tired for it, but if someone wants to do it feel free to do so.

[Michael Stoll]

It is a really nice experience that you whine in the evening that something is missing in Mathlib, and when you get up the next day, it's there! Thanks @Yury G. Kudryashov @Anatole Dedecker !