Showing a sum is summable

Stream: maths

[Mark Gerads]

I want the following lemma, yet don't know how to show it. library_search, hint, and suggest did not help.

lemma ruesSummable (n:ℕ) (h:n>0) (z:ℂ) : summable (λ (k:ℕ), z ^ (n*k) / (n*k).factorial):=

[Ruben Van de Velde]

Do you mean "I think this is in the library, but I can't find it", or "I want to prove it by myself, but I don't know how to start"?

[Mark Gerads]

I would like to prove it; I don't know how to start, and it is not in the library.

[Adam Topaz]

if you can compute the sum, you can use docs#has_sum

[Adam Topaz]

summable is defined as ∃ a, has_sum f a

[Adam Topaz]

And docs#has_sum unfolds to a tendsto assertion.

[Adam Topaz]

In this case you can probably get by with less explicit methods by using summability of the series defining the exponential

[Mark Gerads]

I only got this far, and don't know how to get further:

lemma ruesSummable (n:ℕ) (h:n>0) (z:ℂ) : summable (λ (k:ℕ), z ^ (n*k) / (n*k).factorial):=
begin
  rw [summable],
  use tsum (λ (k:ℕ), z ^ (n*k) / (n*k).factorial),
  rw has_sum,
  sorry,
end

[Congzhou Sha]

You can keep unfolding/rewriting terms until you get something more basic. Can you show the entire file (the imports), or at least what suggest comes up with?

[Jireh Loreaux]

docs#summable_nat_add_iff and docs#exp_series_div_summable and I think will get you almost all the way there.

[Jireh Loreaux]

whoops, sorry, I misread * for +.

[Mark Gerads]

suggest results in an error: excessive memory consumption detected
RootOfUnityExponentialSum.lean

[Jireh Loreaux]

how about docs#summable.comp_injective and docs#exp_series_div_summable, that should do the trick.

[Jireh Loreaux]

Do you understand my suggestion?

[Mark Gerads]

theorem summable.comp_injective {α : Type u_1} {β : Type u_2} {γ : Type u_3} [add_comm_group α] [uniform_space α] [uniform_add_group α] {f : β → α} [complete_space α] {i : γ → β} (hf : summable f) (hi : function.injective i) :
summable (f ∘ i)

This does look like it will work; I need to show that i=(λ (k:ℕ), n*k) is injective, then the pieces should fit, right?

[Jireh Loreaux]

Yes, for which I think it would be easiest to apply docs#strict_mono.injective

[Jireh Loreaux]

Yep, here:

lemma ruesSummable (n:ℕ) (h:n>0) (z:ℂ) : summable (λ (k:ℕ), z ^ (n*k) / (n*k).factorial):=
(exp_series_div_summable ℂ z).comp_injective (strict_mono_mul_left_of_pos h).injective

[Kevin Buzzard]

As an exercise @Mark Gerads can you translate Jireh's term mode proof into a tactic mode proof?

[Kevin Buzzard]

By the way, the mathlib style would be h : 0 < n not h:n>0, because > is banned until Lean 4.

[Mark Gerads]

I suppose just adding begin, exact, and end around the golf code is cheating?
I'll update my file to get rid of > then.

[Jireh Loreaux]

I think what Kevin means is: take the pieces docs#summable.comp_injective, docs#exp_series_div_summable, docs#strict_mono.injective (and potentially docs#strict_mono_mul_left_of_pos, but to be honest I found this with tactic#library_search) and build a proof in tactic mode using these pieces on your own. Optionally, you can look at my proof to understand how the pieces should fit together, but it might be better to try and avoid that.