New to lean/mathlib. Trying to understand the library.

Stream: new members

[Samuel Cohn]

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]

I think you should be using docs#cauchy_seq instead of is_cau_seq, which only exists for bootstrapping reasons

[Mario Carneiro]

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]

I think it is more conventional to use finset.range k as the sum's index set

[Mario Carneiro]

I suspect that you can prove f_pos from the other assumptions

[Samuel Cohn]

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

[Kevin Buzzard]

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]

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]

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

[Ruben Van de Velde]

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

[Patrick Massot]

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]

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]

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]

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]

Probably the alternating series test only works over nat

[Mario Carneiro]

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

[Patrick Massot]

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

[Sebastien Gouezel]

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]

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]

I'd say it depends on whether we have other applications in mind than at_top nat for the filter.

[Mario Carneiro]

I think at_top for other posets or directed sets can be used as well

[Mario Carneiro]

or at_top.prod at_top for sums on nat x nat

[Mario Carneiro]

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

[Sebastien Gouezel]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

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 finsets. 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]

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

[Dylan MacKenzie (ecstatic-morse)]

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]

invite sent

[Dylan MacKenzie (ecstatic-morse)]

Opened as #11689. I took out my alternate definition ofsummable, 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]

Thanks for doing this!

[Catherine Wraback]

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]

a/0 is defined to be zero so there is no issue.

[Ruben Van de Velde]

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

[Riccardo Brasca]

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]

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]

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

[Catherine Wraback]

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]

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