Zulip Chat Archive

Stream: maths

Topic: What's new in Lean maths?


view this post on Zulip Kevin Buzzard (Sep 09 2018 at 11:31):

This thread is for people to occasionally announce or flag code which they or others have written, which is publically available, finished / usable, and which might be of general use or interest to the lean community. I'm starting it because I find looking through mathlib commits confusing and time-consuming, and because there are things which are happening other than mathlib commits.

view this post on Zulip Kevin Buzzard (Sep 09 2018 at 11:38):

@Chris Hughes has proved quadratic reciprocity! This is a bit of a milestone because all proofs have some sort of a combinatorial / counting nature to them, and manipulating finite sets, whilst second nature to mathematicians, can be quite tough in Lean. The PR is still open; it's https://github.com/leanprover/mathlib/pull/327 . There's a bunch of other stuff too -- Fermat's Little Theorem, Wilson's Theorem, the Legendre symbol of course, multiplicative group of a finite field is cyclic and so on. This PR covers a serious chunk of the third year basic number theory course at Imperial College London.

view this post on Zulip Kevin Buzzard (Sep 09 2018 at 11:43):

On a rather more mundane note, work of several people at https://github.com/leanprover/mathlib/commit/4421f46dc2e0ec818344bcd897c1ee75ff82cbad and https://github.com/leanprover/mathlib/commit/085c0125015c29058ce5a418e88a791cb232ee4b has given us the fact that submodules of the quotient module M/Nbiject with submodules of M containing N and we now also have basic definitions of Noetherian modules plus proofs that submodules and quotient modules of Noetherian modules are Noetherian.

view this post on Zulip Johannes Hölzl (Sep 09 2018 at 11:56):

  • rcases (and hence rintros) supports now also quotient types. This allows one to write by rintro ⟨a⟩ ⟨b⟩; exact ... instead of a sequence of quotient.induction_on
  • (small change) more uniform naming filter.vmap is now filter.comap
  • we have our first concrete categories in Lean: CommRing, Top, and Meas! Due to @Scott Morrison and @Reid Barton

view this post on Zulip Patrick Massot (Sep 09 2018 at 18:34):

I think this thread is a very good idea. But we shouldn't forget to update documentation as well. Do we have an example of rcases using quotients in the tactic doc? I guess the quadratic reciprocity stuff should be mentioned in the theories folder of documentation

view this post on Zulip Patrick Massot (Sep 09 2018 at 18:35):

It seems https://github.com/leanprover/mathlib/blob/master/docs/tactics.md mentions quotients but there are not so many examples there

view this post on Zulip Mario Carneiro (Sep 09 2018 at 21:17):

/-- `filter [t1, ⋯, tn]` replaces a goal of the form `s ∈ f.sets`
and terms `h1 : t1 ∈ f.sets, ⋯, tn ∈ f.sets` with `∀x, x ∈ t1 → ⋯ → x ∈ tn → x ∈ s`.

`filter [t1, ⋯, tn] e` is a short form for `{ filter [t1, ⋯, tn], exact e }`.
-/
meta def filter_upwards
  (s : parse types.pexpr_list)
  (e' : parse $ optional types.texpr) : tactic unit

Since when did we have the near tactic?

view this post on Zulip Patrick Massot (Sep 09 2018 at 21:18):

I was about to try to find this

view this post on Zulip Patrick Massot (Sep 09 2018 at 21:18):

But I was never able to use it :(

view this post on Zulip Mario Carneiro (Sep 09 2018 at 21:19):

I recall Cyril showing a very nice version of this tactic in Coq

view this post on Zulip Johannes Hölzl (Sep 10 2018 at 01:54):

I added this 6 month ago. It's just a cheap version of Cyril's near tactic. Its more a reimplementation of Isabelle's eventually tactic

view this post on Zulip Mario Carneiro (Sep 10 2018 at 07:36):

Cross reference: abel tactic

view this post on Zulip Kevin Buzzard (Sep 10 2018 at 09:25):

Oh this is great news. Summary: the situation before this tactic was that we could prove things like (x+y)2=x2+2xy+y2(x+y)^2=x^2+2xy+y^2 if xx and yy were elements of a commutative ring (or even a commutative semiring) using the ring tactic, but for analogous questions about abelian groups the ring tactic did not work, and until now, if simp did not solve the goal, then one had to get one's hands dirty.

view this post on Zulip Kevin Buzzard (Sep 17 2018 at 14:27):

We have linarith, a new tactic that @Rob Lewis has written, which should definitely be mentioned here. It proves a bunch of things which hitherto were quite annoying / fiddly to prove. See it in action here: https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/subject/Feedback.20(Heine.20Borel.20in.20progress)/near/134050573 (e.g. proving that if 0 <= x then x/2 <= x).

view this post on Zulip Johan Commelin (Sep 21 2018 at 05:10):

Today Kevin Buzzard is turning 50 :birthday:. Congratulate him here!
With a group of people we have been hacking like crazy to give him some birthday presents:

  • @Chris Hughes Made immense (really immense!) progress on his exp branch in the community fork. We now have exp, cos, sin (all both complex and real), basic identities like sin_add, a proof that these functions are continuous, the intermediate value theorem, and finally pi. Yeah! :thumbs_up: :clink:
  • Other people have worked hard in a secret repository that is now public: https://github.com/semorrison/kbb (I sincerely apologize if you would have liked to participate but didn't know about this. I tried to contact as many people as I thought would be interested out of band, but of course I couldn't start a thread about this in the #general stream.)
  • This repository contains a definition of det (determinant of matrices) and a proof that it is a monoid morphism. Thanks @Kenny Lau
  • @Jack Crawford has a bunch of stuff on a different implementation of matrices. Well done! (There seems to be a trade-off, the current implementation of matrices is nice to prove things with, his could well be better for computations.)
  • A way to extract a matrix from a linear map between finite-dimensional vector spaces with bases.
  • Characteristic polynomials of square matrices. (But no properties at all.)
  • A proof that PID's are UFD's. Thanks @Johannes Hölzl (This result might be helpful for constructing splitting fields, because you want to know that an arbitrary (nonzero) polynomial factors into a product of irreducibles.)
  • A (admittedly ad-hoc) definition of the modular group, plus a boatload of facts about it (e.g., we have a finite set of representatives of the action of SL2Z on matrices (over int) with determinant m > 0).
  • A definition of complex derivatives, holomorphic function, modular forms.
  • A proof that holomorphic functions form a subring of the ring of functions (on an arbitrary open domain in the complex numbers).
  • A proof that modular forms form a submodule of functions on the upper half plane.
  • An almost definition of Hecke operators. (Sorry Kevin, Lean was fighting back hard.)
    Congratulations (and disucssions of about the maths!) can go here

view this post on Zulip Johan Commelin (Oct 02 2018 at 14:03):

It's time for an update in this thread. And someone should also start the corresponding thread in #general.

view this post on Zulip Johan Commelin (Oct 02 2018 at 14:03):

We now have Hensel's Lemma, thanks to @Rob Lewis

view this post on Zulip Johan Commelin (Oct 02 2018 at 14:04):

We also have holor. A holor is a generalisation of vectors and matrices. It is what the physicists would call a "tensor".

view this post on Zulip Johan Commelin (Oct 02 2018 at 14:05):

@Reid Barton Did a bunch of topology. Stuff on locally compact spaced. He also contributed groupoids.

view this post on Zulip Johan Commelin (Oct 02 2018 at 14:06):

Quadratic reciprocity has been merged. Once again: thanks @Chris Hughes

view this post on Zulip Rob Lewis (Oct 02 2018 at 14:06):

For the sake of completeness, the holor library is from @Alexander Bentkamp based on his work in Isabelle: https://link.springer.com/chapter/10.1007/978-3-319-66107-0_4

view this post on Zulip Patrick Massot (Oct 02 2018 at 14:24):

I don't see holors, locally compact spaces and quadratic reciprocity in https://github.com/leanprover/mathlib/tree/master/docs/theories :sad:

view this post on Zulip Kevin Buzzard (Oct 08 2018 at 16:56):

Thanks to Chris and Kenny, and inspired by work of my UROP students over the summer (especially @Morenikeji Neri ) we now have determinants! #404

view this post on Zulip Mario Carneiro (Oct 08 2018 at 16:58):

next stop characteristic polynomials?

view this post on Zulip Johan Commelin (Oct 08 2018 at 16:59):

Done in kbb

view this post on Zulip Kevin Buzzard (Oct 08 2018 at 17:01):

My birthday present just keeps on giving

view this post on Zulip Johan Commelin (Oct 08 2018 at 17:01):

You only turn 50 once...

view this post on Zulip Johan Commelin (Oct 15 2018 at 16:45):

Thanks to the hard work Johannes we now have a nice start on Lebesgue integration: https://github.com/leanprover/mathlib/commit/0fe284916a73ce92227f77826ad9655b1329eb83

view this post on Zulip Johan Commelin (Oct 15 2018 at 16:45):

Patrick and Johannes have worked very hard on quotient topologies on algebraic structures: https://github.com/leanprover/mathlib/commit/2395183b5b424371d5170f6c7bca691a654ae5bb

view this post on Zulip Johan Commelin (Oct 15 2018 at 16:46):

Chris proved that subgroups of cyclic groups are cyclic: https://github.com/leanprover/mathlib/commit/c5930f574c54e3fd157b1ef8b93da8b1f50c8ed4

view this post on Zulip Patrick Massot (Oct 15 2018 at 17:43):

Uniform spaces have Hausdorff completions https://github.com/leanprover/mathlib/blob/80d688e3ae2a721ab61f4cd000ea3e336158b04f/analysis/topology/completion.lean#L535. More precisely, there is a completion functor which is left-adjoint to the inclusion of complete Hausdorff spaces into all uniform spaces.

view this post on Zulip Patrick Massot (Oct 15 2018 at 17:46):

Abelian topological groups have a uniform space structure https://github.com/leanprover/mathlib/blob/80d688e3ae2a721ab61f4cd000ea3e336158b04f/analysis/topology/topological_groups.lean#L27 characterized by uniform continuity of substraction. The completion of such a topological group is a topological group with its canonical uniform structure (in particular the later is complete). Separated topological ring also have completions with the expected properties

view this post on Zulip Johannes Hölzl (Oct 17 2018 at 07:25):

I merged #386 Chris' PR about trigonometric functions. So we have pi, exp, etc now

view this post on Zulip Kenny Lau (Oct 17 2018 at 07:32):

looks like I messed up something. Could someone help reset leanprover-community/mathlib?

view this post on Zulip Johannes Hölzl (Oct 17 2018 at 07:33):

fixed

view this post on Zulip Kenny Lau (Oct 17 2018 at 07:35):

thanks

view this post on Zulip Johannes Hölzl (Oct 18 2018 at 07:44):

each PID is a UFD is now in mathlib

view this post on Zulip Johan Commelin (Nov 05 2018 at 19:24):

Ok, who is up for a summary of today?

view this post on Zulip Johan Commelin (Nov 05 2018 at 19:24):

First of all: the module refactor landed!

view this post on Zulip Johan Commelin (Nov 05 2018 at 19:24):

Second: Perfect closure has been merged.

view this post on Zulip Kevin Buzzard (Nov 05 2018 at 19:25):

This is a green light for algebraic closure and Galois theory

view this post on Zulip Johan Commelin (Nov 05 2018 at 19:26):

We now have all facts about irrational numbers that you would ever want to know.

view this post on Zulip Johan Commelin (Nov 05 2018 at 19:27):

(Ok, ok, we don't yet have irrationality op pi.)

view this post on Zulip Johan Commelin (Nov 05 2018 at 19:27):

We have Stone-Cech compactification.

view this post on Zulip Patrick Massot (Nov 19 2018 at 21:42):

Simon's monotonicity tactic has been merged in mathlib.

import tactic.monotonicity

example (x y z k m n : )
  (h₀ : z  0)
  (h₁ : y  x)
: (m + x + n) * z + k  z * (y + n + m) + k :=
by ac_mono*

view this post on Zulip Patrick Massot (Nov 19 2018 at 21:47):

We can combine with norm_num too:

example (α : Type) [linear_ordered_ring α] (x y z k : α)
  (h : z  y) :
  (k + 3 + x) - y  (k + 4 + x) - z := by mono* ; norm_num

view this post on Zulip Johan Commelin (Nov 20 2018 at 04:27):

Great news! Thanks @Simon Hudon! This is going to be very helpful. I really want to go back to the simplicial project now. Monotone functions are all over the place there.

view this post on Zulip Simon Hudon (Nov 20 2018 at 04:30):

Please keep me posted of ups and downs of using the tactic :)

view this post on Zulip Scott Morrison (Dec 02 2018 at 22:40):

(co)limits, and (co)limits in the category of Types!

view this post on Zulip Scott Morrison (Dec 02 2018 at 22:40):

There's still more to come (support for all the special shapes, products, equalizers, etc).

view this post on Zulip Scott Morrison (Dec 02 2018 at 22:42):

Also recently: equivalences of categories, along with a new tactic slice, for conving your way into long compositions, without having to use rw category.assoc by hand.

view this post on Zulip Patrick Massot (Jan 05 2019 at 10:46):

Sébastien's bounded continuous function has been merged :tada: Thank you so much Sébastien and Mario! This was a large PR, adding more than 600 lines to mathlib, even after getting Mario-compressed.

The type of bounded continuous functions from a topological space to a metric space, with the corresponding uniform distance. We prove basic statements such as the completeness of the space when the target is complete, and the Arzela-Ascoli theorem saying that a set of functions with a common modulus of continuity is compact. When the target space is a normed space, we also put the canonical normed space structure on the space of bounded continuous functions, working pointwise and checking that everything is compatible with the distance.

view this post on Zulip Sebastien Gouezel (Jan 05 2019 at 10:59):

Thanks a lot Mario, this is awesome!

view this post on Zulip Patrick Massot (Jan 18 2019 at 15:07):

@Johannes Hölzl could you tell us something about this Giry monad?

view this post on Zulip Johannes Hölzl (Jan 18 2019 at 15:24):

Yep, with the newest commits the Giry monad is in mathlib In category speak, its the monad for the measure functor in the category of measurable spaces and functions. With this we get a straight forward way to construct product: prod M1 M2 := do { x <- M1, y <- M2, return (x, y) }
Also I added measurable equivalences, which are helpful to adopt measurability proofs to different (but isomorphic) spaces

view this post on Zulip Johannes Hölzl (Jan 18 2019 at 15:25):

the Giry monad will be also important to write down probabilistic programs or constructions. Especially in the theorem of Ionescu-Tulcea it provides a construction mechanism for discrete-time stochastic processes out of Markov kernels

view this post on Zulip Simon Hudon (Jan 18 2019 at 20:17):

Can you use it in the category types?

view this post on Zulip Kevin Buzzard (Jan 18 2019 at 23:34):

@Luca Gerolla do you understand a word of this? Luca formalised some stochastic stuff in Lean

view this post on Zulip Luca Gerolla (Jan 19 2019 at 10:42):

I can understand the probability notions (after googling) - in class we just focused on Kolmogorov extension theorem since we only studied discrete time-homogeneous Markov processes.
Fascinating to see this general approach to formalise discrete-time stochastic processes :-)

view this post on Zulip Johannes Hölzl (Jan 19 2019 at 16:48):

the next step is to work on projective families, then Ionescu-Tulcea isn't far.

view this post on Zulip Johannes Hölzl (Jan 19 2019 at 16:49):

@Simon Hudon no, we need the category of measurable spaces

view this post on Zulip Simon Hudon (Jan 19 2019 at 18:25):

Doesn't that limit the applicability to writing programs?

view this post on Zulip Johannes Hölzl (Jan 20 2019 at 00:38):

Yes, the need to have a probability measure limits the program. Measurability is a very wide and adaptible concept. If you really want your program to be outside of measurability the Giry monad can't help you

view this post on Zulip Simon Hudon (Jan 20 2019 at 17:22):

I was wondering if you could embed it in type with a trick like:

structure M (a : Type) :=
(s : measurable_space)
(x : Giry s)
(f : s -> a)

view this post on Zulip Simon Hudon (Jan 20 2019 at 17:27):

That allows you to implement pure, map and (i believe) bind

view this post on Zulip Kevin Buzzard (Jan 20 2019 at 18:19):

A scheme is a topological space equipped with some structure and satisfying some axioms. It makes sense to talk about morphisms of schemes (which are continuous maps on the topological spaces plus some other data involving the extra structure plus some axioms), and schemes form a category.

The category of schemes has finite products. In short, if SS and TT are schemes, then there's a product scheme S×TS\times T, defined up to unique isomorphism, and satisfying the usual universal property. However the underlying topological space of a product of schemes is not the product of the underlying topological spaces (and the underlying type of a product is not the product of the underlying types).

I have no idea what monads have got to do with measure theory, but it occurred to me last week when talking to Ramon that with our scheme X idea (this is "unbundled", right?) where X is the underlying type, one can't use instances like scheme X -> scheme Y -> scheme X \times Y because that's the wrong product. Can I use monads in some crazy way to help here? @Johannes Hölzl seems to think that monads can help with products in this measurable situation...

What do products look like when everything gets bundled? Oh -- it's just a map scheme \times scheme -> scheme, right?

@Johan Commelin Why are you having trouble extending a sheaf on a basis to a sheaf on the space, when I managed to do it without using categories? Is this anything to do with bundling or is this just universe issues?

view this post on Zulip Johannes Hölzl (Jan 20 2019 at 23:13):

@Simon Hudon What is Giry s in your case? Is x a measure on s? And what is the measurable space ona?

view this post on Zulip Johannes Hölzl (Jan 20 2019 at 23:16):

@Kevin Buzzard I want to construct the usual product of the shape measure A -> measure B -> measure (A x B). This would be the expected product from measure theory (assuming sigma finite measures). Here the Giry monad allows a factored proof.
I don't see how monads will help with your problem...

view this post on Zulip Chris Hughes (Jan 21 2019 at 15:19):

(deleted)

view this post on Zulip Patrick Massot (Jan 22 2019 at 16:37):

Johannes and Sander defined the rank of a linear map!

view this post on Zulip Johannes Hölzl (Jan 23 2019 at 11:43):

PR #553 was merged, we have now Lipschitz continuous functions, the Banach fixed-point theorem

view this post on Zulip Johannes Hölzl (Jan 23 2019 at 11:43):

We also have the point wise order on products as the canonical order structure

view this post on Zulip Johannes Hölzl (Jan 23 2019 at 13:25):

seqeuence spaces (PR #440) is merged

view this post on Zulip Johannes Hölzl (Jan 24 2019 at 15:07):

Measures form a complete lattice now

view this post on Zulip Johannes Hölzl (Jan 28 2019 at 19:30):

@Kenny Lau 's module refactoring is in mathlib now. A type can now have multiple modules over different base rings.

view this post on Zulip Johannes Hölzl (Jan 29 2019 at 12:21):

@Chris Hughes splitting polynomials and clear_aux_decl are in mathlib now

view this post on Zulip Johan Commelin (Jan 29 2019 at 19:01):

This is great news! Thanks @Chris Hughes :tada:
This means that we can now define all sorts of interesting extensions of Q\mathbb{Q} and Qp\mathbb{Q}_p. Number theory is getting closer and closer!

view this post on Zulip Johannes Hölzl (Jan 29 2019 at 19:06):

no its not splitting fields, just the splitting polynomials. The splitting field PR is still a PR...

view this post on Zulip Johan Commelin (Jan 29 2019 at 19:06):

Aaah, too bad.

view this post on Zulip Kevin Buzzard (Jan 29 2019 at 20:16):

Number theory is still getting closer. I don't want to take on a new project right now but I feel like Dedekind domains might be accessible now, and probably would be an excellent test for the new module refactor.

view this post on Zulip Kevin Buzzard (Jan 29 2019 at 20:17):

That can happen independently of the Galois theory stuff happening at Imperial and of any number fields stuff, it's pure commutative algebra.

view this post on Zulip Johannes Hölzl (Jan 30 2019 at 08:50):

Congratulations to @Kenny Lau: his proof of the Hilbert basis theorem is now in mathlib!

view this post on Zulip Kenny Lau (Jan 30 2019 at 08:51):

Thanks!

view this post on Zulip Kevin Buzzard (Jan 30 2019 at 12:14):

I tried to prove Hilbert basis in September with the old version of modules and it was basically "impossible" -- I know that's a silly word, but what I mean is that the natural proof needed more from modules than mathlib could give me. Since then I've been regarding the proof of this theorem as a good benchmark for the theory of rings and modules, and think it's great that this now works. Commutative algebra is a bit like finite group theory -- there are a bunch of basic techniques, and once you have them all, there is a whole world of theorems which are accessible. It is also the correct generality for proofs of results which number theorists, algebraic geometers etc are interested in. As people might know, at Imperial we are working on Galois theory (mostly the students, not me) and if we can prove the fundamental theorem of Galois theory (FTG) then this will be an even more powerful indication that things are going in the right direction. I can do Hilbert basis in 30 minutes in a lecture and it only relies on the definition of a Noetherian ring, but FTG takes several lectures in total and also relies on a bunch of definitions like normal and separable field extensions.

view this post on Zulip Johannes Hölzl (Feb 06 2019 at 10:13):

We have now @Jan-David Salchow's opeartor name, and @Sebastien Gouezel's premetric spaces and fancy completion criteria. Also @Simon Hudon's fold theory is finally merged

view this post on Zulip Johan Commelin (Feb 06 2019 at 12:09):

Congrats to all of you. Especially @Simon Hudon that was quite a long delivery (-; :baby:

view this post on Zulip Simon Hudon (Feb 06 2019 at 13:12):

Thanks! :D

view this post on Zulip Johannes Hölzl (Feb 07 2019 at 12:34):

@Sebastien Gouezel's isometries and isometric isomorphisms are in mathlib!

view this post on Zulip Kevin Buzzard (Feb 07 2019 at 13:40):

So now how do we prove that if X and Y are isometric metric spaces, and if for all epsilon > 0 there's a covering of X by open discs of radius epsilon such that given any ten distinct discs in this covering, the intersection of these ten discs is empty, then the same is true for Y?

view this post on Zulip Sebastien Gouezel (Feb 07 2019 at 13:59):

Well, by hand, unfolding everything, business as usual. No transfer tactic yet. But now the question makes sense :)

view this post on Zulip Kenny Lau (Feb 16 2019 at 21:28):

Following the merge of #481 we now have a cleaner equivalence relation for localization, universal property of localization, and basic facts about ideals of localization.

view this post on Zulip Kevin Buzzard (Feb 16 2019 at 21:43):

But we don't have Neil's predicate. Will you PR it?

view this post on Zulip Kevin Buzzard (Feb 16 2019 at 21:43):

Then we'll have cleaner proofs that A[1/fg]=A[1/f][1/g]

view this post on Zulip Rob Lewis (Mar 01 2019 at 15:51):

Jeremy's derivatives PR #748 is merged. I believe this means that mathlib now has strictly more math than the Lean 2 library :tada:

view this post on Zulip Patrick Massot (Mar 29 2019 at 20:22):

We missed a couple of highlights in this thread. I can see at least:

view this post on Zulip Johan Commelin (Mar 29 2019 at 20:29):

@Abhimanyu Pallavi Sudhir defined the hyperreals

view this post on Zulip Johan Commelin (Apr 08 2019 at 07:27):

#851 Fundamental theorem of algebra has been merged. Kudos to @Chris Hughes

view this post on Zulip Johan Commelin (Apr 08 2019 at 11:31):

#881 We now have dual vector spaces and a proof that V and dual K V are isomorphic for fin.dim V. Kudos to @Fabian Glöckle

view this post on Zulip Kevin Buzzard (Apr 08 2019 at 11:46):

I showed Chris' proof to Chris' second year analysis lecturer (who taught him this theorem this term). He replied "it's quite difficult to understand -- what is the benefit of writing it in this way instead of LaTeX?"

view this post on Zulip Johan Commelin (Apr 08 2019 at 11:48):

I agree. And I hope that this proof becomes more readable if we have more theory.

view this post on Zulip Ramon Fernandez Mir (Apr 10 2019 at 19:54):

Hi there! I'm a final year Maths and Computing student at Imperial and I'm doing my Master's project with Kevin. For the last few months, I've been working on redefining schemes in Lean. I've completely refactored the lean-stacks-project repository and, even though it's still a work in progress, I'm glad to announce that it's in a good enough state to be shared. You can find it here: https://github.com/ramonfmir/lean-scheme. :-)

The main novelties are:

  • Locally ringed spaces.
  • Using the is_localization predicate to simplify the proof of the sheaf condition for the structure sheaf, avoiding all of the "canonical isomorphism nonsense".
  • Having no files named tagXXXX.lean.

In this time I've found quite a few definitions and lemmas that I believe should be in mathlib so I'll get them mathlib-ready and I'll start PR-ing them.

Also, especially since I know that there are things here which overlap with stuff that some of you are working on, I'd really appreciate your feedback.

view this post on Zulip Kevin Buzzard (Apr 10 2019 at 19:55):

Are you in some way suggesting that calling 20 files tagABCD.lean was in some way a bad idea? ;-)

view this post on Zulip Scott Morrison (Apr 10 2019 at 21:41):

In this time I've found quite a few definitions and lemmas that I believe should be in mathlib

This includes the definition of scheme, right?

view this post on Zulip Scott Morrison (Apr 10 2019 at 21:45):

Quite seriously, "good enough to be shared" is in my experience at most half the work of "usable by other people because it's in mathlib".

view this post on Zulip Scott Morrison (Apr 10 2019 at 21:45):

This isn't meant to be discouraging --- I would really really like to see actual maths in mathlib, and with schemes we're finally breaking into the 2nd half of last century. :-)

view this post on Zulip Scott Morrison (Apr 11 2019 at 02:34):

@Ramon Fernandez Mir, could we talk about refactoring this to use the category theory library? I would start at the file presheaf.lean, merging it with my PR #886.

view this post on Zulip Scott Morrison (Apr 11 2019 at 02:34):

Hopefully it is not actually that much work.

view this post on Zulip Mario Carneiro (Apr 11 2019 at 02:46):

yo people, this is an announce thread, take it somewhere else

view this post on Zulip Johan Commelin (Apr 17 2019 at 09:12):

We now have omega! Kudos to @Seul Baek!

view this post on Zulip Moses Schönfinkel (Apr 17 2019 at 10:27):

This should also be in #general! :)

view this post on Zulip Seul Baek (Apr 17 2019 at 12:45):

Thanks! :)

view this post on Zulip Patrick Massot (Jul 04 2019 at 11:38):

Some catching up for this thread:

Don't hesitate to add things I missed!

view this post on Zulip Johan Commelin (Sep 28 2019 at 02:46):

There is certainly a ton of stuff that has been flowing into mathlib, but most importantly: Sébastien's manifold PR just got merged!

view this post on Zulip Johan Commelin (Sep 28 2019 at 02:47):

@Kevin Buzzard (Now you can update your blogpost from January or something :grinning_face_with_smiling_eyes:)

view this post on Zulip Patrick Massot (Sep 28 2019 at 07:44):

It's a bit early to update this blogpost, we still don't have smooth manifold and the tangent functor.

view this post on Zulip Kevin Buzzard (Sep 28 2019 at 12:48):

I was looking at that blog post only yesterday, and realised I was looking forward to updating it.

view this post on Zulip Patrick Massot (Jul 10 2020 at 08:27):

I know we are very inconsistent in using this thread, but we now have a very nice opportunity: mathlib knows about Cayley-Hamilton! #3276

view this post on Zulip Patrick Massot (Aug 11 2020 at 08:22):

I see the Haar measure PR has been merged! This is a really nice addition to mathlib, and I wonder whether this has been formalized in any other proof assistant. Together with Yury's impressive work on integral refactoring and the fundamental theorem of calculus, it means measure theory and integration is turning into a really good shape.

view this post on Zulip Kevin Buzzard (Aug 11 2020 at 08:29):

Yeah this is awesome. It means we can state Pontryagin duality. But what are we going to do about the fact that the textbook proof is 50 pages of functional analysis but that I need it to state the generalized Riemann Hypothesis?

view this post on Zulip Scott Morrison (Aug 11 2020 at 10:02):

Surely we could state it already? Just talking about the dual group, or the evaluation map from the double dual to the original group, doesn't require knowing about Haar measure.

view this post on Zulip Patrick Massot (Aug 11 2020 at 10:07):

Kevin probably meant he wants Fourier transform.

view this post on Zulip Patrick Massot (Aug 11 2020 at 10:08):

How far are we from having Fubini's theorem? With FTC+Fubini we could say that we have integration in mathlib (maybe we would need completeness of LpL^p spaces to be honest).

view this post on Zulip Scott Morrison (Aug 11 2020 at 10:09):

But we should definitely do all the functional analysis in the vicinity of Pontryagin duality! My guess is that most of this material is going to be fairly pleasant to formalise.

view this post on Zulip Scott Morrison (Aug 11 2020 at 10:10):

I just PR'd a "Fubini" theorem that you will not appreciate. :-) #3732

view this post on Zulip Patrick Massot (Aug 11 2020 at 10:12):

Yes, I saw that PR yesterday and clicking on the link broke my heart. But keep up the good work on categories, we really need sheaves with values in a category!

view this post on Zulip Kevin Buzzard (Aug 11 2020 at 13:17):

Yes sorry, I want L^2(G)=L^2(Ghat) etc

view this post on Zulip Kenny Lau (Aug 12 2020 at 18:35):

rss-bot said:

feat(field_theory/algebraic_closure): algebraic closure (#3733)
feat(field_theory/algebraic_closure): algebraic closure (#3733)

instance : is_alg_closed (algebraic_closure k) :=

TODO: Show that any algebraic extension embeds into any algebraically closed extension (via Zorn's lemma).

Co-authored-by: Patrick Massot <patrickmassot@free.fr>
https://github.com/leanprover-community/mathlib/commit/eb4b2a05384b2c8e096c8c2d61f6e949a031493f

view this post on Zulip Kevin Buzzard (Aug 12 2020 at 19:09):

Reid would point out that you shouldn't have chosen an algebraic closure. It's not even unique up to unique isomorphism! You should have defined the category of algebraic closures of k and proved it's nonempty.

view this post on Zulip Floris van Doorn (Aug 13 2020 at 01:35):

Patrick Massot said:

How far are we from having Fubini's theorem? With FTC+Fubini we could say that we have integration in mathlib (maybe we would need completeness of LpL^p spaces to be honest).

I'm working towards Fubini's theorem. It will still be some work, I'm currently at the stage "define finitary products of measures".

view this post on Zulip Floris van Doorn (Aug 13 2020 at 01:35):

https://github.com/leanprover-community/mathlib/compare/measure-prod

view this post on Zulip Floris van Doorn (Aug 13 2020 at 01:36):

See also https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/product.20measures

view this post on Zulip Kenny Lau (Aug 13 2020 at 07:16):

Kevin Buzzard said:

Reid would point out that you shouldn't have chosen an algebraic closure. It's not even unique up to unique isomorphism! You should have defined the category of algebraic closures of k and proved it's nonempty.

that's is_alg_closed right; and inhabited implies nonempty?

view this post on Zulip Patrick Massot (Aug 13 2020 at 21:28):

I'm really thrilled to see that algebraic closure merged, for several reasons. The whole algebraic closure thing has become very embarrassing. And I'm also very happy to see a new very significant contribution by Kenny, after we failed to push through a number of attempts (collectively, the maintainer team and Kenny). Could we get a layman summary of what happened. Is this a new approach? Is this building on Chris's earlier work? Were there issues that Chris faced and were solved in the meantime?

view this post on Zulip Kevin Buzzard (Aug 13 2020 at 23:02):

Did you see that Larry Paulson wrote alg closures in Isabelle and wrote a paper about it, just a few months ago, crowing about how Isabelle was the first prover with alg closures?

view this post on Zulip Adam Topaz (Aug 13 2020 at 23:04):

Hey, it would be nice to do real closed fields. I'm sure the model theorists and the people working on o-minimality would be happy.

view this post on Zulip Adam Topaz (Aug 13 2020 at 23:05):

And sounds like isabelle doesn't have it :)

view this post on Zulip Aaron Anderson (Aug 13 2020 at 23:21):

You mean to construct the real closure?

view this post on Zulip Aaron Anderson (Aug 13 2020 at 23:22):

Now that algebraic closures exist, proving Artin-Schreier would be a lot easier, because you can build your real closure in the default algebraic closure

view this post on Zulip Adam Topaz (Aug 13 2020 at 23:30):

I'm thinking of the fact that any ordered field embeds in a RCF.

view this post on Zulip Adam Topaz (Aug 13 2020 at 23:30):

Artin-Schreier would be great!

view this post on Zulip Gabriel Ebner (Aug 14 2020 at 08:30):

@Chris Hughes That looks like a password.

view this post on Zulip Gabriel Ebner (Aug 14 2020 at 08:31):

@Rob Lewis Can you delete Chris' post?

view this post on Zulip Johan Commelin (Aug 14 2020 at 09:39):

@Floris van Doorn Congrats with the Haar measure! :octopus:

view this post on Zulip Johan Commelin (Aug 14 2020 at 09:39):

I'm quite excited returning from my holidays and seeing that we now have Haar measures and algebraic closures.

view this post on Zulip Kevin Buzzard (Aug 14 2020 at 09:40):

Welcome back Johan! By the way there about 20 things we need you to look at ;-)

view this post on Zulip Kevin Buzzard (Aug 14 2020 at 09:41):

Here's some stuff you can look at for fun (given that we're in the what's new thread): My MSc student Jujian Zhang got transcendence of e sorry-free! https://jjaassoonn.github.io/transcendental/

view this post on Zulip Kevin Buzzard (Aug 14 2020 at 09:42):

Euxodus reals (a construction of R from Z not going via Q) is at https://github.com/Lix0120/eudoxus/

view this post on Zulip Johan Commelin (Aug 14 2020 at 09:52):

Thanks, I hope transcendental will be PR'd?

view this post on Zulip Johan Commelin (Aug 14 2020 at 09:53):

About the 20 things, I would be happy if people would ping or PM me, and I'll try to look at everything over the next couple of days.

view this post on Zulip Kevin Buzzard (Aug 14 2020 at 09:57):

Oh I just meant the PR queue :-)

view this post on Zulip Kevin Buzzard (Aug 14 2020 at 09:58):

Shenyang Wu got group cohomology working: https://github.com/Shenyang1995/M4R although we had a shock at the last minute when he realised he hadn't defined H^0 :-) (because there are no -1-cochains in his set-up)

view this post on Zulip Kevin Buzzard (Aug 14 2020 at 09:59):

I can't guarantee any of this stuff will end up in mathlib. Students do projects and then they leave to do other things. I'll work on Jujian :-)

view this post on Zulip Yury G. Kudryashov (Aug 14 2020 at 16:21):

Can they at least open PRs and label them please-adopt?

view this post on Zulip Johan Commelin (Aug 14 2020 at 16:25):

Yes, please. That would be great.

view this post on Zulip Rob Lewis (Aug 15 2020 at 13:39):

With all these recent additions, someone should update the mathlib overview and probably the undergrad topics!

view this post on Zulip Patrick Massot (Aug 15 2020 at 16:34):

I added the Haar measure already. I'll add algebraic closures. For FTC I'm waiting for what Yury calls FTC-2 (in particular this is the version that allows to actually compute integrals).

view this post on Zulip Yury G. Kudryashov (Aug 16 2020 at 21:52):

I can easily add a weaker version assuming continuity of the derivative

view this post on Zulip Yury G. Kudryashov (Aug 16 2020 at 21:53):

The proof of the most general version for Lebesgue integral is far less trivial.

view this post on Zulip Kenny Lau (Aug 19 2020 at 06:31):

rss-bot said:

feat(miu_language): a formalisation of the MIU language described by …
feat(miu_language): a formalisation of the MIU language described by D. Hofstadter in "Gödel, Escher, Bach". (#3739)

We define an inductive type derivable so that derivable x represents the notion that the MIU string x is derivable in the MIU language. We show derivable x is equivalent to decstr x, viz. the condition that x begins with an M, has no M in its tail, and for which count I is congruent to 1 or 2 modulo 3.

By showing decidable_pred decstr, we deduce that derivable is decidable.
https://github.com/leanprover-community/mathlib/commit/5d2256da224ed7dfc5c20eb64cffb417d19377c5

rss-bot said:

feat(analysis/calculus) : L'Hôpital's rule, 0/0 case (#3740)
feat(analysis/calculus) : L'Hôpital's rule, 0/0 case (#3740)

This proves several forms of L'Hôpital's rule for computing 0/0 indeterminate forms, based on the proof given here : Wikibooks. See module docstring for more details.
https://github.com/leanprover-community/mathlib/commit/425aee91dfe8d542ecc39e354228f3f661af4b26

view this post on Zulip Johan Commelin (Aug 19 2020 at 12:47):

@Anatole Dedecker Can we now fill this in? Or is there another variant that should be done first?
https://github.com/leanprover-community/leanprover-community.github.io/blob/newsite/data/100.yaml#L193

view this post on Zulip Anatole Dedecker (Aug 19 2020 at 13:15):

Well there's only the 0/0 case for now, but I don't know if we should wait for the anything/infinity case. As I said in the PR I started working on it but I'm not focusing on it right now. Maybe we should have a look at which variations have been proven in other theorem provers to see if we should wait or not.

view this post on Zulip Johan Commelin (Aug 19 2020 at 13:16):

There is no hurry with adding things to that list

view this post on Zulip Johan Commelin (Aug 19 2020 at 13:17):

So let's wait for the infty version

view this post on Zulip Patrick Massot (Aug 19 2020 at 20:28):

I just checked and all entries on Freek's website are proving what Anatole proved. Given that we have no application in mind other than adding an item to this list, I don't see the point of waiting (and of working on other cases, but that's more debatable).

view this post on Zulip Mario Carneiro (Aug 19 2020 at 20:41):

I would say to report it as soon as you have something that can plausibly be given the name

view this post on Zulip Mario Carneiro (Aug 19 2020 at 20:42):

don't wait until you have the most general thing that can plausibly be given the name because mathematicians are ridiculously liberal about applying old names to vast generalizations

view this post on Zulip Johan Commelin (Aug 20 2020 at 02:57):

https://github.com/leanprover-community/leanprover-community.github.io/pull/117

view this post on Zulip Johan Commelin (Aug 25 2020 at 03:47):

rss-bot said:

feat(combinatorics): define simple graphs (#3458)
feat(combinatorics): define simple graphs (#3458)

adds basic definition of simple_graphs

Co-authored-by: Aaron Anderson <awainverse@gmail.com>
https://github.com/leanprover-community/mathlib/commit/d4d33deaa14500c982022408ad94b4979b7e337f

view this post on Zulip Johan Commelin (Aug 25 2020 at 03:47):

We finally have graphs!

view this post on Zulip Johan Commelin (Aug 25 2020 at 03:48):

Thanks a lot @Aaron Anderson @Jalex Stark @Kyle Miller and other contributors, for your perseverance

view this post on Zulip Kenny Lau (Aug 31 2020 at 06:45):

rss-bot said:

feature(algebraic_geometry/Scheme): the category of schemes (#3961)
feature(algebraic_geometry/Scheme): the category of schemes (#3961)

The definition of a Scheme, and the category of schemes as the full subcategory of locally ringed spaces.

Co-authored-by: Johan Commelin <johan@commelin.net>

Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Ashvni <ashvni.n@gmail.com>
https://github.com/leanprover-community/mathlib/commit/b79fc0379ae786153fc22ce5ee6751505e36a3d9

view this post on Zulip Scott Morrison (Sep 01 2020 at 22:46):

This is a tactic, not maths, but I hope mathematicians will enjoy @Simon Hudon's recently landed tactic:

import tactic.slim_check
import data.nat.prime

open nat

example (n : ) (p : prime n) : n^2 - 1 % 4 = 0 := by slim_check -- found problems, n := 2
example (n : ) (p : prime n) (h : 2 < n) : n^2 - 1 % 4 = 0 := by slim_check -- found problems, n := 3
example (n : ) (p : prime n) (h : 2 < n) : (n^2 - 1) % 4 = 0 := by slim_check -- gave up

view this post on Zulip Johan Commelin (Sep 02 2020 at 03:36):

@Simon Hudon You're a boss!

view this post on Zulip Simon Hudon (Sep 02 2020 at 03:41):

:bow:

view this post on Zulip Simon Hudon (Sep 02 2020 at 03:42):

I'm glad it's already popular :) I hope to see the generators that you guys come up with

view this post on Zulip Kevin Buzzard (Sep 02 2020 at 06:27):

That's a great showcase example Scott :-)

view this post on Zulip Scott Morrison (Sep 02 2020 at 06:57):

I'm embarrassed to say it's more realistic than it should have been --- In the second line I suspected slim_check before I suspected my parentheses. :-)

view this post on Zulip Kenny Lau (Sep 07 2020 at 11:47):

rss-bot said:

feat(algebraic_geometry/structure_sheaf): stalk_iso (#4047)
feat(algebraic_geometry/structure_sheaf): stalk_iso (#4047)

Given a ring R and a prime ideal p, construct an isomorphism of rings between the stalk of the structure sheaf of R at p and the localization of R at p.

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Johan Commelin <johan@commelin.net>
https://github.com/leanprover-community/mathlib/commit/94b96cff7665a86d9ea806ecb62eb60849d798a9

view this post on Zulip Kenny Lau (Sep 07 2020 at 11:48):

In symbols: OSpecR,p=Rp\mathcal O_{\operatorname{Spec} R, \mathfrak p} = R_{\mathfrak p}

view this post on Zulip Johan Commelin (Sep 07 2020 at 11:57):

Thanks a lot @Kenny Lau

view this post on Zulip Kevin Buzzard (Sep 07 2020 at 12:15):

Presumably we can state Gamma Spec Adjointness in the language of category theory already? Can we prove it?

view this post on Zulip Kevin Buzzard (Sep 07 2020 at 12:15):

I would not expect tidy to do it but it's worth a try :-)

view this post on Zulip Kevin Buzzard (Sep 07 2020 at 12:15):

@Kenny Lau is it accessible?

view this post on Zulip Scott Morrison (Sep 07 2020 at 12:49):

There's still a bit to do. Spec isn't even a functor yet.

view this post on Zulip Reid Barton (Sep 07 2020 at 13:08):

well, one way to make it a functor is to first prove it's adjoint to something :upside_down:

view this post on Zulip Kevin Buzzard (Sep 07 2020 at 13:31):

Is global sections a functor?

view this post on Zulip Kevin Buzzard (Sep 07 2020 at 13:31):

Spec being a functor doesn't sound hard

view this post on Zulip Kenny Lau (Sep 07 2020 at 13:31):

do we have morphisms yet?

view this post on Zulip Kevin Buzzard (Sep 07 2020 at 13:31):

In which category?

view this post on Zulip Kevin Buzzard (Sep 07 2020 at 13:32):

The category of locally ringed spaces I guess

view this post on Zulip Adam Topaz (Sep 07 2020 at 13:32):

Morphisms of schemes are there.

view this post on Zulip Adam Topaz (Sep 07 2020 at 13:32):

As a full subcat of locally ringed spaces

view this post on Zulip Kevin Buzzard (Sep 07 2020 at 13:33):

I see, so the content is getting the morphism of presheaves from the morphism of rings

view this post on Zulip Adam Topaz (Sep 07 2020 at 13:33):

I think what Reid was saying is that it would be just as easy to prove that Spec is a functor as it would be to prove the universal property of Spec, which is already the adjointness property :)

view this post on Zulip Kevin Buzzard (Sep 07 2020 at 13:33):

One should prove that it's a morphism of the underlying function type sheaf first and then verify that it preserves the predicate

view this post on Zulip Johan Commelin (Sep 07 2020 at 13:34):

If you want to state the adjunction for LRS, then it's easy. Because we have Spec as funtor to LRS

view this post on Zulip Johan Commelin (Sep 07 2020 at 13:34):

Uuh, maybe only on objects

view this post on Zulip Johan Commelin (Sep 07 2020 at 13:34):

But Spec as functor to schemes isn't done yet. We don't know that affine schemes are schemes.

view this post on Zulip Adam Topaz (Sep 07 2020 at 13:35):

Johan Commelin said:

But Spec as functor to schemes isn't done yet. We don't know that affine schemes are schemes.

Oh?

view this post on Zulip Kevin Buzzard (Sep 07 2020 at 13:35):

Oh I see!

view this post on Zulip Kevin Buzzard (Sep 07 2020 at 13:35):

Wait

view this post on Zulip Kevin Buzzard (Sep 07 2020 at 13:35):

I'm not sure i believe you

view this post on Zulip Johan Commelin (Sep 07 2020 at 13:35):

Well, after Kenny's PR, I guess we can now do that as well

view this post on Zulip Johan Commelin (Sep 07 2020 at 13:36):

The point was that we didn't know the stalks were local

view this post on Zulip Johan Commelin (Sep 07 2020 at 13:36):

Huh, now I'm confused

view this post on Zulip Johan Commelin (Sep 07 2020 at 13:36):

How did we define Spec as LRS before this PR?

view this post on Zulip Adam Topaz (Sep 07 2020 at 13:37):

LRS should be RS

view this post on Zulip Adam Topaz (Sep 07 2020 at 13:37):

That's how it was done before.

view this post on Zulip Johan Commelin (Sep 07 2020 at 13:38):

Yup, you're right

view this post on Zulip Kevin Buzzard (Sep 07 2020 at 13:40):

Aah got it

view this post on Zulip Johan Commelin (Sep 07 2020 at 13:45):

I have no idea how hard Spec as functor will be

view this post on Zulip Johan Commelin (Sep 07 2020 at 13:45):

Showing that you get local morphisms on the stalks... might be painful

view this post on Zulip Johan Commelin (Sep 07 2020 at 13:45):

As in... another PR of 200 lines?

view this post on Zulip Adam Topaz (Sep 07 2020 at 13:50):

Here's the proof in stacks: https://stacks.math.columbia.edu/tag/01I1

view this post on Zulip Adam Topaz (Sep 07 2020 at 13:51):

It looks like given a morphism AΓ(X,OX)A \to \Gamma(X,\mathcal{O}_X), where X is a LRS, it shouldn't be too hard to construct the associated morphism XSpecAX \to Spec A .

view this post on Zulip Adam Topaz (Sep 07 2020 at 13:51):

as ringed spaces, that is.

view this post on Zulip Kenny Lau (Sep 13 2020 at 10:48):

rss-bot said:

feat(algebraic_geometry/*): Gamma the global sections functor (#4126)
feat(algebraic_geometry/*): Gamma the global sections functor (#4126)
https://github.com/leanprover-community/mathlib/commit/5d35e626086c4e1639e49cd7cf574bc48592f554

view this post on Zulip Kenny Lau (Sep 14 2020 at 09:48):

rss-bot said:

feat(field_theory/fixed): dimension over fixed field is order of grou…
feat(field_theory/fixed): dimension over fixed field is order of group (#4125)

theorem dim_fixed_points (G : Type u) (F : Type v) [group G] [field F]
  [fintype G] [faithful_mul_semiring_action G F] :
  findim (fixed_points G F) F = fintype.card G

https://github.com/leanprover-community/mathlib/commit/1c2ddbcf800b070afddf1886e6329e400073b764

view this post on Zulip Johan Commelin (Sep 14 2020 at 09:51):

Galois theory is looming around the corner

view this post on Zulip Johan Commelin (Sep 14 2020 at 09:54):

Chapeau @Kenny Lau :clink:

view this post on Zulip Scott Morrison (Sep 14 2020 at 09:55):

I didn't even notice that PR going by. This is lovely!

view this post on Zulip Johan Commelin (Sep 14 2020 at 09:57):

@Kenny Lau Can you sketch what's left in your opinion? I guess

  • Define Galois group
  • Add an instance of faithful_mul_semiring_action (Gal L K) L under the assumption that the extension is normal and separable
  • An isomorphism between K and fixed_points (Gal L K) L
  • ...?

view this post on Zulip Kenny Lau (Sep 14 2020 at 10:14):

Tentative plan:

  1. Show the equivalence between "L/K is normal and separable" and "|Aut(L/K)| = [L:K]", and call one of those conditions "L/K is Galois".
  2. Show that if L/E/K is Galois then L/E is Galois (via normal and separable).
  3. Define Gal(L/E) : subgroup (Aut(L/K)) for E : subalgebra K L.
  4. Define fixed H : subalgebra K L for H : subgroup (Aut(L/K)).
  5. Then |Gal(L/fixed H)| = [L : fixed H] = |H| (2, #4125) so Gal(L/fixed H) = H.
  6. Then [L : fixed (Gal(L/E))] = |Gal(L/E)| = [L:E] (#4125, 2) so fixed (Gal(L/E)) = E.
  7. Show that the splitting field of a separable polynomial is Galois.

view this post on Zulip Kevin Buzzard (Sep 14 2020 at 10:17):

@Thomas Browning @Patrick Lutz and the other Berkeley people -- are you working on some of this stuff independently or are you all in sync and aware of each other's work?

view this post on Zulip Thomas Browning (Sep 14 2020 at 17:24):

Right now, we're temporarily paused on the Galois theory as we try to get the primitive element theorem into mathlib (which might make the forward direction of part 1 a bit easier). I'll make sure to keep track of what Kenny's doing.

view this post on Zulip Kevin Buzzard (Sep 14 2020 at 17:28):

I learnt the primitive element theorem in my Galois theory course :-)

view this post on Zulip Johan Commelin (Sep 27 2020 at 03:27):

rss-bot said:

feat(field_theory): prove primitive element theorem (#4153)
feat(field_theory): prove primitive element theorem (#4153)

Proof of the primitive element theorem. The main proof is in field_theory/primitive_element.lean. Some lemmas we used have been added to other files. We have also changed the notation for adjoining an element to a field to be easier to use.

Co-authored-by: Patrick Lutz <pglutz@berkeley.edu>
https://github.com/leanprover-community/mathlib/commit/253b120d59045b6eaec35781711be1d756f02fb3

view this post on Zulip Johan Commelin (Sep 27 2020 at 03:28):

rss-bot said:

feat(algebra/universal_enveloping_algebra): construction of universal…
feat(algebra/universal_enveloping_algebra): construction of universal enveloping algebra and its universal property (#4041)

Main definitions

* universal_enveloping_algebra
* universal_enveloping_algebra.algebra
* universal_enveloping_algebra.lift
* universal_enveloping_algebra.ι_comp_lift
* universal_enveloping_algebra.lift_unique
* universal_enveloping_algebra.hom_ext

Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
https://github.com/leanprover-community/mathlib/commit/d0b594766906c0e3ca9082228fffd8c9e0ff5435

view this post on Zulip Johan Commelin (Sep 27 2020 at 03:28):

rss-bot said:

feat(analysis/convex/integral): Jensen's inequality for integrals (#4…
feat(analysis/convex/integral): Jensen's inequality for integrals (#4225)
https://github.com/leanprover-community/mathlib/commit/5c957ec8b74ec01bad07c0f0455c31aa1795bc9f

view this post on Zulip Johan Commelin (Sep 27 2020 at 03:28):

That was a good day for mathlib (-;

view this post on Zulip Heather Macbeth (Oct 01 2020 at 23:10):

rss-bot said:

feat(analysis/normed_space/inner_product): Define the inner product b…
feat(analysis/normed_space/inner_product): Define the inner product based on is_R_or_C (#4057)
https://github.com/leanprover-community/mathlib/commit/9ceb1141fab68a2cd3ec27621018539bf1139d87

@Frédéric Dupuis Congratulations on this! I guess it's safe to formalize anything in Hilbert / Banach space theory now without worrying about duplication -- what will you do next?

view this post on Zulip Scott Morrison (Oct 01 2020 at 23:54):

This is really great! Let's make Banach/C-star/von Neumann algebras. :-)

view this post on Zulip Heather Macbeth (Oct 01 2020 at 23:54):

I think the next step should be the Hilbert projection theorem!

view this post on Zulip Heather Macbeth (Oct 01 2020 at 23:55):

Oops, I didn't mean that. We already have it.

view this post on Zulip Heather Macbeth (Oct 01 2020 at 23:55):

I meant its corollary, that the dual of a Hilbert space is isomorphic to itself!

view this post on Zulip Scott Morrison (Oct 01 2020 at 23:56):

I really don't know what we have in mathlib in this direction at the moment, but wish I did. Perhaps I should try to add something to learn. Any pointers or requests welcome. :-)

view this post on Zulip Heather Macbeth (Oct 01 2020 at 23:58):

Could you define the dual of a Hilbert space? We have the dual of a Banach space:
https://leanprover-community.github.io/mathlib_docs/analysis/normed_space/dual.html
and probably need to do some terrible trick like the product-of-metric-spaces trick to make the dual of a Hilbert space defeq

view this post on Zulip Heather Macbeth (Oct 01 2020 at 23:59):

But maybe I am speaking too soon, I feel like @Frédéric Dupuis should have first pick among all the new goodies available.

view this post on Zulip Heather Macbeth (Oct 02 2020 at 00:04):

By the way, @Scott Morrison, mathlib does have Banach algebras.
docs#normed_algebra
(plus complete_space). What do you want to do with them?

view this post on Zulip Scott Morrison (Oct 02 2020 at 00:04):

Oh! :-)

view this post on Zulip Scott Morrison (Oct 02 2020 at 00:05):

I didn't realise we'd already made it that far! In a former life I worked on von Neumann algebras (well, the entirely non-analytic story of the representation theory of subfactors, but anyway...) so it's just a direction I'd love to see in mathlib.

view this post on Zulip Scott Morrison (Oct 02 2020 at 00:06):

No particular concrete plans. I do have a branch where I prove Bell's inequality and Tsirelson's inequality, but I jump through some hoops to do them purely algebraically, rather than giving the natural C-star algebra proof.

view this post on Zulip Heather Macbeth (Oct 02 2020 at 00:10):

I don't know anything about this! But one could probably define a C-star algebra now, if that's the first step.

view this post on Zulip Frédéric Dupuis (Oct 02 2020 at 00:53):

Thanks @Heather Macbeth ! I agree that this dual business would be a natural next step. Working towards the spectral theorem would be nice also -- the finite dimensional case should be doable fairly soon now. @Alexander Bentkamp was hoping to work on this also, I believe?

view this post on Zulip Heather Macbeth (Oct 02 2020 at 00:58):

Another question is whether/how to rewrite
https://leanprover-community.github.io/mathlib_docs/analysis/normed_space/hahn_banach.html
using the new class. Maybe this can be done by identifying a core set of lemmas for the real case only, like you and Sébastien implemented with orthogonal projection.

view this post on Zulip Frédéric Dupuis (Oct 02 2020 at 01:00):

Right, with some luck this might turn out to be pretty easy.

view this post on Zulip Alexander Bentkamp (Oct 02 2020 at 07:24):

@Frédéric Dupuis said:

Thanks Heather Macbeth ! I agree that this dual business would be a natural next step. Working towards the spectral theorem would be nice also -- the finite dimensional case should be doable fairly soon now. Alexander Bentkamp was hoping to work on this also, I believe?

Great work on the is_R_or_C front! Don't expect too much from me in the coming months, though. I need to focus on my PhD thesis.

view this post on Zulip Frédéric Dupuis (Oct 02 2020 at 13:39):

BTW, @Scott Morrison I wouldn't mind having a look at that branch with the Bell and Tsirelson inequalities, I actually have no idea how to do this without at least C*-algebras!

view this post on Zulip Scott Morrison (Oct 03 2020 at 00:31):

There's nothing much to it. We define a star_ordered_ring as an ordered ring with a star structure, and a guarantee that star X * X is nonnegative. Then both the CHSH and Tsirelson inequalities can be proved by appropriate sums-of-squares decompositions. I actually can't remember for Tsirelson whether I found the relevant SOS decomposition somewhere, or found it myself in mathematica.

view this post on Zulip Scott Morrison (Oct 03 2020 at 00:31):

It's on the bell branch.

view this post on Zulip Scott Morrison (Oct 03 2020 at 00:31):

I'll PR soon.

view this post on Zulip Frédéric Dupuis (Oct 03 2020 at 01:22):

Ah I see! Is this star ordered ring something that's in common use somewhere, or did you come up with it for the occasion?

view this post on Zulip Scott Morrison (Oct 03 2020 at 01:29):

I don't recall seeing it used. It seemed a reasonable intermediate step on the way to Cstar algebras.

view this post on Zulip Scott Morrison (Oct 03 2020 at 01:30):

When you see people talking about the interaction of *-structures and orderings, sometimes instead people say that only the self-adjoint elements are ordered. I'm not sure why, however; it's still only a partial order.

view this post on Zulip Frédéric Dupuis (Oct 03 2020 at 01:44):

Yeah, I don't think I've ever seen anyone extend the ordering to non-self-adjoint elements.

view this post on Zulip Frédéric Dupuis (Oct 03 2020 at 01:45):

(Until today I guess!)

view this post on Zulip Patrick Massot (Jan 04 2021 at 08:39):

Since #4945, we have:

import measure_theory.interval_integral

open interval_integral

example :  (x : ) in 0..1, x = 1/2 :=
begin
  have : deriv (λ x : , x^2/2) = λ x, x,
  { ext x,
    simp, field_simp, ring },
  simp only [ this],
  rw integral_deriv_eq_sub,
  { norm_num },
  { simp },
  { rw this,
    exact continuous_id.continuous_on }
end

view this post on Zulip Patrick Massot (Jan 04 2021 at 08:40):

We are still far away from the target proof (which would be by compute), but this is still a huge relief.

view this post on Zulip Kevin Buzzard (Jan 04 2021 at 09:03):

Can we integrate x^n from 0 to 1 yet? x^2?

view this post on Zulip Bryan Gin-ge Chen (Jan 04 2021 at 09:14):

(Almost) the same proof works:

import measure_theory.interval_integral

open interval_integral

example (n : ) :  (x : ) in 0..1, x ^ n = 1 / (n + 1) :=
begin
  have : deriv (λ x : , x^(n + 1) / (n + 1)) = λ x, x ^ n,
  { ext x,
    have : (n + 1 : )  0 := by { norm_cast, linarith },
    simp, field_simp [this], ring },
  simp only [ this],
  rw integral_deriv_eq_sub,
  { norm_num },
  { simp },
  { rw this,
    exact (continuous_pow n).continuous_on }
end

view this post on Zulip Kevin Buzzard (Jan 04 2021 at 10:15):

How about sin(x)?

view this post on Zulip Patrick Massot (Jan 04 2021 at 10:24):

import measure_theory.interval_integral
import analysis.special_functions.trigonometric

open interval_integral real
open_locale real

example :  (x : ) in 0..π, sin x = 2 :=
begin
  have : deriv (λ x : , -cos x) = sin, by simp,
  simp only [ this],
  rw integral_deriv_eq_sub,
  { simp, ring },
  { simp },
  { rw this,
    exact continuous_sin.continuous_on }
end

view this post on Zulip Patrick Massot (Jan 04 2021 at 10:26):

For concrete computations like this, we clearly need a version of the lemma where we don't need to oscillate with rewriting using the derivative computation.

view this post on Zulip Rob Lewis (Jan 04 2021 at 10:34):

This is exactly the scenario where something like the Mathematica link is useful. You don't need to trust whatever computes the derivative, so you can farm it out to whatever system can manage.

view this post on Zulip Patrick Massot (Jan 04 2021 at 10:36):

It would be really nice to make this link actually usable for end users.

view this post on Zulip Sebastien Gouezel (Jan 04 2021 at 10:42):

A way to have a simple usable tactic would be for the user to provide the primitive. Then the tactic would try to close as many goals as possible using simp or continuity (which should be much faster once a new Lean release is made), and leave the remaining goals to the user.

view this post on Zulip Patrick Massot (Jan 04 2021 at 10:43):

I think Rob is saying that Mathematica or Sage or whatever could replace the user in your plan.

view this post on Zulip Rob Lewis (Jan 04 2021 at 10:48):

Indeed. It is usable if you have Mathematica installed and there's an example of it doing exactly this (with sorries of course).

view this post on Zulip Sebastien Gouezel (Jan 04 2021 at 10:51):

Sure, but it needs mathematica, so it should not stay like that in the final files. I imagine a tactic compute_integral [-sin], and a version compute_integral? that would call mathematica and output Try this: compute_integral [-sin].

view this post on Zulip Gabriel Ebner (Jan 04 2021 at 10:56):

Already a reformulation of integral_deriv_eq_sub goes a long way towards making this more readable:

import measure_theory.interval_integral
import analysis.special_functions.trigonometric

open interval_integral real set
open_locale real

theorem integral_deriv_eq_sub'
  {E} {f' :   E} {a b : } [measurable_space E] [normed_group E]
  [topological_space.second_countable_topology E]
  [complete_space E] [normed_space  E] [borel_space E]
  (f :   E)
  (hf' : deriv f = f')
  (hderiv :  x  interval a b, differentiable_at  f x)
  (hcont' : continuous_on f' (interval a b)) :
   y in a..b, f' y = f b - f a :=
by rw [ hf', integral_deriv_eq_sub hderiv]; cc

example :  x in 0..π, sin x = 2 :=
begin
  rw integral_deriv_eq_sub' (λ x, -cos x); simp,
  norm_num,
  exact continuous_sin.continuous_on,
end

If now simp could do norm_num, and we had automation for continuity..

view this post on Zulip Rob Lewis (Jan 04 2021 at 10:58):

simp doesn't do norm_num but norm_num does simp!

example :  x in 0..π, sin x = 2 :=
begin
  rw integral_deriv_eq_sub' (λ x, -cos x); norm_num,
  exact continuous_sin.continuous_on,
end

view this post on Zulip Rob Lewis (Jan 04 2021 at 10:59):

We do have continuity but it doesn't solve this, a missing attribute?

view this post on Zulip Kenny Lau (Jan 04 2021 at 11:00):

Wow, we have come a long way. This was certainly unimaginable when I first joined Gitter Lean.

view this post on Zulip Patrick Massot (Jan 04 2021 at 11:00):

Gabriel Ebner said:

Already a reformulation of integral_deriv_eq_sub goes a long way towards making this more readable:

Yes, this is exactly what I meant by "we clearly need a version of the lemma where we don't need to oscillate with rewriting using the derivative computation".

view this post on Zulip Kevin Buzzard (Jan 04 2021 at 11:02):

Kenny Lau said:

Wow, we have come a long way. This was certainly unimaginable when I first joined Gitter Lean.

That was three years ago. We're learning slower than a human student :-)

view this post on Zulip Sebastien Gouezel (Jan 04 2021 at 11:04):

lemma continuous_sin : continuous sin

is missing a continuity attribute, indeed.

view this post on Zulip Sebastien Gouezel (Jan 04 2021 at 11:08):

I wonder why

attribute [continuity] continuous_sin

example :  x in 0..π, sin x = 2 :=
begin
  rw integral_deriv_eq_sub' (λ x, -cos x);
  simp [continuous.continuous_on] {discharger := `[norm_num1 <|> continuity]},
end

fails. We are left with the goal 1 + 1 = 2, that norm_num1 should have closed.

view this post on Zulip Sebastien Gouezel (Jan 04 2021 at 11:14):

It's because the discharger only works on side conditions, but not on the main goal.

attribute [continuity] continuous_sin

example :  x in 0..π, sin x = 2 :=
begin
  rw integral_deriv_eq_sub' (λ x, -cos x);
  simp [continuous.continuous_on] {discharger := `[continuity]}; try {norm_num1},
end

works fine.

view this post on Zulip Kevin Buzzard (Jan 04 2021 at 11:37):

Well this is a really great development. I know Isabelle and Coq can do all this but I wonder how long it took them and I wonder how much of the multivariable stuff they have

view this post on Zulip Benjamin Davidson (Jan 07 2021 at 06:49):

I'm just seeing this conversation now, so I suppose I'm a bit late to the party, but I've actually been working on a few of these integration lemmas as a follow-up to #4945. I hadn't yet opened a PR since I was waiting to finish some on which I am stuck, but I would be glad to open a PR with the ones that are done. I had anyway been hoping that this could serve as part of a larger push to add more integration theorems to mathlib, and this way people could just add to the PR as they please. There is already some overlap with the lemmas discussed here.

view this post on Zulip Yury G. Kudryashov (Jan 07 2021 at 07:57):

#5647 drops some measurability assumptions in FTC-2

view this post on Zulip Floris van Doorn (Jan 07 2021 at 08:01):

At some point in the future we (also) need to drop some continuity assumptions in FTC-2, right?

view this post on Zulip Yury G. Kudryashov (Jan 07 2021 at 08:02):

Yes

view this post on Zulip Heather Macbeth (Jan 08 2021 at 06:18):

With #5300, we have the derivative of arcsin. Therefore by #4945 we have the integral of 1 / sqrt (1 - x ^ 2). So it should be possible to get the area of a circle (Freek prob 9) without much trouble.

I suppose one needs a few measure theory facts also -- eg, that the integral of the characteristic function of a set is the measure of the set (is this in mathlib?).

view this post on Zulip Heather Macbeth (Jan 08 2021 at 06:20):

exercise for @Anatole Dedecker @Andrew Souther @Benjamin Davidson @James Arthur ...?

view this post on Zulip Floris van Doorn (Jan 08 2021 at 06:20):

For the Lebesgue integral, it's docs#measure_theory.lintegral_indicator combined with docs#measure_theory.set_lintegral_one

view this post on Zulip Floris van Doorn (Jan 08 2021 at 06:21):

For the Bochner integral, also use docs#measure_theory.lintegral_coe_eq_integral or a nearby lemma

view this post on Zulip Heather Macbeth (Jan 08 2021 at 06:26):

One wants to apply this to a subset of R2\mathbb{R}^2 (the disc), so Floris' work on product measures should be involved somehow too.

view this post on Zulip Heather Macbeth (Jan 08 2021 at 06:31):

Heather Macbeth said:

exercise for Anatole Dedecker Andrew Souther Benjamin Davidson James Arthur ...?

(or someone on Kevin's discord server?)

view this post on Zulip Andrew Souther (Jan 08 2021 at 06:34):

I'd be happy to try helping with this :sweat_smile:

view this post on Zulip Kevin Buzzard (Jan 08 2021 at 10:31):

I think someone on the discord might be trying too -- just to let you know.

view this post on Zulip James Arthur (Jan 08 2021 at 10:47):

Heather Macbeth said:

exercise for Anatole Dedecker Andrew Souther Benjamin Davidson James Arthur ...?

working on it...

view this post on Zulip Heather Macbeth (Jan 09 2021 at 00:15):

@James Arthur Great! Looks like you are working on the fact that 1121x2dx=π\int_{-1}^12\sqrt{1-x^2}dx=\pi, maybe @Andrew Souther can work on the other part (that the measure of the unit disc is 1121x2dx\int_{-1}^12\sqrt{1-x^2}dx)?

view this post on Zulip Benjamin Davidson (Jan 09 2021 at 22:36):

I'd be happy to try working on this as well

view this post on Zulip Marc Masdeu (Jan 13 2021 at 15:29):

Benjamin Davidson said:

I'm just seeing this conversation now, so I suppose I'm a bit late to the party, but I've actually been working on a few of these integration lemmas as a follow-up to #4945. I hadn't yet opened a PR since I was waiting to finish some on which I am stuck, but I would be glad to open a PR with the ones that are done. I had anyway been hoping that this could serve as part of a larger push to add more integration theorems to mathlib, and this way people could just add to the PR as they please. There is already some overlap with the lemmas discussed here.

I have just opened my first PR (https://github.com/leanprover-community/mathlib/pull/5724), which proves integration by parts. It needs a lot of work probably to be accepted...is anyone interested in looking at it?

view this post on Zulip Heather Macbeth (Jan 13 2021 at 15:34):

Thanks, this is very welcome! I will look later today, and someone else may well get there first :)

view this post on Zulip Benjamin Davidson (Feb 23 2021 at 07:50):

Heather Macbeth said:

With #5300, we have the derivative of arcsin. Therefore by #4945 we have the integral of sqrt (1 - x ^ 2) (which is 12(x1x2+arcsin(x))\tfrac{1}{2}\left(x\sqrt{1-x^2}+\arcsin(x)\right). So it should be possible to get the area of a circle (Freek prob 9) without much trouble.

I suppose one needs a few measure theory facts also -- eg, that the integral of the characteristic function of a set is the measure of the set (is this in mathlib?).

This is finally here! #6374

view this post on Zulip Johan Commelin (Feb 23 2021 at 07:53):

@Benjamin Davidson should this be in archive/? I imagine this should just go somewhere in src/

view this post on Zulip Benjamin Davidson (Feb 23 2021 at 07:56):

We thought it shouldn't be in src/ because our definition of a disc is not optimal. There's a paragraph in the module docstring of the file which elaborates on that.

view this post on Zulip Johan Commelin (Feb 23 2021 at 08:01):

Ok, I'm not expert enough on this part of the library, but I would think that R×R\R \times \R is a common enough ambient space that your work can go in the main library.

view this post on Zulip Ruben Van de Velde (Feb 23 2021 at 08:26):

This doesn't necessarily need to block the PR, but do you know how much API is missing to use the euclidean_space definition / how hard it would be to add?

view this post on Zulip Benjamin Davidson (Feb 23 2021 at 08:54):

I believe @Floris van Doorn is working on it.

view this post on Zulip Benjamin Davidson (Feb 23 2021 at 08:55):

Let me link this discussion for reference.

view this post on Zulip Benjamin Davidson (Mar 02 2021 at 04:26):

Pertaining to the earlier discussion in this topic about integration...
rss-bot said:

feat(analysis/special_functions/integrals): some simple integration l…
feat(analysis/special_functions/integrals): some simple integration lemmas (#6216)

Integration of some simple functions, including sin, cos, pow, and inv. @ADedecker and I are working on the integrals of some more intricate functions, which we hope to add in a subsequent (series of) PR(s).

With this PR, simple integrals are now computable by norm_num. Here are some examples:

import analysis.special_functions.integrals
open real interval_integral
open_locale real

example :  x in 0..π, sin x = 2 := by norm_num
example :  x in 0..π/4, cos x = sqrt 2 / 2 := by simp
example :  x: in 2..4, x^(3:) = 60 := by norm_num
example :  x in 0..2, -exp x = 1 - exp 2 := by simp
example :  x: in (-1)..4, x = 15/2 := by norm_num
example :  x: in 8..11, (1:) = 3 := by norm_num
example :  x: in 2..3, x⁻¹ = log (3/2) := by norm_num
example :  x: in 0..1, 1 / (1 + x^2) = π/4 := by simp

integral_deriv_eq_sub' courtesy of @gebner.
https://github.com/leanprover-community/mathlib/commit/5c016137dd39d63112646c04432491130c6f5713

view this post on Zulip Yury G. Kudryashov (Mar 09 2021 at 18:19):

#6395 docs#paracompact_space merged, #6478 shrinking lemma is ready-to-merge

view this post on Zulip Johan Commelin (Mar 19 2021 at 10:30):

#6631: feat(field_theory/abel_ruffini): solvable by radicals implies solvable Galois group

view this post on Zulip Patrick Massot (Mar 19 2021 at 10:31):

Was this added to our mathlib overview?

view this post on Zulip Ruben Van de Velde (Mar 19 2021 at 10:39):

It was not

view this post on Zulip Johan Commelin (Mar 19 2021 at 10:42):

@Patrick Massot Good point, sorry that I forgot to check this before merging.
@Thomas Browning would you please PR an extra entry to the overview?

view this post on Zulip Mario Carneiro (Mar 19 2021 at 21:31):

Do we have unsolvability of the quintic yet? I assume this was the main missing piece

view this post on Zulip Kevin Buzzard (Mar 19 2021 at 21:32):

I'm pretty sure there was a mammoth effort to prove that x^5-x-1 had Galois group S_5 :-) (although they did go for a rather roundabout proof...). So perhaps all that's left is that S_5 is not solvable?

view this post on Zulip Thomas Browning (Mar 19 2021 at 23:20):

Two things left: S_5 is not solvable (practically done, just needs to be cleaned up & PRed), and constructing a polynomial with Galois group S_5.
For the latter there are two choices: x^5-4x+2 (we've done a fair amount of work in this direction, but there's more left), or x^n-x-1 (irreducibility is done and in the PR process, but getting Galois group S_n is harder and will require more algebraic number theory). We'll probably go with the former, but I would like to do the latter at some point.

view this post on Zulip Thomas Browning (Mar 19 2021 at 23:22):

The painful thing about x^5-4x+2 is that you have to work hands-on with its roots. In particular you have to show that it has 3 real roots, so that complex conjugation gives a transposition.

view this post on Zulip Heather Macbeth (Mar 19 2021 at 23:27):

Thomas Browning said:

The painful thing about x^5-4x+2 is that you have to work hands-on with its roots. In particular you have to show that it has 3 real roots, so that complex conjugation gives a transposition.

This is an intermediate value theorem argument, right?

view this post on Zulip Heather Macbeth (Mar 19 2021 at 23:27):

Or is there a better, "purely algebraic" way?

view this post on Zulip Thomas Browning (Mar 19 2021 at 23:36):

It's an intermediate value theorem argument, but you also have to argue that those are the only 3 real roots

view this post on Zulip Thomas Browning (Mar 19 2021 at 23:38):

And even then, it's painful to state and show that complex conjugation is a transposition

view this post on Zulip Heather Macbeth (Mar 19 2021 at 23:51):

Thomas Browning said:

It's an intermediate value theorem argument, but you also have to argue that those are the only 3 real roots

For this part, I guess we need an existence-and-uniqueness version of the intermediate value theorem, which applies when the function is monotone.

view this post on Zulip Heather Macbeth (Mar 19 2021 at 23:53):

The transposition argument sounds unpleasant :)

view this post on Zulip Kevin Buzzard (Mar 20 2021 at 00:53):

We have calculus now right? Isn't there even some old method of Newton for counting real roots of polynomials?

view this post on Zulip Yury G. Kudryashov (Mar 20 2021 at 01:55):

There's also an algorithm that takes the coefficients and tells the number of real roots on a given interval.

view this post on Zulip Yury G. Kudryashov (Mar 20 2021 at 01:56):

(on a given interval of ereal)

view this post on Zulip Yury G. Kudryashov (Mar 20 2021 at 01:59):

Probably formalizing it (as a theorem + tactic) is a good project on its own (but not required to deal with 1 specific polynomial).

view this post on Zulip Johan Commelin (Mar 20 2021 at 04:13):

Note that this is essentially nr.100 from Freek's list :rofl:

view this post on Zulip Mario Carneiro (Mar 20 2021 at 04:19):

To prove x^5-4x+2 has 3 real roots, it has at least 3 by the intermediate value theorem (evaluate at -large, 0, 1, large), and its derivative is 5x^4-4, which is convex, so it has at most 2 roots (rolle's theorem implies that if it has >3 roots then the derivative has >2 roots).

view this post on Zulip Thomas Browning (Mar 20 2021 at 04:20):

Yup, that's the proof that I had in mind

view this post on Zulip Alex J. Best (Mar 20 2021 at 04:48):

Johan Commelin said:

Note that this is essentially nr.100 from Freek's list :rofl:

A while ago I had a go at this, not sure I got very far and right now I can't continue this. But this is definitely a good project if someone wants to continue, or just start afresh :wink:. No idea what state this is in or even what proof I was following, so caveat emptor

import data.real.basic
import data.polynomial.field_division
import ring_theory.polynomial.basic
import init.algebra.order
import data.nat.parity
import tactic
open_locale classical
noncomputable theory

namespace polynomial
/-- pairs up consecutive elements of a list applies f and returns a list of length one less -/
def map_adjacent {α β : Type*} (f : α  α  β) (l : list α) : list β :=
l.zip_with f l.tail
#eval map_adjacent (+) [1, 2]
#eval map_adjacent (+) [1, 2, 3]
#eval map_adjacent (λ x y, (x < y : bool)) [1, 2, 1]
#eval map_adjacent (λ (x y : ), (xor (0 < x) (0 < y) : bool)) ([-2, 2, 1] : list )

variables {R : Type*} [linear_ordered_field R] {p : polynomial R}
/-- the (multi)-set of positive roots of a polynomial -/
def positive_roots (p : polynomial R) : multiset R := p.roots.filter (λ r, 0 < r)

lemma mem_positive_roots {x : R} : x  p.positive_roots  x  p.roots  0 < x :=
by rw [positive_roots, multiset.mem_filter]

lemma positive_roots_X_sub_C_of_zero_lt {x : R} (h : 0 < x) : (X - C x).positive_roots = {x} :=
begin
  rw [positive_roots, roots_X_sub_C, multiset.filter_cons_of_pos _ h, multiset.filter_zero],
  refl,
end

lemma positive_roots_normalize_eq_positive_roots :
  (normalize p).positive_roots = p.positive_roots :=
begin
  rw [positive_roots, roots_normalize],
  refl,
end

lemma positive_roots_mul {q : polynomial R} (hpq : p * q  0):
  (p * q).positive_roots = p.positive_roots + q.positive_roots :=
begin
  rw [positive_roots, roots_mul hpq, multiset.filter_add],
  refl,
end

lemma positive_roots_empty_of_positive_coeffs (h :  n  p.support, 0 < p.coeff n) :
  p.positive_roots =  :=
begin
  by_contra he,
  have hp : p  0 := begin
    intro hp,
    apply he,
    rw [positive_roots, hp, roots_zero, multiset.empty_eq_zero, multiset.filter_zero],
  end,
  obtain x, hx := multiset.exists_mem_of_ne_zero he,
  cases mem_positive_roots.mp hx with hxr hxp,
  rw [mem_roots hp, is_root.def, eval_eq_sum] at hxr,
  apply lt_irrefl (0 : R),
  nth_rewrite_rhs 0  hxr,
  convert finset.sum_lt_sum_of_nonempty _ _,
  swap,
  exact 0,
  simp only [pi.zero_apply, finset.sum_const_zero],
  exact nonempty_support_iff.mpr hp,
  intros n hn,
  specialize h n hn,
  rw [pi.zero_apply],
  exact mul_pos h (pow_pos hxp n),
end

/-- The sign changes of the non-zero coefficients of a polynomial-/
def sign_changes (p : polynomial R) : list Prop :=
  map_adjacent (λ i j, 0 < coeff p i * coeff p j) (p.support.sort ())
/-- The number of sign changes of the non-zero coefficients of a polynomial-/
def card_sign_changes (p : polynomial R) :  := (sign_changes p).count false
#print card_sign_changes
--lemma card_sign_changes_mul_X_sub_C_of_zero_lt (p : polynomial R) (x : R) (hx : 0 < x) :
--   :=sorry
#check coeff_mul_X_sub_C

lemma support_C_mul_of_ne_zero {x : R} (h : x  0) : (p * C x).support = p.support :=
begin
  ext,
  simp [mem_support_iff_coeff_ne_zero, h],
end

lemma card_sign_changes_normalize_eq_card_sign_changes :
  (normalize p).card_sign_changes = p.card_sign_changes :=
begin
  rw [card_sign_changes, sign_changes],
  simp only [coe_norm_unit, coeff_mul_C, normalize_apply],
  have :  {a b c : R} (hb : b  0), 0 < a * b * (c * b)  0 < a * c :=
  begin
    intros a b c hb,
    rw (by ring : a * b * (c * b) = a * c * b^2),
    have : 0 < b^2 := pow_two_pos_of_ne_zero b hb, -- TODO why does nlinarith need this
    rw (by {intro t; split; intro h; nlinarith, } :  t, 0 < t * b^2  0 < t),
  end,
  simp only [this (norm_unit p.leading_coeff).ne_zero],
  congr' 3,
  exact support_C_mul_of_ne_zero ((norm_unit (leading_coeff p)).ne_zero),
end

lemma coeff_mul_X_sub_C' {p : polynomial R} {r : R} {a : } :
  coeff (p * (X - C r)) a = (if 0 < a then coeff p (a - 1) else 0) - coeff p a * r :=
begin
  split_ifs,
  { have : a = (a - 1) + 1 := by omega,
    rw [this, coeff_mul_X_sub_C],
    simp, },
  { have : a = 0 := by omega, simp [this], },
end

lemma card_sign_changes_X_sub_C_mul {x : R} (hx : 0 < x) (hp : coeff p 0  0) :
  p.card_sign_changes + 1  ((X - C x : polynomial R) * p).card_sign_changes :=
begin
  rw mul_comm,
  simp only [card_sign_changes, sign_changes, coeff_mul_X_sub_C'],
  have : 0  (p * (X - C x)).support :=
  begin
    --simp only [finset.mem_sort],
    rw mem_support_iff_coeff_ne_zero,
    simp only [mul_coeff_zero, zero_sub, coeff_X_zero, ne.def, neg_eq_zero, coeff_C_zero, coeff_sub,
      mul_eq_zero],
    push_neg,
    exact hp, ne_of_gt hx⟩,
  end,
  have : (finset.sort has_le.le (p * (X - C x)).support).head = 0 :=
  begin
    rw [ list.nth_le_zero, finset.sorted_zero_eq_min'],
    apply nat.eq_zero_of_le_zero,
    exact finset.min'_le _ _ this,
    rw [finset.length_sort, finset.card_pos],
    exact 0, this⟩,
  end,
  cases h : finset.sort has_le.le (p * (X - C x)).support with hd tl;
  simp [h] at this,
  sorry,
  subst this,
  --simp_rw ← list.eq_ this,
  sorry,
end

theorem descartes_sign_rule' (hp : p  0) : p.positive_roots.card  card_sign_changes p :=
begin
  induction h : p.positive_roots.card generalizing p hp,
  { exact zero_le (card_sign_changes p), },
  { obtain x, hx := multiset.card_pos_iff_exists_mem.mp (by rw h; exact nat.succ_pos n),
    rw mem_positive_roots at hx,
    rw  h,
    have := mul_div_eq_iff_is_root.mpr ((mem_roots hp).mp hx.1),
    rw [ this, positive_roots_mul, multiset.card_add],
    calc (X - C x).positive_roots.card + (p / (X - C x)).positive_roots.card = 1 + (p / (X - C x)).positive_roots.card : by simp [positive_roots_X_sub_C_of_zero_lt hx.2]
      ...  1 + (p / (X - C x)).card_sign_changes : nat.add_le_add_left _ 1
      ... = (p / (X - C x)).card_sign_changes + 1 : add_comm _ _
      ...  ((X - C x) * (p / (X - C x))).card_sign_changes : card_sign_changes_X_sub_C_mul hx.2,
    { rw  this at hp,
      have : (p / (X - C x)).positive_roots.card = n :=
      begin
        rw [ this, positive_roots_mul hp] at h,
        simp [multiset.card_add, positive_roots_X_sub_C_of_zero_lt hx.2] at h,
        exact nat.succ.inj h,
      end,
      convert ih (right_ne_zero_of_mul hp) this, },
    { rw mul_div_eq_iff_is_root.mpr ((mem_roots hp).mp hx.1),
      exact hp, }, },
end

theorem descartes_sign_rule (hp : p  0) :
   d, card_sign_changes p = p.positive_roots.card + 2 * d :=
begin
  suffices :  {g : polynomial R} (hm : g.monic),
     d, card_sign_changes g = g.positive_roots.card + 2 * d,
  begin
    specialize this (polynomial.monic_normalize hp),
    rw [card_sign_changes_normalize_eq_card_sign_changes,
      positive_roots_normalize_eq_positive_roots] at this,
    exact this,
  end,
  clear_dependent p,
  intros,
  sorry
end
end polynomial

#lint

view this post on Zulip Alex J. Best (Mar 20 2021 at 04:52):

Maybe I was following http://sepwww.stanford.edu/data/media/public/oldsep/stew_save/descartes.pdf ?

view this post on Zulip Heather Macbeth (Mar 20 2021 at 04:52):

Mario Carneiro said:

To prove x^5-4x+2 has 3 real roots, it has at least 3 by the intermediate value theorem (evaluate at -large, 0, 1, large), and its derivative is 5x^4-4, which is convex, so it has at most 2 roots (rolle's theorem implies that if it has >3 roots then the derivative has >2 roots).

To rephrase this slightly: consider the three intervals (,2/54](-\infty, -\sqrt{2}/\sqrt[4]{5}] and [2/54,2/54][-\sqrt{2}/\sqrt[4]{5}, \sqrt{2}/\sqrt[4]{5}] and [2/54],)[\sqrt{2}/\sqrt[4]{5}], \infty). The function is monotone on each of these intervals and on each of the intervals the function when evaluated at the two endpoints has different signs. So there are three roots.

view this post on Zulip Heather Macbeth (Mar 20 2021 at 04:53):

Do we really need convexity, Rolle, etc? (Of course we do have these things if needed.)

view this post on Zulip Mario Carneiro (Mar 20 2021 at 11:39):

evaluating f(x):=x54x+2f(x):=x^5-4x+2 at 2/54\sqrt 2/\sqrt[4]5 and checking the sign sounds painful. Still, I think this works if you instead use monotonicity in the middle interval to prove f(2/54)f(0)>0f(-\sqrt 2/\sqrt[4]5)\ge f(0)>0 and monotonicity in the last interval to show f(2/54)f(1)<0f(\sqrt 2/\sqrt[4]5)\le f(1)<0

view this post on Zulip Kevin Buzzard (Mar 20 2021 at 12:33):

Checking the sign shouldn't be painful. Let x be sqrt(2)/5^{1/4}. It's easy enough to prove x^4=4/5 so now all you need is the sign of 2-3.2x which means you have to figure out which is bigger, 2 or 3.2x, but these are both positive so you can raise to the 4th power again.

view this post on Zulip Kevin Buzzard (Mar 20 2021 at 12:34):

Oh but I've just reread Mario's post and saw that he has a way around this :-)

view this post on Zulip Yury G. Kudryashov (Mar 26 2021 at 22:40):

Poincaré recurrence theorem #2311 is now merged to master

view this post on Zulip Kevin Buzzard (Mar 28 2021 at 21:12):

I see @Heather Macbeth has made the unit circle into a Lie group. I love work like this, because it shows that the general machinery we are creating can actually be used in practice. As many people will be aware, this is not automatic: for example we have a definition of complexes of objects in a category in mathlib and are just beginning to discover that actually it needs to be modified a little if we want to get a theory of cohomology of complexes which we can work with. One reason that it is so important to aim for the stars is that when you have grandiose goals in mind it forces you to get foundational stuff into mathlib and to get it working. If you look at e.g. the odd order theorem in Coq you see that this lofty goal ended up driving the development of mathcomp, for example.

Another lofty goal I always have at the back of my mind is the theory of automorphic forms and automorphic representations. The pre-adelic definition of these things involves CC^\infty functions on quotients of Lie groups like GLn(R)/GLn(Z)GL_n(\R)/GL_n(\Z) (or equivalently functions on GLn(R)GL_n(\R) which are GLn(Z)GL_n(\Z)-invariant) and which satisfy some differential equations coming from the universal enveloping algebra of the Lie algebra. With work of @Oliver Nash and others on Lie algebras, and now this, one can see these ideas becoming a bit closer to reality. How far are we from having groups like GLn(R)GL_n(\R) as Lie groups? Do we know that the tangent space at the origin of a Lie group is naturally a Lie algebra?

One of the big problems with Hales' dream to start formalising abstracts is that we still don't have so many of the words that research mathematicians use. I don't really have a good feeling as to what is missing in subjects like geometry, analysis etc, but in number theory there are a lot of fundamental definitions which are slowly moving from "crazy dream" to "actually might be possible if someone sits down and does it". Definitions are hard, and we don't always get them right first time. But our approach of "give it a go and see if it works" is I think paying big dividends. Congratulations to Heather, Yury, Sebastien, Nicolo and the others involved for making Lie groups and, importantly, giving a non-trivial example!

view this post on Zulip Heather Macbeth (Mar 28 2021 at 21:25):

GLn(k)GL_n(\mathbb{k}) is completely doable! See
https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/GL(n)
I think that @Nicolò Cavalleri may even have made a start on it. If not, it'd be a great exercise for someone looking to cut her teeth on the manifolds library.

view this post on Zulip Heather Macbeth (Mar 28 2021 at 23:04):

Oh also, if someone wants to prove that the unit quaternions are a Lie group, I think it would follow by very much the same argument as for the circle.

view this post on Zulip Kevin Buzzard (Mar 28 2021 at 23:09):

someone could do the unit reals as well, just to check there are no off-by-one errors :-)

view this post on Zulip Kevin Buzzard (Mar 28 2021 at 23:10):

My MSc student Shenyang Wu defined group cohomology as cocycles over coboundaries, and it was only when he was checking some examples about a week before the project deadline he discovered that his HnH^n was actually Hn+1H^{n+1} :-) Luckily he had time to fix it!

view this post on Zulip Scott Morrison (Mar 28 2021 at 23:11):

Unit octonions form a Lie loop? :-)

view this post on Zulip Bryan Gin-ge Chen (Mar 28 2021 at 23:11):

Kevin Buzzard said:

someone could do the unit reals as well, just to check there are no off-by-one errors :-)

Do we have an instance stating that all finite groups are Lie groups?

view this post on Zulip Heather Macbeth (Mar 28 2021 at 23:24):

Bryan Gin-ge Chen said:

Do we have an instance stating that all finite groups are Lie groups?

No, I don't think so, another good exercise for "someone" ... maybe the first step is to show that a set equipped with the discrete topology is a 0-dimensional smooth manifold.

view this post on Zulip David Michael Roberts (Mar 29 2021 at 00:01):

Scott Morrison said:

Unit octonions form a Lie loop? :-)

A nice small project, if not already done, is that the three Moufang identities all imply each other, and that octonions form a Moufang loop.

view this post on Zulip Scott Morrison (Mar 29 2021 at 00:26):

Do we have the octonions in the first place? I know some students in the past did the Cayley-Dickson construction, but as far as I know it wasn't PR'd.

view this post on Zulip Bryan Gin-ge Chen (Mar 29 2021 at 00:27):

I don't think we have the octonions yet, but we do have quaternions.

view this post on Zulip Bryan Gin-ge Chen (Mar 29 2021 at 00:32):

It'd be good to open mathlib issues for all these project ideas that are "within reach".

view this post on Zulip Scott Morrison (Mar 29 2021 at 00:46):

Hmm... I think there would be too many.

view this post on Zulip Scott Morrison (Mar 29 2021 at 00:46):

I agree we should have some mechanism!

view this post on Zulip Oliver Nash (Mar 29 2021 at 10:00):

Kevin Buzzard said:

Do we know that the tangent space at the origin of a Lie group is naturally a Lie algebra?

We do not yet know this but it is on one of my TODO lists. See also this old conversation: https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Lie.20groups.20and.20Lie.20algebras/near/198654172

Congratulations to Heather, Yury, Sebastien, Nicolo and the others involved for making Lie groups and, importantly, giving a non-trivial example!

Yes indeed. Congratulations and thank you to all of you. Seeing Lie groups come to life is really exciting!

view this post on Zulip Nicolò Cavalleri (Mar 30 2021 at 12:06):

Heather Macbeth said:

GLn(k)GL_n(\mathbb{k}) is completely doable! See
https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/GL(n)
I think that Nicolò Cavalleri may even have made a start on it. If not, it'd be a great exercise for someone looking to cut her teeth on the manifolds library.

Hey yes I did most of the work and I will publish it if someone wants to go on from what I've done. It is just very old code (I think from august) and I am having problems merging it, but I will write here when I'll be done

view this post on Zulip Yury G. Kudryashov (Mar 30 2021 at 21:03):

I formalized Urysohn's lemma in #6967. After a few attempts to formalize the proof from ncatlab I found a way to do it without "C x → C y → C ((x + y) / 2) recursion on dyadic rationals" (probably reinvented another wheel).

view this post on Zulip Yury G. Kudryashov (Mar 30 2021 at 21:03):

The "dyadic recursion" is much easier on paper than in Lean.

view this post on Zulip Yury G. Kudryashov (Mar 30 2021 at 21:04):

(especially if you want to construct a monotone family of open sets and use some properties of this family)

view this post on Zulip Bhavik Mehta (Mar 30 2021 at 21:08):

Yury G. Kudryashov said:

The "dyadic recursion" is much easier on paper than in Lean.

Could you say a bit more about why it's easier on paper than in Lean? I'm interested in arguments which are tricky in Lean when they don't feel tricky in maths

view this post on Zulip Yury G. Kudryashov (Mar 30 2021 at 21:11):

Have a look at the proof (see link above) and try to imagine how you will formalize it.

view this post on Zulip Yury G. Kudryashov (Mar 30 2021 at 21:16):

In one of the approaches, you have step : Π a b : α, a < b → {c // a < c ∧ c < b} (here α = opens X, a < b means closure a ⊆ b), a0, a1, and h01 : a0 < a1; then you need to construct a monotone function on dyadic rationals by using f ((x + y) / 2) = h (f x) (f y) _, where _ is a recursive proof of f x < f y.

view this post on Zulip Heather Macbeth (Mar 30 2021 at 21:16):

@Yury G. Kudryashov, this is great, I was going to try to resurrect Reid's proof of Urysohn (mentioned here) or re-prove it myself in the coming weeks. Can I ask what you need it for? I would like to know that continuous functions approximate in L^p the characteristic function of a measurable set (wrt a Radon measure) -- maybe this is something you are working on?

view this post on Zulip Heather Macbeth (Mar 30 2021 at 21:17):

Or, more generally (what I really want), that continuous functions are dense in L^p.

view this post on Zulip Yury G. Kudryashov (Mar 30 2021 at 21:17):

I'm working on smooth partitions of unity and it seems strange to formalize smooth partitions of unity without formalizing continuous version first.

view this post on Zulip Yury G. Kudryashov (Mar 30 2021 at 21:19):

So, I'm going to PR continuous partitions of unity and Tietze extension theorem.

view this post on Zulip Heather Macbeth (Mar 30 2021 at 21:21):

OK, I will work on consequences for L^p I mentioned, if that won't step on your toes.

view this post on Zulip Bhavik Mehta (Mar 30 2021 at 21:22):

Yury G. Kudryashov said:

In one of the approaches, you have step : Π a b : α, a < b → {c // a < c ∧ c < b} (here α = opens X, a < b means closure a ⊆ b), a0, a1, and h01 : a0 < a1; then you need to construct a monotone function on dyadic rationals by using f ((x + y) / 2) = h (f x) (f y) _, where _ is a recursive proof of f x < f y.

Right - does this not work?

view this post on Zulip Yury G. Kudryashov (Mar 30 2021 at 21:22):

This probably works but I failed to do it in a couple of evenings.

view this post on Zulip Yury G. Kudryashov (Mar 30 2021 at 21:23):

And I did the other proof in 1 morning.

view this post on Zulip Yury G. Kudryashov (Mar 30 2021 at 21:23):

And in less than 500 LOC including comments.

view this post on Zulip Bhavik Mehta (Mar 30 2021 at 21:24):

I see, so the standard proof is just harder to formalise than the one you found?

view this post on Zulip Yury G. Kudryashov (Mar 30 2021 at 21:25):

Yes (or I missed some nice way to formalize it).

view this post on Zulip David Wärn (Mar 30 2021 at 21:37):

I don't know this argument very well, so maybe this is nonsense / not helpful, but docs#order.ideal_of_cofinals is meant to help with some abstraction for this kind of countable recursion (if you want to use something like the dyadic argument). Here you would define a poset P of 'finite approximations', let's say a term consists of a finite subset of [0,1] together with appropriate open sets U(r), V(r) (following Wikipedia) for every r in this finite subset. Then you would show that for any x in [0, 1], any finite approximation can be extended so as to include x (this corresponds to defining a cofinal set in P). Then you take your favourite countable dense subset of [0, 1], and docs#order.ideal_of_cofinals on the corresponding countable family of cofinals should give you what you need

view this post on Zulip Yury G. Kudryashov (Mar 30 2021 at 22:00):

I'll have a look at this later (we can have two proofs, one in examples).

view this post on Zulip Yury G. Kudryashov (Mar 31 2021 at 19:07):

Smooth bump functions docs#smooth_bump_function and a baby version of Whitney's weak embedding theorem docs#exists_embedding_findim_of_compact are now in master.

view this post on Zulip Gihan Marasingha (May 07 2021 at 18:25):

Kevin Buzzard said:

...
Another lofty goal I always have at the back of my mind is the theory of automorphic forms and automorphic representations
...

Is there anything even on classical modular forms in mathlib or is the idea first to develop the more general theory? Is there any value in working on special cases?

view this post on Zulip Kevin Buzzard (May 07 2021 at 19:22):

There are several people who might be working on modular forms and I have a student who will be working on them with me this summer. I'm not 100% sure if these people want to go public yet so I'm not entirely sure what else to say, but as far as I know we don't even have a definition yet in mathlib. Things like Hecke operators should be easy, boundedness conditions at cusps can be done with a hack (you don't need to develop a theory of holomorphic functions on an open disc, although of course this is also something that desperately needs doing) and the big problem will be proving that the spaces are finite-dimensional because this basically is finiteness of coherent cohomology of a compact Riemann surface and it will also take a lot of work to reduce it to this case. Riemann-Roch is another approach but again this will be tons of work. Without finite-dimensionality you're rather limited in what you can do in the general theory, however there are tons of examples one could do which don't need this, for example Eisenstein series, theta series, Delta and so on


Last updated: May 09 2021 at 09:11 UTC