Having trouble taking a derivative

Stream: new members

[Mark Gerads]

Playing around with Lean and got this far... 2*sorry.

import all

open classical

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


lemma ruesDiffDeriv (n:ℕ) (m:ℤ) (z:ℂ) : has_deriv_at (ruesDiff n m) (ruesDiff n (m+1) z) z :=
begin
  rw [has_deriv_at, has_deriv_at_filter, has_fderiv_at_filter],
  simp only [continuous_linear_map.smul_right_apply, continuous_linear_map.one_apply, algebra.id.smul_eq_mul],
  rw [asymptotics.is_o],
  intros c h,
  rw [asymptotics.is_O_with, ruesDiff, ruesDiff, nhds],
  simp only [euclidean_domain.mod_eq_zero, complex.norm_eq_abs, set.mem_set_of_eq],
  sorry,
end

lemma ruesDiffDeriv2 (n:ℕ) (m:ℤ) (z:ℂ) : deriv (ruesDiff n m) z = ruesDiff n (m+1) z :=
begin
  rw [deriv, fderiv],
  dsimp only,
  sorry,
end

Help is much appreciated.

[Eric Wieser]

That feels like it would be easier if you defined the function without the if

[Eric Wieser]

That is, write an expression that generates the powers k that you care about, rather than filtering them

[Eric Wieser]

You can of course prove that one definition is equal to the other

[Mark Gerads]

Well, I will show the series of conditional ite stuff to be equivalent to a geometric series of a root of unity. The geometric series cancels to 0 if the root of unity is not 1, and something else if the root of unity is 1, but I don't think that will make it easier to take the derivative.

[Mark Gerads]

Looking at complex.has_deriv_at_exp and deriv_exp for insight.

[Mark Gerads]

I figured out a sorry!

lemma ruesDiffDeriv2 (n:ℕ) (m:ℤ) (z:ℂ) : deriv (ruesDiff n m) z = ruesDiff n (m+1) z :=
begin
  rw (ruesDiffDeriv n m z).deriv,
end

[Mark Gerads]

I feel like I am closer now with this. Can someone prove openUnitDiskIsOpen?

lemma openUnitDiskIsOpen : is_open {a : ℂ | complex.abs a < 1} :=
begin
  sorry,
end

lemma ruesDiffDeriv (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],
  refine eventually_nhds_iff.mpr _,
  use {a:ℂ|complex.abs a < 1},
  simp only [set.mem_set_of_eq, algebra.id.smul_eq_mul, complex.norm_eq_abs, complex.abs_zero, zero_lt_one, and_true],
  split,
  intros x xLt1,
  {
    rw [ruesDiff, ruesDiff, ruesDiff],
    simp only [euclidean_domain.mod_eq_zero],
    sorry,
  },
  exact openUnitDiskIsOpen,
end

[Andrew Yang]

docs#metric.is_open_ball should be helpful. This is found by searching is_open.+ball in vscode.