Tsum in Zeta function

Stream: new members

[Brandon Werbel]

Hey all, my name is Brandon Werbel. Full disclosure, I'm still a senior in high school, meaning that everything I know after BC Calculus has been self-taught. I stumbled across Lean over the summer and, after making my way through the Natural Numbers Game (kudos by the way, great way of introducing new people to lean), I've started reading through TPL. I've currently finished the first three sections, and have plans to keep going.

I'm writing a paper for school about Bernoulli Numbers and the Riemann Zeta function, so I thought it would be interesting to practice with lean in this area. Unfortunately, I haven't gotten very far. I want to start by defining the Zeta function for real numbers, but haven't worked with infinite sums at all in lean. Here's all I have so far:

import topology.algebra.infinite_sum analysis.special_functions.pow

noncomputable def elem (x : ℝ) (n : ℕ) : ℝ := 1 / (n ^ x)
noncomputable def zeta (x : ℝ) : ℝ := tsum (elem x)

I'm not getting any errors with this, but I'm unable to check that zeta has been implemented the way it should be. I'm especially worried about this because, as I said before, I've never used tsum before and haven't been able to find good examples of it in use. I've tried things like #reduce zeta 2, but keep getting the (deterministic) timeout error. Any thoughts? Thanks in advance!

[Yaël Dillies]

You might have stuck on the wrong problem because people here have been thinking about defining the Riemann zeta function for years :sweat_smile: Let me ping @Kevin Buzzard who is one of the most knowledgeable people about this.

[Alex J. Best]

Your definition seems fine to me to define zeta for real x > 1, unfortunately reduce won't really do much useful on definitions such as this. reduce will only really expand the definitions of things, so you'll never see something mathematically non-trivial like zeta 2 = pi^2 / 6 or an approximation out of it. All you can really do is try to prove things about it

[Alex J. Best]

For instance you could try to prove that the function you defined is always positive and decreasing for x > 1

[Alex J. Best]

Using lemmas like docs#tsum_pos

[Alex J. Best]

Note that mathlib has docs#real.summable_one_div_nat_rpow already

[Brandon Werbel]

That makes sense, wasn't expecting it to see anything like pi ^2 / 6 from reduce. I was really more hoping for something like an approximation of the value, something I could check against a calculator to make sure I'm on the right track

[Brandon Werbel]

Yup, I also saw the p_series file in mathlib, I'm more working on this as a small challenge for myself to get to know lean better, not to contribute to mathlib

[Brandon Werbel]

Thanks for the ideas!

[Alex J. Best]

Yeah I was thinking more that the p-series file would be useful for you, glad you found it already! Unfortunately as far as I know there is no great way to see an approximation of a tsum in Lean, you can switch your definition to a finite sum and compute some values, but that's not always that helpful

[Brandon Werbel]

Awesome, that's good to know! I'll try working with some finite values, thanks!

[Junyan Xu]

You'd be interested in this thread.

[Kevin Buzzard]

I guess it might be quite tricky to do numerical approximations of zeta! @Brandon Werbel for a long time we had a definition of $\pi$ and could prove things like $\sin(\pi)=0$ but we couldn't even prove $\pi>3$. Lean's way of thinking about things like real numbers defined as infinite sums or zeros of functions is very different to the way numbers are taught in school, where one way of "understanding" a number is computing it to 5 decimal places; this is kind of psychological rather than anything else.

If you wanted to try a cool project then, because for a fixed real $x>1$ the function $n^{-x}$ is decreasing in $n$, one could use some kind of "integral test" to prove $\sum_{n\geq N}n^{-x}\leq \int_{N-1}^\infty t^{-x} dt$, evaluate this integral and thus prove an explicit error bound for the terms in the sum after some point. Once you have this you can get bounds for the whole sum by summing the first few terms, which should presumably be possible for $x$ an integer. But Lean is not a calculator! Even if you tried $x=1.5$ you'd still be stuck with evaluating $2^{1.5}$ and as far as I know Lean has no idea what that is. Again you would have to _prove_ anything you want to know about it -- for example you could prove $2.822<2^{1.5}<2.829$ by squaring both sides:

import data.real.pi.bounds

-- we have to *prove* this, we can't "compute" it.
-- The real numbers are not a computable object.
example : (2.828 : ℝ) < (2 : ℝ) ^ (1.5 : ℝ) :=
begin
  apply lt_of_pow_lt_pow 2,
  { apply real.rpow_nonneg_of_nonneg, -- powers of >= 0 are >= 0
    norm_num, -- no powers involved any more so the "normalise numerals" tactic works
  },
  { rw ← real.rpow_nat_cast (2 ^ _),
    rw ← real.rpow_mul, -- now all the powers are integers
    { norm_num, },
    { norm_num }, },
end

example : (2 : ℝ) ^ (1.5 : ℝ) < 2.829 :=
begin
  apply lt_of_pow_lt_pow 2,
  { norm_num, },
  { rw ← real.rpow_nat_cast (2 ^ _),
    rw ← real.rpow_mul, -- now all the powers are integers
    { norm_num, },
    { norm_num }, },
end

As you can see, Lean is not a "computer" in the sense that it is not designed to do computations, it's designed to prove theorems! When we switch to Lean 4 I suspect that more people will start thinking about how to make Lean a better computer, but right now it's mostly being used as a prover, and if you're pre-uni then you might well not have seen too many proofs, so it will be interesting to see what you manage to make the system do!

[Brandon Werbel]

Okay yeah, that makes sense, that Lean doesn't act as a computer, but a prover. Thanks for explaining it like that, it helps with the way I've been thinking about problems, especially irrational numbers.