Why is there a def for `geom_sum`?

Stream: general

[Scott Morrison]

src#geom_sum is a definition def geom_sum (x : α) (n : ℕ) := ∑ i in range n, x ^ i. Is there any reason to have this definition, instead of just stating the results about the sum itself? Looking through mathlib, it seems that everywhere that people need to use geom_sum, they need to begin by rewriting by geom_sum_def, which seems rather annoying.

It also means that none of the simp lemmas actually apply until you rewrite things in terms of geom_sum, which seems tedious: I'd say if there's reason to keep the definition we probably should restate all its simp lemmas with geom_def unfolded.

[Kevin Buzzard]

Just to remark that I've been using geometric sums in LTE and I didn't use this definition once

[Johan Commelin]

Kevin, did you use finite or infinite geometric sums?

[Johan Commelin]

@Scott Morrison would it help if we make it an abbreviation?

[Kevin Buzzard]

Aah, infinite ones. Is it something to do with ticking off something on the UG list?

[Scott Morrison]

I tried abbreviation, and it doesn't help with the @[simp] lemma problem, because that is working syntactically, so it can't see that explicit sums are geom_sums.

[Eric Wieser]

Yeah, my first thought was "this might be needed by undergrad.yml"

[Scott Morrison]

Can I just make it notation?

[Eric Wieser]

I don't even think there's any point having the notation

[Scott Morrison]

Is there a way to expand geom_sum x n as ∑ i in range n, x ^ i?

[Scott Morrison]

Mostly I just want to notation temporarily to check that the file behaves as expected, without actually having to rewrite it :-)

[Scott Morrison]

Does anyone know if this notation is possible, without a token between the x and n? I can't find an example in mathlib.

[Eric Wieser]

notation `geom_sum` x := λ n, (range n).sum ((^) x) maybe?

[Scott Morrison]

Let me try

[Eric Wieser]

If you can deal with one lingering lambda

[Scott Morrison]

Doesn't seem to work anyway.

[Scott Morrison]

Every geom_sum x n gives a function expected at x term has type ...

[Scott Morrison]

Maybe notation `geom_sum` x:2000 := (λ n, (range n).sum ((^) x))

[Scott Morrison]

Still too much lambda, oh well, I'll bite the bullet and write them out.

[Kyle Miller]

I wonder if it would be worth having an elab_inline attribute, so then we could have synonyms that don't get in the way of rewrites, and we wouldn't need to abuse notation?

[Kyle Miller]

For the "too much lambda" problem, maybe there could be a special elab_beta identity function that causes the elaborator to do beta reduction using its first two arguments.