Switch limit and derivative given uniform convergence

Stream: Is there code for X?

[Kevin Wilson]

Hi there! In trying to clean up my proof on the density of squarefree numbers, I was trying to beef up some of the dirichlet series capacity of the library. To do so, I really need the following lemma or something very much like it:

import analysis.calculus.deriv

open filter metric

lemma swap_limit_and_derivative
(f : ℕ → ℝ → ℝ)
(f' : ℕ → ℝ → ℝ)
(g : ℝ → ℝ)
(g' : ℝ → ℝ)
(x r R : ℝ)
(hrR : r < R)
(hf : ∀ (n : ℕ), ∀ (y : ℝ), y ∈ ball x R → has_deriv_at (f n) (f' n y) y)
(hf' : ∀ (n : ℕ), continuous_on (f' n) (closed_ball x r))
(hfg : ∀ (y : ℝ), y ∈ closed_ball x r → tendsto (λ n, f n y) at_top (nhds (g y)))
(hfg' : tendsto_uniformly_on f' g' at_top (closed_ball x r)) :
∀ y : ℝ, y ∈ ball x r → has_deriv_at g (g' y) y :=
begin
  sorry,
end

Does anyone know if this lemma exists in the library? Thanks!

[Chris Birkbeck]

I'm currently trying to clean up and PR a similar complex version of this in #13500, but I don't know if this real version is already in mathlib.

[Kevin Wilson]

Nice! Also, I actually need the complex version for Dirichlet series, I just always work in R out of habit. It should be true for any normed field, so if it's there for R it's probably there for C :-)

For #13500 you need to be able to swap the integral and limit instead of a derivative and a limit, correct? (I'm not sure if Morera's Theorem is already proved in the library or not.) IIRC, they both eventually invoke the mean value theorem a couple of times. I'd be curious how you're handling that (as it seems a bit of a pain in the butt :-) ).

[Chris Birkbeck]

Yes exactly, the swapping the limit and integral is also a pain! (at least how I did it), but we have tendsto_integral_of_dominated_convergence which does the hard bit.

So I don't think there is a mean value theorem in the complex case (or at least what I think of the MVT to be saying, but in the real case there is, and so this is how I would do it), so I just commute the limit and integral and then show one can differentiate under the integral. The big inputs in this case come from the Cauchy integral formula.

[Kevin Wilson]

Oh my complex analysis is definitely rusty. I was thinking of the circle integral as a real integral of a vector valued function and so you should have a mean value inequality? But maybe that doesn't work or maybe it doesn't give you what you need to prove it. As I say, definitely a bit rusty!

Anyway, your theorem is the thing I actually need :-) So I shall just wait for that!