Zulip Chat Archive

Stream: maths

Topic: Showing a sum is summable


Mark Gerads (Sep 22 2022 at 16:03):

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 (Sep 22 2022 at 16:11):

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 (Sep 22 2022 at 16:19):

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

Adam Topaz (Sep 22 2022 at 16:23):

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

Adam Topaz (Sep 22 2022 at 16:23):

summable is defined as ∃ a, has_sum f a

Adam Topaz (Sep 22 2022 at 16:24):

And docs#has_sum unfolds to a tendsto assertion.

Adam Topaz (Sep 22 2022 at 16:25):

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

Mark Gerads (Sep 22 2022 at 18:03):

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 (Sep 22 2022 at 18:13):

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 (Sep 22 2022 at 18:20):

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

Jireh Loreaux (Sep 22 2022 at 18:21):

whoops, sorry, I misread * for +.

Mark Gerads (Sep 22 2022 at 18:21):

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

Jireh Loreaux (Sep 22 2022 at 18:25):

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

Jireh Loreaux (Sep 22 2022 at 18:28):

Do you understand my suggestion?

Mark Gerads (Sep 22 2022 at 18:32):

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 (Sep 22 2022 at 18:37):

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

Jireh Loreaux (Sep 22 2022 at 18:39):

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 (Sep 22 2022 at 18:46):

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

Kevin Buzzard (Sep 22 2022 at 18:47):

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

Mark Gerads (Sep 22 2022 at 18:49):

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 (Sep 22 2022 at 19:13):

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.


Last updated: Dec 20 2023 at 11:08 UTC