# Zulip Chat Archive

## Stream: general

### Topic: Proving identities from Table of Integrals, Series, and Prod

#### Congzhou Sha (Sep 19 2022 at 22:19):

This is definitely going to be a massive undertaking, but I've started proving identities from the book by Gradshteyn and Ryzhik (https://github.com/mikesha2/identitylib). So far, a lot of it is algebraic hell...

#### Moritz Doll (Sep 19 2022 at 22:27):

This is great. One way I tried to convince analysts that formalization is useful (this is quite a hard task) is saying that having formalization of these huge libraries of special functions identities and estimates in a digitalized form would be so much better than what we have now (also considering that these things tend to have mistakes and no proofs). For the really interesting parts I think we still lack the complex analysis tools, but the more fundamental things would be great to have in mathlib.

#### Eric Wieser (Sep 19 2022 at 22:29):

I'd be very surprised if this lemma about derivatives combining additively is not in mathlib as something like docs#has_deriv_at.add

#### Congzhou Sha (Sep 19 2022 at 22:46):

It's absolutely in there, and I've been trying to learn more theorems that are already in mathlib, but philosophically, it shouldn't matter, right? As long as I see "goal accomplished"

#### Scott Morrison (Sep 20 2022 at 02:04):

Here's the argument that it does matter. Beyond just being formally checked, we want mathematical results to be discoverable, usable, and maintainable. All of these problems getting easier the tighter the integration with mathlib. It's very important for usability that libraries can be imported simultaneously with mathlib (duplication is not actually an issue here). I would argue that a repository becomes much more maintainable if it adheres to the same standards (documentation, proof style, lemma naming, etc) as mathlib --- first because there are lots of people familiar with those standards who can contribute, and secondly because it significantly lowers the barrier to porting critical parts of an external library into mathlib if it becomes necessary (either for mathlib's own purposes, or maintenance).

I think the "perfect" approach to formalizing a large set of results (assuming they are significant enough and on topic enough to warrant living in mathlib, but that certainly applies here) is to PR them all directly into mathlib, using doc-strings to label the theorems as coming from some named collection. (e.g. see how we link to the Stacks project in many places).

It is obviously more work, but there are significant payoffs: the discipline of going through the mathlib PR process results in much better code at the end of the day (plus you learn "mathlib style", making it easier to collaborate with others), and of course you get to hope that your contributions are maintained longer, and discovered by more people.

On the other hand, perfect is the enemy of good, and it's completely fine to work off in your own repository, duplication mathlib results as you see fit. :-)

#### Congzhou Sha (Sep 22 2022 at 15:02):

I'm actually pretty concerned about the transition from Lean 3 to Lean 4 as well (especially for mathlib). Also since this is a hobby project for me, I think that it makes sense for me to work with a stable mathlib build, so for now I think I won't commit directly the mathlib. At some point in the future when I think I have a pretty good grasp on mathlib and I've proven a substantial number of identities, I will work on streamlining my results with theorems from mathlib and submitting PRs, which should be a far easier task than the initial writing of the theorems.

As a small update, it took me about a week to get through the first 4 identities, and I'm hoping my speed will improve as I do more. I think I might need to formalize some umbral calculus to make some of the combinatoric identities easier: image.png

#### Scott Morrison (Sep 23 2022 at 00:58):

Another take on this is that there is typically a bit of a learning curve in making mathlib PRs, and that you will likely find that you are substantially rewriting material during the PR process. Making a few small PRs early in the process may save effort overall, as you'll be able to do more of your development in mathlib style/quality on the first pass.

#### Kevin Buzzard (Sep 23 2022 at 10:43):

@Congzhou Sha Here's a golfed proof of the first lemma:

```
@[simp] theorem arithmetic_progression_0_111 (n : ℕ) (a r : ℝ) :
∑ (k : ℕ) in finset.range n, (a + k * r) = n * (a + (n - 1) * r / 2) :=
begin
induction n with n ih,
{ simp, },
{ rw [finset.sum_range_succ, ih],
simp, ring,
},
end
```

You don't need to do all this `rw right_distrib`

stuff -- we have tools like `ring`

for that.

A comment on the `@[simp]`

attribute: `simp`

will never fire on a lemma like

```
@[simp] theorem geometric_progression_0_112 (n : ℕ) (a q : ℝ) (h : q ≠ 1) :
∑ (k : ℕ) in finset.range n, a * q ^ k = a * (q ^ n - 1) / (q - 1) :=
```

because the simplifier will not be able to find a proof of the hypothesis `q \ne 1`

.

#### Yaël Dillies (Sep 23 2022 at 10:45):

Technically speaking, `simp`

*could* prove `q ≠ 1`

, but only in very few cases.

#### Kevin Buzzard (Sep 23 2022 at 10:47):

```
lemma k_squared_geometric_progression_algebra (x : ℝ) (n : ℕ) :
-x ^ (n + 2) * ↑n * ↑n +
(2 * x ^ (n + 1) * ↑n * ↑n +
(-x * x * x * x ^ n * ↑n * ↑n + 3 * x * x * x ^ n * ↑n * ↑n -
3 * x * x ^ n * ↑n * ↑n)) =
2 * x ^ (n + 2) * ↑n * ↑n +
(-x ^ (n + 1) * ↑n * ↑n - x ^ (n + 3) * ↑n * ↑n) :=
begin
ring_exp,
end
```

#### Eric Rodriguez (Sep 23 2022 at 10:49):

you can always pass them in, though, Kevin:

```
import data.real.basic
open_locale big_operators
@[simp] theorem geometric_progression_0_112 (n : ℕ) (a q : ℝ) (h : q ≠ 1) :
∑ (k : ℕ) in finset.range n, a * q ^ k = a * (q ^ n - 1) / (q - 1) := sorry
example (n : ℕ) (a q t : ℝ) : ∑ (k : ℕ) in finset.range n, a * q ^ k = t :=
begin
simp [show q ≠ 1, from sorry],
-- ⊢ a * (q ^ n - 1) / (q - 1) = t
end
```

I've definitely seen `simp`

lemmas in this way (and indeed, docs#nat.succ_succ_ne_one is a simp lemma too)

#### Kevin Buzzard (Sep 23 2022 at 10:50):

```
theorem sum_integers_0_121_7 (n : ℕ) :
∑ (k : ℕ) in finset.range (n + 1), (↑k : ℝ) ^ 7 = n ^ 2 * (n + 1) ^ 2 * (3 * n ^ 4 + 6 * n ^ 3 - n ^ 2 - 4 * n + 2) / 24 :=
begin
induction n with n ih,
{ simp, },
{ rw [finset.sum_range_succ, ih],
simp, ring,
},
end
```

This pattern can do all this stuff. Did you know that there's a general theorem for d'th powers involving Bernoulli polynomials? We might even have it in mathlib.

#### Kevin Buzzard (Sep 23 2022 at 10:52):

```
theorem convert_proof_real_to_nat (n : ℕ) (f g : ℕ → ℕ) :
∑ (k : ℕ) in finset.range (n + 1), (↑(f k) : ℝ) = ↑(g n) →
∑ (k : ℕ) in finset.range (n + 1), f k = g n :=
begin
intro h,
exact_mod_cast h,
end
```

#### Kevin Buzzard (Sep 23 2022 at 10:54):

```
@[simp] lemma pure_geometric_progression (n : ℕ) (q : ℝ) (h : q ≠ 1) :
∑ (k : ℕ) in finset.range n, q ^ k = (q ^ n - 1) / (q - 1) :=
begin
simpa using geometric_progression_0_112 n 1 q h,
end
```

`simpa using this`

is `simp at this, exact this`

#### Kevin Buzzard (Sep 23 2022 at 10:59):

```
lemma deriv_of_geometric_rv (n : ℕ) (x : ℝ) (h : x ≠ 1):
((↑n + 1) * x ^ n * (x - 1) - (x ^ (n + 1) - 1)) / (x - 1) ^ 2 =
∑ (k : ℕ) in finset.range n, (↑k + 1) * x ^ k :=
begin
exact (deriv_of_geometric n x h).symm,
end
```

Dot notation is super-cool! The type of `deriv_of_geometric n x h`

is `eq _ _`

so `(deriv_of_geometric n x h).symm`

means `eq.symm deriv_of_geometric n x h`

which you can use instead of the `symmetry`

tactic.

#### Kevin Buzzard (Sep 23 2022 at 11:07):

```
lemma deriv_of_geometric (n : ℕ) (x : ℝ) (h : x ≠ 1):
∑ (k : ℕ) in finset.range n, (↑k + 1) * x ^ k =
((↑n + 1) * x ^ n * (x - 1) - (x ^ (n + 1) - 1)) / (x - 1) ^ 2 :=
begin
-- proof which avoids analysis:
-- First clear denominators:
have foo : (x - 1) ≠ 0 := by { intro h2, apply h, linarith},
field_simp [foo],
-- now just use induction on n
induction n with d hd,
-- and it's just algebra
{ simp, },
{ rw [finset.sum_range_succ, add_mul, hd],
simp, ring_exp, },
end
```

You can't need analysis to prove this because it's true in any field. The algebra proof is far less painful than the analytic route you took (the algebra route completely involves the long `deriv_except_at_one`

)

#### Congzhou Sha (Sep 23 2022 at 14:45):

Kevin Buzzard said:

`lemma deriv_of_geometric (n : ℕ) (x : ℝ) (h : x ≠ 1): ∑ (k : ℕ) in finset.range n, (↑k + 1) * x ^ k = ((↑n + 1) * x ^ n * (x - 1) - (x ^ (n + 1) - 1)) / (x - 1) ^ 2 := begin -- proof which avoids analysis: -- First clear denominators: have foo : (x - 1) ≠ 0 := by { intro h2, apply h, linarith}, field_simp [foo], -- now just use induction on n induction n with d hd, -- and it's just algebra { simp, }, { rw [finset.sum_range_succ, add_mul, hd], simp, ring_exp, }, end`

You can't need analysis to prove this because it's true in any field. The algebra proof is far less painful than the analytic route you took (the algebra route completely involves the long

`deriv_except_at_one`

)

Yeah, it ‘s interesting how the easiest way to come up with the correct algebraic expression is to do the analysis route by pencil and paper, but then formalizing is easier with induction.

Thanks for all the suggestions, I’ll go through and streamline everything! There were definitely cases where `ring`

wasn’t able to solve the goal (cancelling terms like (1 - x) ^ 2 / (1 - x) ^ 3) and I had to manually cancel some terms, but I see you use `ring_exp`

for some of that

#### Kevin Buzzard (Sep 23 2022 at 17:15):

You just need to know the tricks (which you learn by trying stuff and then looking at other people's solutions, which is why I showed you some of my solutions). `ring`

can't deal with division because division isn't part of the structure of a ring. But there are tactics like `field_simp`

which are specifically designed for clearing denominators (division is part of the structure of a field).

Last updated: Aug 03 2023 at 10:10 UTC