# Zulip Chat Archive

## Stream: new members

### Topic: New to lean/mathlib. Trying to understand the library.

#### Samuel Cohn (Dec 01 2021 at 04:12):

Hello, I'm a former mathematician (analyst) now software engineer who got interested in the mathlib project from some of the Youtube lectures on it. I played the NNG and went through tutorial that uses sequences in $\mathbb{R}$ and had a great time! I figured the next step might be to try to prove some small result that no one had bothered to show, and I settled on the alternating series test. My first issue was just finding a definition of convergence. It seems that the preferred definition uses filters which I had once played with in an introductory topology class but is rather unfamiliar to me. By reading existing results I was able to settle on a statement for the result which seems correct:

```
theorem alternating_series_summable {f : ℕ → ℝ} (f_pos : ∀ n, f n ≥ 0) (hf : ∀ m n : ℕ, 0 < m → m ≤ n → f n ≤ f m) (converges_to_zero : filter.tendsto f filter.at_top (𝓝 0)) :
is_cau_seq absolute_value.abs (λ (k : ℕ), ( ∑ (i : ℕ) in (finset.Icc 0 k), (((-1) ^ i) * f (i)) ))
```

Even so, I now have to prove some basic facts about convergence of sequences in $\mathbb{R}$ using this definition that I don't know how to unpack easily.

Is there a definition of convergence on $\mathbb{R}$ or at least metric spaces which I can use to formulate the result in a slightly less abstract way? In general in mathlib, are theorems about more specific objects going to be referencing more general definitions in order to state or prove the result?

#### Mario Carneiro (Dec 01 2021 at 04:15):

I think you should be using docs#cauchy_seq instead of `is_cau_seq`

, which only exists for bootstrapping reasons

#### Mario Carneiro (Dec 01 2021 at 04:17):

Also, we have a definition of convergent sum but I think the sums in this theorem don't qualify since we require that sums are absolutely convergent

#### Mario Carneiro (Dec 01 2021 at 04:18):

I think it is more conventional to use `finset.range k`

as the sum's index set

#### Mario Carneiro (Dec 01 2021 at 04:19):

I suspect that you can prove `f_pos`

from the other assumptions

#### Samuel Cohn (Dec 01 2021 at 04:22):

Thanks for the suggestions. I agree that f_pos is superfluous.

#### Kevin Buzzard (Dec 01 2021 at 08:27):

As Mario says, the topological sum `tsum`

only works for absolutely convergent series. I don't think we have the definition of the sum of a series as taught to undergraduates! `tsum`

is a sum over the cofinite filter so must be invariant under rearrangement of the sum

#### Kevin Buzzard (Dec 01 2021 at 08:28):

I remember being surprised by this but then later on it occurred to me that maybe this basic notion is not actually used by analysts? I have no idea if this is true.

#### Kevin Buzzard (Dec 01 2021 at 08:28):

If this is just a fun first project then you can define infinite sums using the traditional definition yourself

#### Ruben Van de Velde (Dec 01 2021 at 08:33):

https://leanprover-community.github.io/undergrad_todo.html does indeed mention some things about series

#### Patrick Massot (Dec 01 2021 at 08:44):

About series vs sum, the main thing we never decided was whether we wanted the indexing set of series to be more general than natural numbers. But I now think we should go with nat, just to be able to remove those stupid items from the undergrad TODO list.

#### Patrick Massot (Dec 01 2021 at 08:45):

Samuel, you can get started on this lemma in an idiomatic way but removing all the scary stuff with:

```
import analysis.specific_limits -- This is a bit random but should be enough
open_locale big_operators topological_space
open filter finset
theorem cauchy_seq_of_alternating_series {f : ℕ → ℝ} (hf : antitone f)
(converges_to_zero : tendsto f at_top (𝓝 0)) :
cauchy_seq (λ k : ℕ, ∑ i in range k, (-1) ^ i * f i) :=
begin
simp only [metric.tendsto_at_top, real.dist_0_eq_abs] at converges_to_zero,
simp only [metric.cauchy_seq_iff, real.dist_eq],
sorry
end
```

#### Mario Carneiro (Dec 01 2021 at 08:45):

shouldn't there be a way to generalize it to other index filters beside the cofinite one? You can take the filter of upper integer sets to get the "undergraduate sum"

#### Patrick Massot (Dec 01 2021 at 08:46):

Mario, this was indeed the question. But nobody ever got interested enough to figure out the answer (it requires going through the main results we teach about series and check what remains true).

#### Mario Carneiro (Dec 01 2021 at 08:47):

Probably the alternating series test only works over nat

#### Mario Carneiro (Dec 01 2021 at 08:48):

but a reasonable starting point in any case is a filter-dependent `tsum`

#### Patrick Massot (Dec 01 2021 at 09:07):

The alternating series test is indeed pretty specific, but you could also start summing at any number in int.

#### Sebastien Gouezel (Dec 01 2021 at 10:07):

The `tsum`

we have currently is by very far the one that is most relevant in analysis. Sometimes when summing over nat one also uses the convergence along `range n`

, but it is not nearly well behaved as the previous one -- in a sense, it is closer to resummation methods for diverging series. So I'd rather go for a specific definition for this convergence over `range n`

, instead of changing the definition of `tsum`

by adding an additional filter. Note that here are other resummation methods that can not be expressed as a limit over a filter, so this new definition wouldn't be the right definition anyway.

#### Mario Carneiro (Dec 01 2021 at 10:09):

I didn't mean changing the definition of `tsum`

btw, I meant adding a `tsumf`

(name TBD) definition which takes a filter argument, which I'm sure will get a small fraction of the uses

#### Sebastien Gouezel (Dec 01 2021 at 10:10):

I'd say it depends on whether we have other applications in mind than `at_top nat`

for the filter.

#### Mario Carneiro (Dec 01 2021 at 10:11):

I think `at_top`

for other posets or directed sets can be used as well

#### Mario Carneiro (Dec 01 2021 at 10:12):

or `at_top.prod at_top`

for sums on `nat x nat`

#### Mario Carneiro (Dec 01 2021 at 10:12):

but, well, we've gotten this far exactly because it's a pretty niche situation

#### Sebastien Gouezel (Dec 01 2021 at 10:13):

Yes, it can definitely be used, but are there real examples in real mathematics?

#### Mario Carneiro (Dec 01 2021 at 10:13):

but I suspect having the full algebra will make it easier to prove some things by abstract nonsense involving map and comap

#### Mario Carneiro (Dec 01 2021 at 10:16):

we can also have a definition that specializes to `at_top nat`

, but having a common generalization will avoid needing to prove some theorems 2 or 3 times

#### Dylan MacKenzie (ecstatic-morse) (Jan 27 2022 at 01:12):

I *also* finished the natural game and picked the alternating series test from the list of missing undergraduate subjects as something relatively easy to attempt next. I checked for open PRs on the repo to see if anyone was working on it, but failed to search the Zulip instance (sorry!).

I managed to prove the following:

```
lemma alt_partial_sum_is_cauchy_seq
{a: ℕ → ℝ}
(ha_tendsto_zero : tendsto a at_top (𝓝 0))
(ha_anti : antitone a)
(ha_nonneg : ∀ n, 0 ≤ a n) -- could be derived from the first two
: cauchy_seq (λ k, ∑ n in range k, (-1)^n * a n) -- I also have a version for `-a n` (first term is negative)
```

Like Samuel Cohn, I got stuck when I tried to use this to prove `summable`

since it only works for absolutely convergent series, so I went looking for help and found this thread. I've since added a version of `summable`

that works over `range`

instead of all `finset`

s. It seems like something more general is desirable, although I didn't quite understand what Mario Carneiro wanted for `tsumf`

. This was my first encounter with filters, and while I found Patrick's talk and Kevin's blog post very helpful, they still confuse me. I was taught only the math needed for an electrical engineering degree, i.e. Fourier series and some basic arithmetic :smile:.

I pushed the proof to my mathlib branch in case anyone wants to take a look. I suspect it's pretty amateurish—this is my first attempt at formalizing something after all—but maybe some parts could be upstreamed into mathlib with a few tweaks?

#### Mario Carneiro (Jan 27 2022 at 01:21):

It looks pretty good overall. There are some minor style things but it looks ready for a PR

#### Dylan MacKenzie (ecstatic-morse) (Jan 27 2022 at 01:23):

That's great! I'll read the style guide and fix it up, as well as put the parity helpers in the correct module.

Could I have write access to non-master branches like the contributing guide suggests?

#### Mario Carneiro (Jan 27 2022 at 01:25):

invite sent

#### Dylan MacKenzie (ecstatic-morse) (Jan 27 2022 at 06:27):

Opened as #11689. I took out my alternate definition of`summable`

, changed some names ("alt" to "alternating") to be more consistent with mathlib, fixed at least some of the style things and did some :golf:. Hopefully it's not too bad.

#### Kevin Buzzard (Jan 27 2022 at 13:06):

Thanks for doing this!

#### Catherine Wraback (Jan 27 2022 at 21:23):

Hello everyone! I am new to using lean for my University research and had a question about a theorem that I came across in the mathlib documentation. I applied the tactic div_mul_div_cancel in my proof and for it to work I only had to specify that c didn't equal 0. Upon examining the documentation, I noticed that it only requires c to be nonzero, but not b. Could someone explain why b isn't required to be nonzero? I would think that it would be required because otherwise it leaves the possibility for an answer to be a/0 (if b was equal to 0).

I attached the theorem documentation below for easy reference! Thanks for the help!

```
theorem div_mul_div_cancel {G₀ : Type u_2} [group_with_zero G₀] {b c : G₀} (a : G₀) (hc : c ≠ 0) :
(a / c) * (c / b) = a / b
```

#### Patrick Massot (Jan 27 2022 at 21:24):

`a/0`

is defined to be zero so there is no issue.

#### Ruben Van de Velde (Jan 27 2022 at 21:24):

Division by zero is defined to yield zero. Do you see how that makes the theorem true?

#### Riccardo Brasca (Jan 27 2022 at 21:37):

Let me clarify that we are not crazy: we allow division by anything for practical reasons (it would be a nightmare to have a partially defined function), but the main theorem about division, namely `(a/b)*b = a`

holds only if b`≠ 0`

. Sometimes some results are true without `b ≠ 0`

, but this is essentially a coincidence (but we are happy to have one assumption less to verify).

#### Yaël Dillies (Jan 27 2022 at 22:00):

We tend to love those additional theorems a bit too much :sweat_smile:. For example, `(a + b)/c = a/c + b/c`

, `a/(a/a) = a`

, `a/b/(c/d) = d/c * a/b`

...

#### Johan Commelin (Jan 28 2022 at 03:19):

@Catherine Wraback See also https://xenaproject.wordpress.com/2020/07/05/division-by-zero-in-type-theory-a-faq/

#### Catherine Wraback (Jan 28 2022 at 15:05):

Johan Commelin said:

Catherine Wraback See also https://xenaproject.wordpress.com/2020/07/05/division-by-zero-in-type-theory-a-faq/

Thank you for linking this! That makes a lot more sense!

#### Bhavik Mehta (Jan 28 2022 at 15:22):

@Eric Rodriguez I think linking this on the FAQ could be helpful too!

Last updated: Dec 20 2023 at 11:08 UTC