## Stream: new members

### Topic: sum_mul

#### 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


#### Iocta (Aug 12 2020 at 23:36):

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

#### Iocta (Aug 12 2020 at 23:39):

aha, tsum_mul_right looks promising

#### 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?

#### Iocta (Aug 12 2020 at 23:46):

like k

#### Dan Stanescu (Aug 12 2020 at 23:50):

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

#### Iocta (Aug 12 2020 at 23:51):

just for clarity for the reader

#### 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)),


#### 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