Proving identities from Table of Integrals, Series, and Prod

Stream: general

[Congzhou Sha]

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]

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]

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]

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]

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]

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]

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]

@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_distribstuff -- 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]

Technically speaking, simp could prove q ≠ 1, but only in very few cases.

[Kevin Buzzard]

  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]

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]

  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]

  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]

    @[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]

    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]

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]

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]

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).