Having trouble taking a derivative

Stream: maths

[Mark Andrew Gerads]

It seems so simple, yet is so difficult in Lean. I may well have went in a wrong direction with the partial proof.

import analysis.special_functions.exponential

open classical complex asymptotics normed_space
open_locale classical big_operators nat

noncomputable
def ruesDiff (n:ℕ) (m:ℤ) (z:ℂ) : ℂ :=
  tsum (λ (k:ℕ), if ((k:ℤ)+m)%n=0 then z ^ k / k.factorial else 0)

lemma ruesDiffHasDeriv (n:ℕ) (m:ℤ) (z:ℂ) : has_deriv_at (ruesDiff n m) (ruesDiff n (m+1) z) z :=
begin
  rw [has_deriv_at_iff_is_o_nhds_zero],
  refine is_o_iff_forall_is_O_with.mpr _,
  intros c cGt0,
  rw [asymptotics.is_O_with, filter.eventually],
  simp only [algebra.id.smul_eq_mul, complex.norm_eq_abs],
  sorry,
end

[Heather Macbeth]

@Mark Andrew Gerads Are you sure you understand the paper proof?

[Heather Macbeth]

You might like to try writing it out carefully with, e.g., Corollary 6.2.13 in https://www.jirka.org/ra/realanal.pdf

[Mark Andrew Gerads]

This is basically the Taylor series for the exponential function, except some terms are zeroed out. I would just take the derivative of each term, and the terms not zeroed out move to the left 1 spot as they are differentiated.

[Heather Macbeth]

Right, that's not a proof.

[Mark Andrew Gerads]

Does mathlib have this?

lemma expHasDeriv (z:ℂ) : has_deriv_at (exp) (exp z) z :=

If so, then I would be interested in reading it for inspiration. library_search! did not find it.

[Junyan Xu]

docs#complex.has_strict_deriv_at_exp depends on docs#has_deriv_at_iff_is_o_nhds_zero so it's not based on termwise differentiation; #14090 was recently merged though and you may be able to make use of it.

[Matt Diamond]

there's also docs#complex.has_deriv_at_exp on the same page

[Matt Diamond]

I found it by searching has_deriv_at exp in the mathlib search box

[Matt Diamond]

I would encourage you to try that strategy in addition to library_search... I'm not familiar with this part of mathlib but I was able to find the lemma by choosing my search terms wisely

[Matt Diamond]

(I didn't see Junyan's comment until after I found it)

[Matt Diamond]

taking advantage of the search UI in the mathlib docs can save you a lot of time!

[Anatole Dedecker]

Let me just say that you shouldn’t take docs#complex.exp or docs#real.exp as inspiration for anything. Instead, you might want to have a look at docs#exp (so the theorem you’re looking for is really docs#has_deriv_at_exp)

[Anatole Dedecker]

Since we don’t have the tools to do the termwise differentiation (IIUC), your best option is to argue that this defines an analytic functions and thus it is differentiable with the derivative you think

[Anatole Dedecker]

Oh actually no because the only thing it gives you for free is the derivative at zero

[Mark Andrew Gerads]

Heather Macbeth said:

You might like to try writing it out carefully with, e.g., Corollary 6.2.13 in https://www.jirka.org/ra/realanal.pdf

Before I try to understand the proof, I would like to know that the complex analysis proof is exactly the same as the real analysis proof.

[Vincent Beffara]

You can do this (but it's not in mathlib):

variables [complete_space E] {f : 𝕜 → E} {p : formal_multilinear_series 𝕜 𝕜 E} {w : 𝕜} {n : ℕ}

noncomputable def formal_multilinear_series.deriv (p : formal_multilinear_series 𝕜 𝕜 E) :
  formal_multilinear_series 𝕜 𝕜 E :=
λ n, (n + 1) • (p (n + 1)).curry_left 1

lemma coeff_deriv : p.deriv.coeff n = (n + 1) • p.coeff (n + 1) := sorry

lemma apply_eq_iff_coeff_eq : p n = q n ↔ p.coeff n = q.coeff n := sorry

lemma eq_iff_coeff_eq : p = q ↔ ∀ n, p.coeff n = q.coeff n := sorry

lemma change_origin_series_eq_deriv :
  p.change_origin_series 1 n 1 (fin.snoc matrix.vec_empty 1) = p.deriv n 1 := sorry

lemma has_fpower_series_on_ball_deriv (hp : has_fpower_series_on_ball f p w r) :
  has_fpower_series_on_ball (deriv f) p.deriv w r :=

(including some of the lemmas I had to use to prove the last one, which IIUC is essentially what you are looking for). In particular, the API around docs#formal_multilinear_series.change_origin_series is helpful here, but not the easiest one to figure out. As far as I understand, these lemmas are not in mathlib because they are not at the right level of generality, but the formal_multilinear_series 𝕜 𝕜 E with deriv is a very common use case so it might make sense to include them.

[Vincent Beffara]

Also, docs#has_fpower_series_at.has_deriv_at and docs#has_fpower_series_at.has_strict_fderiv_at which all lead to docs#has_fpower_series_on_ball.fderiv

[Mark Andrew Gerads]

I still feel lost even with all these comments, so I decided to read "Complex Analysis" by John M. Howie. If I do not find my answer in that book, I will try a different Complex Analysis book.

[Vincent Beffara]

My impression is that most of your issues will not be mathematical but linked to the mathlib API, which takes a while to figure out. To fit in there, your first goal would probably be to define a formal_multilinear_series \C \C \C term corresponding to your function, show that it has infinite radius of convergence, and define the function itself using docs#formal_multilinear_series.sum (and have the fact that it is the sum of the series using docs#formal_multilinear_series.has_fpower_series_on_ball).

Then, docs#has_fpower_series_on_ball.fderiv and related from my previous comment are close to what you need, but there is some impedance mismatch between the fderiv version in mathlib and the deriv version that you need, which AFAIK is not bridged by lemmas that you will find in that form in mathlib. Mostly it has to do with identifying linear maps in dimension 1 with scalars.

[Vincent Beffara]

For instance:

variables {𝕜 E : Type*} [nontrivially_normed_field 𝕜] [normed_add_comm_group E] [normed_space 𝕜 E]

def plain_old_series (𝕜 : Type*) [nontrivially_normed_field 𝕜] {E : Type*}  [normed_add_comm_group E]
  [normed_space 𝕜 E] (a : ℕ → E) : formal_multilinear_series 𝕜 𝕜 E :=
λ n, continuous_multilinear_map.mk_pi_field 𝕜 (fin n) (a n)

example (a : ℕ → E) (n : ℕ) : (plain_old_series 𝕜 a).coeff n = a n :=
by simp [formal_multilinear_series.coeff, plain_old_series]

[Vincent Beffara]

Here is something that will work:

import analysis.analytic.basic
import analysis.complex.basic
import analysis.calculus.deriv
import analysis.calculus.fderiv_analytic

noncomputable theory

open formal_multilinear_series

variables {𝕜 E : Type*} [nontrivially_normed_field 𝕜] [normed_add_comm_group E] [normed_space 𝕜 E]
  [complete_space E] {p q : formal_multilinear_series 𝕜 𝕜 E} {n : ℕ} {f : 𝕜 → E} {w : 𝕜} {r : ennreal}

def plain_old_series (𝕜 : Type*) [nontrivially_normed_field 𝕜] {E : Type*}  [normed_add_comm_group E]
  [normed_space 𝕜 E] (a : ℕ → E) : formal_multilinear_series 𝕜 𝕜 E :=
λ n, continuous_multilinear_map.mk_pi_field 𝕜 (fin n) (a n)

lemma plain_old_series_coeff {a : ℕ → E} {n : ℕ} : (plain_old_series 𝕜 a).coeff n = a n :=
by simp [formal_multilinear_series.coeff, plain_old_series]

noncomputable def formal_multilinear_series.deriv (p : formal_multilinear_series 𝕜 𝕜 E) :
  formal_multilinear_series 𝕜 𝕜 E :=
λ n, (n + 1) • (p (n + 1)).curry_left 1

lemma coeff_deriv : p.deriv.coeff n = (n + 1) • p.coeff (n + 1) :=
begin
  simp only [formal_multilinear_series.deriv, formal_multilinear_series.coeff],
  simp only [fin.prod_cons, continuous_multilinear_map.smul_apply, apply_eq_prod_smul_coeff,
    continuous_multilinear_map.curry_left_apply, pi.one_apply, finset.prod_const_one, mul_one],
end

lemma apply_eq_iff_coeff_eq : p n = q n ↔ p.coeff n = q.coeff n :=
begin
  simp only [continuous_multilinear_map.ext_iff],
  split; intro h,
  { simpa using h 1 },
  { simp [h] }
end

lemma eq_iff_coeff_eq : p = q ↔ ∀ n, p.coeff n = q.coeff n :=
by simp [formal_multilinear_series.ext_iff, apply_eq_iff_coeff_eq]

lemma change_origin_series_eq_deriv :
  p.change_origin_series 1 n 1 (fin.snoc matrix.vec_empty 1) = p.deriv n 1 :=
begin
  change p.change_origin_series 1 n 1 1 = p.deriv n 1,
  let S : finset {s : finset (fin (1 + n)) // s.card = n} := finset.univ,
  suffices : S.card • p.coeff (1 + n) = p.deriv.coeff n,
    simpa [change_origin_series, change_origin_series_term] using this,
  simp [coeff_deriv, S, add_comm 1 n, finset.card_univ]
end

lemma has_fpower_series_on_ball.deriv (hp : has_fpower_series_on_ball f p w r) :
  has_fpower_series_on_ball (deriv f) p.deriv w r :=
begin
  let ev : (𝕜 →L[𝕜] E) →L[𝕜] E := continuous_linear_map.apply _ _ 1,
  convert ← (ev.comp_has_fpower_series_on_ball hp.fderiv),
  refine eq_iff_coeff_eq.mpr (λ n, _),
  simp only [ev, formal_multilinear_series.coeff, linear_isometry_equiv.coe_coe'',
    continuous_linear_map.comp_formal_multilinear_series_apply, change_origin_series_eq_deriv,
    function.comp_app, continuous_linear_map.comp_continuous_multilinear_map_coe,
    continuous_multilinear_curry_fin1_apply, continuous_linear_map.apply_apply, matrix.zero_empty]
end

lemma has_fpower_series_on_ball.has_deriv_at (hp : has_fpower_series_on_ball f p w r) {z : 𝕜}
  (hz : z ∈ emetric.ball w r) : has_deriv_at f (p.deriv.sum (z - w)) z :=
begin
  have h1 := hp.deriv,
  have h2 : differentiable_at 𝕜 f z,
    from hp.differentiable_on.differentiable_at (is_open.mem_nhds emetric.is_open_ball hz),
  have h3 := has_deriv_at_deriv_iff.mpr h2,
  convert h3,
  have h4 : z - w ∈ emetric.ball (0 : 𝕜) r,
    by simpa [edist_comm z w, ← edist_sub_left z w z] using hz,
  simpa [formal_multilinear_series.sum] using (h1.has_sum h4).tsum_eq,
end

------------------------

def rues (n m k : ℕ) : ℂ := if (k + m) % n = 0 then (1 : ℂ) / k.factorial else 0

def rues_series (n m : ℕ) := plain_old_series ℂ (rues n m)

@[simp] lemma rues_series_radius {n m : ℕ} : (rues_series n m).radius = ⊤ := sorry

@[simp] lemma rues_series.deriv {n m : ℕ} : (rues_series n m).deriv = rues_series n (m + 1) :=
begin
  refine eq_iff_coeff_eq.mpr (λ k, _),
  simp [coeff_deriv, rues_series, plain_old_series_coeff],
  sorry -- but this is a useful lemma anyway
end

def rues_function (n m : ℕ) : ℂ → ℂ := (rues_series n m).sum

lemma ruesDiffHasDeriv (n m : ℕ) (h : 0 < n) (z : ℂ) :
  has_deriv_at (rues_function n m) (rues_function n (m + 1) z) z :=
begin
  have h1 : ∀ {n m}, 0 < (rues_series n m).radius := by simp,
  have h2 := (rues_series n m).has_fpower_series_on_ball h1,
  have h3 : z ∈ emetric.ball (0 : ℂ) (rues_series n m).radius := by simp,
  simpa [rues_function] using h2.has_deriv_at h3
end

[Vincent Beffara]

"Above the fold" is something that I believe should be in mathlib (but it is kind of messy and would need some refinement). "Below the fold" is domain specific, I did not fill the sorries but they should be fairly straightforward, and needed in any case for the initial question...

[Mark Andrew Gerads]

I made some progress.

lemma inv_mul_other_mul_self_cancel (z1 z2:ℂ) (h:z1≠0): z1⁻¹ * z2 * z1 = z2:=
  by field_simp

@[simp] lemma rues_series.deriv {n m : ℕ} : (rues_series n m).deriv = rues_series n (m + 1) :=
begin
  refine eq_iff_coeff_eq.mpr (λ k, _),
  simp [coeff_deriv, rues_series, plain_old_series_coeff],
  rw [rues,rues],
  simp only [nat.factorial_succ, nat.cast_mul, nat.cast_add, nat.cast_one, one_div, mul_inv_rev, mul_ite, mul_zero],
  rw (show k + (m + 1)=k + 1 + m, by ring),
  congr' 1,
  norm_cast at *,
  ring_nf,
  have h1:↑(k + 1)≠(0:ℂ),
  norm_cast at *,
  rw inv_mul_other_mul_self_cancel (↑(k + 1)) ((↑(k.factorial))⁻¹) h1,
end

[Mark Andrew Gerads]

How does one get this lemma?

@[simp] lemma rues_series_radius {n m : ℕ} : (rues_series n m).radius = ⊤ :=

I understand that the normal way is to find a limit like $\lim_{n\to\infty}(a_n)^{1/n}$, but that limit does not exist when $a_n$ alternates between 0 and other numbers. I suspect the easiest way is to show the radius is infinite in the case of $\exp(z)$, maybe using (exp_series_div_summable ℂ (abs z)) or something similar, and use the absolute convergence to bound the absolute value of rues_series n m z via rues_series n m (abs z). Something like that might work.
I would appreciate help.

[Vincent Beffara]

You can try using docs#formal_multilinear_series.radius_eq_liminf to follow this idea, or you can ask here if there is a lemma saying that the radius of a series with smaller coefficients is larger (and possibly nerdsnipe someone into proving it) and then use this, which would be the most natural option.

Alternatively you can have a look at docs#exp_series_radius_eq_top and its proof and adapt it to your case.

[Mark Andrew Gerads]

Thanks. I look forward to you getting your 'above the fold' lemmas into mathlib.

[Jireh Loreaux]

I don't think this exists, but I have been nerdsniped. It's easy to combine this with docs#formal_multilinear_series.radius_eq_liminf to get that the radius of a series with smaller coefficients is larger. I encourage you to clean it up and PR it.

import analysis.analytic.radius_liminf

open filter
open_locale nnreal ennreal

lemma foo (a b : ℕ → ℝ≥0) (h : a ≤ b) :
  at_top.liminf (λ n, 1 / ((b n ^ (1 / (n : ℝ))) : ℝ≥0∞)) ≤
  at_top.liminf (λ n, 1 / ((a n ^ (1 / (n : ℝ))) : ℝ≥0∞)) :=
begin
  refine liminf_le_liminf (_ : ∀ᶠ n in at_top, (1 / ((b n ^ (1 / (n : ℝ))) : ℝ≥0∞)) ≤
    (1 / ((a n ^ (1 / (n : ℝ))) : ℝ≥0∞))),
  filter_upwards [Ioi_mem_at_top 0] with n hn,
  simp only [one_div, ennreal.inv_le_inv,
    ennreal.rpow_le_rpow_iff (inv_pos.mpr $ nat.cast_pos.mpr hn)],
  exact_mod_cast h n,
end

[Vincent Beffara]

My version (I nerdsniped myself :grinning_face_with_smiling_eyes:):

lemma radius_le_radius_of_nnnorm_le (h : ∀ n, ∥p n∥₊ ≤ ∥q n∥₊) : q.radius ≤ p.radius :=
begin
  simp [radius_eq_liminf],
  refine @liminf_le_liminf ennreal ℕ _ at_top _ _ _ _ _,
  { refine eventually_of_forall (λ n, _),
    simp only [ennreal.inv_le_inv, ennreal.coe_le_coe],
    exact nnreal.rpow_le_rpow (h n) (by positivity) },
  { exact ⟨0, by simp⟩ },
  { exact ⟨⊤, by simp⟩ }
end

lemma radius_le_radius_of_nnnorm_le' (h : ∀ n, ∥p.coeff n∥ ≤ ∥q.coeff n∥) : q.radius ≤ p.radius :=
radius_le_radius_of_nnnorm_le (by simp [← norm_to_nnreal, h])

[Mark Andrew Gerads]

I made progress again, but am stuck with (list.of_fn 1).prod not simplifying. It is the same problem located at both sorrys.

import analysis.analytic.basic
import analysis.complex.basic
import analysis.calculus.deriv
import analysis.calculus.fderiv_analytic
import analysis.analytic.radius_liminf
import analysis.normed_space.exponential

noncomputable theory

open formal_multilinear_series
open filter
open_locale nnreal ennreal

variables {𝕜 E : Type*} [nontrivially_normed_field 𝕜] [normed_add_comm_group E] [normed_space 𝕜 E]
  [complete_space E] {p q : formal_multilinear_series 𝕜 𝕜 E} {n : ℕ} {f : 𝕜 → E} {w : 𝕜} {r : ennreal}

def plain_old_series (𝕜 : Type*) [nontrivially_normed_field 𝕜] {E : Type*}  [normed_add_comm_group E]
  [normed_space 𝕜 E] (a : ℕ → E) : formal_multilinear_series 𝕜 𝕜 E :=
λ n, continuous_multilinear_map.mk_pi_field 𝕜 (fin n) (a n)

lemma plain_old_series_coeff {a : ℕ → E} {n : ℕ} : (plain_old_series 𝕜 a).coeff n = a n :=
by simp [formal_multilinear_series.coeff, plain_old_series]

noncomputable def formal_multilinear_series.deriv (p : formal_multilinear_series 𝕜 𝕜 E) :
  formal_multilinear_series 𝕜 𝕜 E :=
λ n, (n + 1) • (p (n + 1)).curry_left 1

lemma coeff_deriv : p.deriv.coeff n = (n + 1) • p.coeff (n + 1) :=
begin
  simp only [formal_multilinear_series.deriv, formal_multilinear_series.coeff],
  simp only [fin.prod_cons, continuous_multilinear_map.smul_apply, apply_eq_prod_smul_coeff,
    continuous_multilinear_map.curry_left_apply, pi.one_apply, finset.prod_const_one, mul_one],
end

lemma apply_eq_iff_coeff_eq : p n = q n ↔ p.coeff n = q.coeff n :=
begin
  simp only [continuous_multilinear_map.ext_iff],
  split; intro h,
  { simpa using h 1 },
  { simp [h] }
end

lemma eq_iff_coeff_eq : p = q ↔ ∀ n, p.coeff n = q.coeff n :=
by simp [formal_multilinear_series.ext_iff, apply_eq_iff_coeff_eq]

lemma change_origin_series_eq_deriv :
  p.change_origin_series 1 n 1 (fin.snoc matrix.vec_empty 1) = p.deriv n 1 :=
begin
  change p.change_origin_series 1 n 1 1 = p.deriv n 1,
  let S : finset {s : finset (fin (1 + n)) // s.card = n} := finset.univ,
  suffices : S.card • p.coeff (1 + n) = p.deriv.coeff n,
    simpa [change_origin_series, change_origin_series_term] using this,
  simp [coeff_deriv, S, add_comm 1 n, finset.card_univ]
end

lemma has_fpower_series_on_ball.deriv (hp : has_fpower_series_on_ball f p w r) :
  has_fpower_series_on_ball (deriv f) p.deriv w r :=
begin
  let ev : (𝕜 →L[𝕜] E) →L[𝕜] E := continuous_linear_map.apply _ _ 1,
  convert ← (ev.comp_has_fpower_series_on_ball hp.fderiv),
  refine eq_iff_coeff_eq.mpr (λ n, _),
  simp only [ev, formal_multilinear_series.coeff, linear_isometry_equiv.coe_coe'',
    continuous_linear_map.comp_formal_multilinear_series_apply, change_origin_series_eq_deriv,
    function.comp_app, continuous_linear_map.comp_continuous_multilinear_map_coe,
    continuous_multilinear_curry_fin1_apply, continuous_linear_map.apply_apply, matrix.zero_empty]
end

lemma has_fpower_series_on_ball.has_deriv_at (hp : has_fpower_series_on_ball f p w r) {z : 𝕜}
  (hz : z ∈ emetric.ball w r) : has_deriv_at f (p.deriv.sum (z - w)) z :=
begin
  have h1 := hp.deriv,
  have h2 : differentiable_at 𝕜 f z,
    from hp.differentiable_on.differentiable_at (is_open.mem_nhds emetric.is_open_ball hz),
  have h3 := has_deriv_at_deriv_iff.mpr h2,
  convert h3,
  have h4 : z - w ∈ emetric.ball (0 : 𝕜) r,
    by simpa [edist_comm z w, ← edist_sub_left z w z] using hz,
  simpa [formal_multilinear_series.sum] using (h1.has_sum h4).tsum_eq,
end

lemma radius_le_radius_of_nnnorm_le (h : ∀ n, ∥p n∥₊ ≤ ∥q n∥₊) : q.radius ≤ p.radius :=
begin
  simp [radius_eq_liminf],
  refine @liminf_le_liminf ennreal ℕ _ at_top _ _ _ _ _,
  { refine eventually_of_forall (λ n, _),
    simp only [ennreal.inv_le_inv, ennreal.coe_le_coe],
    exact nnreal.rpow_le_rpow (h n) (by positivity) },
  { exact ⟨0, by simp⟩ },
  { exact ⟨⊤, by simp⟩ }
end

lemma radius_le_radius_of_nnnorm_le' (h : ∀ n, ∥p.coeff n∥ ≤ ∥q.coeff n∥) : q.radius ≤ p.radius :=
radius_le_radius_of_nnnorm_le (by simp [← norm_to_nnreal, h])

------------------------

#check exp_series ℂ ℂ
#check (exp_series ℂ ℂ).coeff
#check (exp_series ℂ ℂ).radius

def rues_coeff (n m k : ℕ) : ℂ := if (k + m) % n = 0 then (1 : ℂ) / k.factorial else 0

def rues_series (n m : ℕ) := plain_old_series ℂ (rues_coeff n m)

@[simp] lemma rues_series_radius {n m : ℕ} : (rues_series n m).radius = ⊤ :=
begin
  have h:∀ (k:ℕ), ∥(rues_series n m).coeff k∥ ≤ ∥(exp_series ℂ ℂ).coeff k∥,
  {
    intro k,
    rw [coeff,coeff],
    rw [rues_series,exp_series],
    rw [plain_old_series],
    simp only [continuous_multilinear_map.mk_pi_field_apply, pi.one_apply, finset.prod_const_one, algebra.id.smul_eq_mul, one_mul,
  complex.norm_eq_abs, continuous_multilinear_map.smul_apply, continuous_multilinear_map.mk_pi_algebra_fin_apply,
  absolute_value.map_mul, map_inv₀, complex.abs_cast_nat],
    rw rues_coeff,
    have h3:=classical.em ((k + m) % n = 0),
    cases h3,
    {
      rw [if_pos h3],
      simp only [one_div, map_inv₀, complex.abs_cast_nat],
      sorry,
    },
    {
      rw [if_neg h3],
      simp only [absolute_value.map_zero],
      sorry,
    },
  },
  have h2:=radius_le_radius_of_nnnorm_le' h,
  rw (exp_series_radius_eq_top ℂ ℂ) at h2,
  exact eq_top_iff.mpr h2,
end

lemma inv_mul_other_mul_self_cancel (z1 z2:ℂ) (h:z1≠0): z1⁻¹ * z2 * z1 = z2:=
  by field_simp

@[simp] lemma rues_series.deriv {n m : ℕ} : (rues_series n m).deriv = rues_series n (m + 1) :=
begin
  refine eq_iff_coeff_eq.mpr (λ k, _),
  simp [coeff_deriv, rues_series, plain_old_series_coeff],
  rw [rues_coeff,rues_coeff],
  simp only [nat.factorial_succ, nat.cast_mul, nat.cast_add, nat.cast_one, one_div, mul_inv_rev, mul_ite, mul_zero],
  rw (show k + (m + 1)=k + 1 + m, by ring),
  congr' 1,
  norm_cast at *,
  ring_nf,
  have h1:↑(k + 1)≠(0:ℂ),
  norm_cast at *,
  rw inv_mul_other_mul_self_cancel (↑(k + 1)) ((↑(k.factorial))⁻¹) h1,
end

def rues_function (n m : ℕ) : ℂ → ℂ := (rues_series n m).sum

lemma ruesDiffHasDeriv (n m : ℕ) (h : 0 < n) (z : ℂ) :
  has_deriv_at (rues_function n m) (rues_function n (m + 1) z) z :=
begin
  have h1 : ∀ {n m}, 0 < (rues_series n m).radius := by simp,
  have h2 := (rues_series n m).has_fpower_series_on_ball h1,
  have h3 : z ∈ emetric.ball (0 : ℂ) (rues_series n m).radius := by simp,
  simpa [rues_function] using h2.has_deriv_at h3
end

[Vincent Beffara]

docs#list.prod_of_fn

[Mark Andrew Gerads]

The derivative is now proved with no sorry in sight! Thanks everyone, especially @Vincent Beffara .

[Vincent Beffara]

I tried it on my side, here is my version:

@[simp] lemma rues_series_radius {n m : ℕ} : (rues_series n m).radius = ⊤ :=
begin
  suffices : (exp_series ℂ ℂ).radius ≤ (rues_series n m).radius,
    simpa [exp_series_radius_eq_top ℂ ℂ] using this,
  refine radius_le_radius_of_nnnorm_le' (λ k, _),
  by_cases (k + m) % n = 0;
  simp [rues_series, rues, exp_series, coeff, list.prod_of_fn, plain_old_series, h]
end

@[simp] lemma rues_series.deriv {n m : ℕ} : (rues_series n m).deriv = rues_series n (m + 1) :=
begin
  refine eq_iff_coeff_eq.mpr (λ k, _),
  have : (k : ℂ) + 1 ≠ 0 := by { norm_cast; exact ne_zero.ne (k + 1) },
  simp [rues_series, rues, (show k + (m + 1) = k + 1 + m, by ring)],
  congr' 1,
  field_simp [this, ← div_div],
end

def rues_function (n m : ℕ) : ℂ → ℂ := (rues_series n m).sum

lemma ruesDiffHasDeriv (n m : ℕ) (h : 0 < n) (z : ℂ) :
  has_deriv_at (rues_function n m) (rues_function n (m + 1) z) z :=
begin
  have h2 := (rues_series n m).has_fpower_series_on_ball (by simp),
  have h3 : z ∈ emetric.ball (0 : ℂ) (rues_series n m).radius := by simp,
  simpa [rues_function] using h2.has_deriv_at h3
end

[Vincent Beffara]

Is there any piece of additional API that you would have found useful? I will turn these lemmas into a PR at some point, and would like to know what to add or change before that ...

[Mark Andrew Gerads]

Well, I suppose I would like to show that your rues_function equals my other definition, which uses tsum in the first post of this thread.
Another lemma that would be useful is showing something like

lemma ruesDiffSummable (n:ℕ) (h:0<n) (m:ℤ) (z:ℂ) : summable (λ (k:ℕ), if ((k:ℤ)+m)%n=0 then z ^ k / k.factorial else 0):=

using the fact that (rues_series n m).radius = ⊤
I don't know how hard that would be because I haven't tried it yet.

[Vincent Beffara]

For the first one, you can combine docs#formal_multilinear_series.has_sum and docs#has_sum.tsum_eq (up to the difference between nat and int).

For the second, does docs#formal_multilinear_series.summable_norm_mul_pow with r = 1 work for you? Or even docs#formal_multilinear_series.summable

[Mark Andrew Gerads]

It looks like metric.emetric_ball_top can be used with docs#formal_multilinear_series.summable to get my desired result.