Zulip Chat Archive

Stream: new members

Topic: sum_mul


view this post on Zulip Iocta (Aug 12 2020 at 23:33):

sum_mul doesn't exist, what do I mean?

import measure_theory.probability_mass_function
import analysis.normed_space.indicator_function
import measure_theory.set_integral
import analysis.specific_limits
import data.real.basic
import data.nat.basic
import algebra.geom_sum


open set filter topological_space measure_theory
open_locale classical topological_space interval

example (p : nnreal) (hp : p  1) :
(∑' (k:nat), (1 - p ) ^ (k - 1) * p) = (∑' (k:nat), (1 - p) ^ (k -1) ) * p :=
begin
  -- rw sum_mul,
end

view this post on Zulip Iocta (Aug 12 2020 at 23:36):

In english, I want to pull the p out of the \sum over k

view this post on Zulip Iocta (Aug 12 2020 at 23:39):

aha, tsum_mul_right looks promising

view this post on Zulip Iocta (Aug 12 2020 at 23:46):

When lean picks a variable name for me such as b in ⊢ (∑' (b : ℕ), (1 - p) ^ (b - 1)) * p = 1, how do I tell it I want a different name?

view this post on Zulip Iocta (Aug 12 2020 at 23:46):

like k

view this post on Zulip Dan Stanescu (Aug 12 2020 at 23:50):

Do you really need to? In my experience, it doesn't matter.

view this post on Zulip Iocta (Aug 12 2020 at 23:51):

just for clarity for the reader

view this post on Zulip Alex J. Best (Aug 13 2020 at 00:02):

You can use change or show.
Either a short form like

  show summable (λ (l : ), _),

or for clarity

  show summable (λ (l : ), (1 - p) ^ (l - 1)),

view this post on Zulip Kevin Buzzard (Aug 13 2020 at 07:20):

Just to note that you're using natural number subtraction, which should be avoided because you'll have problems with it later


Last updated: May 06 2021 at 21:09 UTC