sum_mul

Stream: new members

[Iocta]

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]

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

[Iocta]

aha, tsum_mul_right looks promising

[Iocta]

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]

like k

[Dan Stanescu]

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

[Iocta]

just for clarity for the reader

[Alex J. Best]

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]

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