What's new in Lean maths?

Stream: maths

[Kevin Buzzard]

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.

[Kevin Buzzard]

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

[Kevin Buzzard]

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.

[Johannes Hölzl]

• 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

[Patrick Massot]

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

[Patrick Massot]

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

[Mario Carneiro]

/-- `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?

[Patrick Massot]

I was about to try to find this

[Patrick Massot]

But I was never able to use it :(

[Mario Carneiro]

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

[Johannes Hölzl]

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

[Mario Carneiro]

Cross reference: abel tactic

[Kevin Buzzard]

Oh this is great news. Summary: the situation before this tactic was that we could prove things like $(x+y)^2=x^2+2xy+y^2$ if $x$ and $y$ 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.

[Kevin Buzzard]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Rob Lewis]

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

[Patrick Massot]

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

[Kevin Buzzard]

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

[Mario Carneiro]

next stop characteristic polynomials?

[Johan Commelin]

Done in kbb

[Kevin Buzzard]

My birthday present just keeps on giving

[Johan Commelin]

You only turn 50 once...

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Patrick Massot]

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.

[Patrick Massot]

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

[Johannes Hölzl]

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

[Kenny Lau]

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

[Johannes Hölzl]

fixed

[Kenny Lau]

thanks

[Johannes Hölzl]

each PID is a UFD is now in mathlib

[Johan Commelin]

Ok, who is up for a summary of today?

[Johan Commelin]

First of all: the module refactor landed!

[Johan Commelin]

Second: Perfect closure has been merged.

[Kevin Buzzard]

This is a green light for algebraic closure and Galois theory

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

We have Stone-Cech compactification.

[Patrick Massot]

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*

[Patrick Massot]

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

[Johan Commelin]

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.

[Simon Hudon]

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

[Scott Morrison]

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

[Scott Morrison]

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

[Scott Morrison]

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.

[Patrick Massot]

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.

[Sebastien Gouezel]

Thanks a lot Mario, this is awesome!

[Patrick Massot]

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

[Johannes Hölzl]

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

[Johannes Hölzl]

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

[Simon Hudon]

Can you use it in the category types?

[Kevin Buzzard]

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

[Luca Gerolla]

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

[Johannes Hölzl]

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

[Johannes Hölzl]

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

[Simon Hudon]

Doesn't that limit the applicability to writing programs?

[Johannes Hölzl]

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

[Simon Hudon]

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)

[Simon Hudon]

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

[Kevin Buzzard]

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 $S$ and $T$ are schemes, then there's a product scheme $S\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?

[Johannes Hölzl]

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

[Johannes Hölzl]

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

[Chris Hughes]

(deleted)

[Patrick Massot]

Johannes and Sander defined the rank of a linear map!

[Johannes Hölzl]

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

[Johannes Hölzl]

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

[Johannes Hölzl]

seqeuence spaces (PR #440) is merged

[Johannes Hölzl]

Measures form a complete lattice now

[Johannes Hölzl]

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

[Johannes Hölzl]

@Chris Hughes splitting polynomials and clear_aux_decl are in mathlib now

[Johan Commelin]

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

[Johannes Hölzl]

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

[Johan Commelin]

Aaah, too bad.

[Kevin Buzzard]

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.

[Kevin Buzzard]

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

[Johannes Hölzl]

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

[Kenny Lau]

Thanks!

[Kevin Buzzard]

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.

[Johannes Hölzl]

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

[Johan Commelin]

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

[Simon Hudon]

Thanks! :D

[Johannes Hölzl]

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

[Kevin Buzzard]

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?

[Sebastien Gouezel]

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

[Kenny Lau]

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.

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Rob Lewis]

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

[Patrick Massot]

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

• Sébastien proved Baire's theorem
• Kenny proved Nakayma's lemma
• Alexander introduced convex sets and functions

[Johan Commelin]

@Abhimanyu Pallavi Sudhir defined the hyperreals

[Johan Commelin]

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

[Johan Commelin]

#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

[Kevin Buzzard]

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?"

[Johan Commelin]

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

[Ramon Fernandez Mir]

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.

[Kevin Buzzard]

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

[Scott Morrison]

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?

[Scott Morrison]

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

[Scott Morrison]

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

[Scott Morrison]

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

[Scott Morrison]

Hopefully it is not actually that much work.

[Mario Carneiro]

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

[Johan Commelin]

We now have omega! Kudos to @Seul Baek!

[Moses Schönfinkel]

This should also be in #general! :)

[Seul Baek]

Thanks! :)

[Patrick Massot]

Some catching up for this thread:

• Michael Howes defined group presentations
• Kenny defined direct limit of modules, abelian groups, rings, and fields and constructed integral closures in commutative rings
• Sébastien proved the open mapping theorem
• Paul-Nicolas made a normalize cast tactic
• Scott defined monoidal categories
• Joe defined the Bochner integral
• Alexander refactored linear combinations

Don't hesitate to add things I missed!

[Johan Commelin]

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

[Johan Commelin]

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

[Patrick Massot]

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

[Kevin Buzzard]

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

[Patrick Massot]

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

[Patrick Massot]

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.

[Kevin Buzzard]

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?

[Scott Morrison]

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.

[Patrick Massot]

Kevin probably meant he wants Fourier transform.

[Patrick Massot]

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 $L^p$ spaces to be honest).

[Scott Morrison]

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.

[Scott Morrison]

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

[Patrick Massot]

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!

[Kevin Buzzard]

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

[Kenny Lau]

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

[Kevin Buzzard]

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.

[Floris van Doorn]

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 $L^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".

[Floris van Doorn]

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

[Floris van Doorn]

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

[Kenny Lau]

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?

[Patrick Massot]

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?

[Kevin Buzzard]

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?

[Adam Topaz]

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.

[Adam Topaz]

And sounds like isabelle doesn't have it :)

[Aaron Anderson]

You mean to construct the real closure?

[Aaron Anderson]

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

[Adam Topaz]

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

[Adam Topaz]

Artin-Schreier would be great!

[Gabriel Ebner]

@Chris Hughes That looks like a password.

[Gabriel Ebner]

@Rob Lewis Can you delete Chris' post?

[Johan Commelin]

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

[Johan Commelin]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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/

[Kevin Buzzard]

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

[Johan Commelin]

Thanks, I hope transcendental will be PR'd?

[Johan Commelin]

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.

[Kevin Buzzard]

Oh I just meant the PR queue :-)

[Kevin Buzzard]

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)

[Kevin Buzzard]

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

[Yury G. Kudryashov]

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

[Johan Commelin]

Yes, please. That would be great.

[Rob Lewis]

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

[Patrick Massot]

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

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

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

[Kenny Lau]

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

[Johan Commelin]

@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

[Anatole Dedecker]

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.

[Johan Commelin]

There is no hurry with adding things to that list

[Johan Commelin]

So let's wait for the infty version

[Patrick Massot]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

We finally have graphs!

[Johan Commelin]

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

[Kenny Lau]

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

[Scott Morrison]

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

[Johan Commelin]

@Simon Hudon You're a boss!

[Simon Hudon]

:bow:

[Simon Hudon]

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

[Kevin Buzzard]

That's a great showcase example Scott :-)

[Scott Morrison]

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

[Kenny Lau]

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

[Kenny Lau]

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

[Johan Commelin]

Thanks a lot @Kenny Lau

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

@Kenny Lau is it accessible?

[Scott Morrison]

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

[Reid Barton]

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

[Kevin Buzzard]

Is global sections a functor?

[Kevin Buzzard]

Spec being a functor doesn't sound hard

[Kenny Lau]

do we have morphisms yet?

[Kevin Buzzard]

In which category?

[Kevin Buzzard]

The category of locally ringed spaces I guess

[Adam Topaz]

Morphisms of schemes are there.

[Adam Topaz]

As a full subcat of locally ringed spaces

[Kevin Buzzard]

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

[Adam Topaz]

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

[Kevin Buzzard]

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

[Johan Commelin]

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

[Johan Commelin]

Uuh, maybe only on objects

[Johan Commelin]

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

[Adam Topaz]

Johan Commelin said:

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

Oh?

[Kevin Buzzard]

Oh I see!

[Kevin Buzzard]

Wait

[Kevin Buzzard]

I'm not sure i believe you

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

Huh, now I'm confused

[Johan Commelin]

How did we define Spec as LRS before this PR?

[Adam Topaz]

LRS should be RS

[Adam Topaz]

That's how it was done before.

[Johan Commelin]

Yup, you're right

[Kevin Buzzard]

Aah got it

[Johan Commelin]

I have no idea how hard Spec as functor will be

[Johan Commelin]

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

[Johan Commelin]

As in... another PR of 200 lines?

[Adam Topaz]

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

[Adam Topaz]

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

[Adam Topaz]

as ringed spaces, that is.

[Kenny Lau]

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

[Kenny Lau]

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

[Johan Commelin]

Galois theory is looming around the corner

[Johan Commelin]

Chapeau @Kenny Lau :clink:

[Scott Morrison]

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

[Johan Commelin]

@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
• ...?

[Kenny Lau]

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.

[Kevin Buzzard]

@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?

[Thomas Browning]

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.

[Kevin Buzzard]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

That was a good day for mathlib (-;

[Heather Macbeth]

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?

[Scott Morrison]

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

[Heather Macbeth]

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

[Heather Macbeth]

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

[Heather Macbeth]

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

[Scott Morrison]

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

[Heather Macbeth]

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

[Heather Macbeth]

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

[Heather Macbeth]

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

[Scott Morrison]

Oh! :-)

[Scott Morrison]

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.

[Scott Morrison]

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.

[Heather Macbeth]

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

[Frédéric Dupuis]

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?

[Heather Macbeth]

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.

[Frédéric Dupuis]

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

[Alexander Bentkamp]

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

[Frédéric Dupuis]

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!

[Scott Morrison]

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.

[Scott Morrison]

It's on the bell branch.

[Scott Morrison]

I'll PR soon.

[Frédéric Dupuis]

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?

[Scott Morrison]

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

[Scott Morrison]

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.

[Frédéric Dupuis]

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

[Frédéric Dupuis]

(Until today I guess!)

[Patrick Massot]

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

[Patrick Massot]

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

[Kevin Buzzard]

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

[Bryan Gin-ge Chen]

(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

[Kevin Buzzard]

How about sin(x)?

[Patrick Massot]

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

[Patrick Massot]

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.

[Rob Lewis]

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.

[Patrick Massot]

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

[Sebastien Gouezel]

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.

[Patrick Massot]

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

[Rob Lewis]

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

[Sebastien Gouezel]

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

[Gabriel Ebner]

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

[Rob Lewis]

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

[Rob Lewis]

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

[Kenny Lau]

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

[Patrick Massot]

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

[Kevin Buzzard]

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

[Sebastien Gouezel]

lemma continuous_sin : continuous sin

is missing a continuity attribute, indeed.

[Sebastien Gouezel]

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.

[Sebastien Gouezel]

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.

[Kevin Buzzard]

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

[Benjamin Davidson]

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.

[Yury G. Kudryashov]

#5647 drops some measurability assumptions in FTC-2

[Floris van Doorn]

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

[Yury G. Kudryashov]

Yes

[Heather Macbeth]

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

[Heather Macbeth]

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

[Floris van Doorn]

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

[Floris van Doorn]

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

[Heather Macbeth]

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

[Heather Macbeth]

Heather Macbeth said:

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

(or someone on Kevin's discord server?)

[Andrew Souther]

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

[Kevin Buzzard]

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

[James Arthur]

Heather Macbeth said:

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

working on it...

[Heather Macbeth]

@James Arthur Great! Looks like you are working on the fact that $\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 $\int_{-1}^12\sqrt{1-x^2}dx$)?

[Benjamin Davidson]

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

[Marc Masdeu]

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?

[Heather Macbeth]

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

[Benjamin Davidson]

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 $\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

[Johan Commelin]

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

[Benjamin Davidson]

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.

[Johan Commelin]

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

[Ruben Van de Velde]

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?

[Benjamin Davidson]

I believe @Floris van Doorn is working on it.

[Benjamin Davidson]

Let me link this discussion for reference.

[Benjamin Davidson]

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

[Yury G. Kudryashov]

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

[Johan Commelin]

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

[Patrick Massot]

Was this added to our mathlib overview?

[Ruben Van de Velde]

It was not

[Johan Commelin]

@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?

[Mario Carneiro]

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

[Kevin Buzzard]

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?

[Thomas Browning]

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.

[Thomas Browning]

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.

[Heather Macbeth]

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?

[Heather Macbeth]

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

[Thomas Browning]

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

[Thomas Browning]

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

[Heather Macbeth]

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.

[Heather Macbeth]

The transposition argument sounds unpleasant :)

[Kevin Buzzard]

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

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

(on a given interval of ereal)

[Yury G. Kudryashov]

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

[Johan Commelin]

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

[Mario Carneiro]

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

[Thomas Browning]

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

[Alex J. Best]

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

[Alex J. Best]

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

[Heather Macbeth]

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 $(-\infty, -\sqrt{2}/\sqrt[4]{5}]$ and $[-\sqrt{2}/\sqrt[4]{5}, \sqrt{2}/\sqrt[4]{5}]$ and $[\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.

[Heather Macbeth]

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

[Mario Carneiro]

evaluating $f(x):=x^5-4x+2$ at $\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(-\sqrt 2/\sqrt[4]5)\ge f(0)>0$ and monotonicity in the last interval to show $f(\sqrt 2/\sqrt[4]5)\le f(1)<0$

[Kevin Buzzard]

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.

[Kevin Buzzard]

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

[Yury G. Kudryashov]

Poincaré recurrence theorem #2311 is now merged to master

[Kevin Buzzard]

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 $C^\infty$ functions on quotients of Lie groups like $GL_n(\R)/GL_n(\Z)$ (or equivalently functions on $GL_n(\R)$ which are $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 $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!

[Heather Macbeth]

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

[Heather Macbeth]

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.

[Kevin Buzzard]

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

[Kevin Buzzard]

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 $H^n$ was actually $H^{n+1}$ :-) Luckily he had time to fix it!

[Scott Morrison]

Unit octonions form a Lie loop? :-)

[Bryan Gin-ge Chen]

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?

[Heather Macbeth]

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.

[David Michael Roberts]

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.

[Scott Morrison]

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.

[Bryan Gin-ge Chen]

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

[Bryan Gin-ge Chen]

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

[Scott Morrison]

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

[Scott Morrison]

I agree we should have some mechanism!

[Oliver Nash]

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!

[Nicolò Cavalleri]

Heather Macbeth said:

$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

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

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

[Bhavik Mehta]

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

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

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.

[Heather Macbeth]

@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?

[Heather Macbeth]

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

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

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

[Heather Macbeth]

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

[Bhavik Mehta]

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?

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

And I did the other proof in 1 morning.

[Yury G. Kudryashov]

And in less than 500 LOC including comments.

[Bhavik Mehta]

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

[Yury G. Kudryashov]

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

[David Wärn]

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

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

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.

[Gihan Marasingha]

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?

[Kevin Buzzard]

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

[Taylor Belcher]

Alex J. Best said:

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

I've got some first year undergrads and we are looking at trying to work on this. Do you know if anyone has picked it up?

[Johan Commelin]

I'm not aware of anyone. But maybe @Alex J. Best heard from someone. I don't think it has been discussed on Zulip at least.

[Bryan Gin-ge Chen]

(just dropping a link to Taylor's earlier thread on Descartes Rule of Signs)

[Taylor Belcher]

Thanks!

[Alex J. Best]

Yeah I haven't seen anyone take this up, so by all means go for it! I'm more than happy to discuss what I was trying to do there in that attempt if its helpful :smile:.

[Oliver Nash]

It recently became possible to _state_ the classification of semisimple Lie algebras in Mathlib.

For a MWE, create a new file and paste the following gross blob of setup at the top:

import algebra.lie.classical
import algebra.lie.cartan_matrix
import algebra.lie.semisimple
import algebra.lie.direct_sum
import field_theory.algebraic_closure
open lie_algebra
open_locale direct_sum
notation L₁ ` ≅ₗ⁅` K `⁆ `L₂ := nonempty (L₁ ≃ₗ⁅K⁆ L₂)
abbreviation sl (l : ℕ) (K : Type*) [field K] := special_linear.sl (fin l) K
abbreviation sp (l : ℕ) (K : Type*) [field K] := symplectic.sp (fin l) K
abbreviation so (l : ℕ) (K : Type*) [field K] := orthogonal.so (fin l) K

section delme -- Get rid of this section with fixes elsewhere, should not be necessary.

variables (ι R L : Type*) [comm_ring R] [lie_ring L] [lie_algebra R L] (I : ι → lie_ideal R L)

instance foo : lie_ring (⨁ i, I i) := @direct_sum.lie_ring ι (λ i, I i) _
instance bar : lie_algebra R (⨁ i, I i) := @direct_sum.lie_algebra R ι _ (λ i, I i) _ _

end delme

[Oliver Nash]

Then immediately below that the actual good stuff:

/-- Let `K` be an algebraically closed field of characteristic zero. -/
variables (K : Type*) [field K] [is_alg_closed K] [char_zero K]

/-- Let `L` be a finite-dimensional Lie algebra over `K`. -/
variables (L : Type*) [lie_ring L] [lie_algebra K L] [finite_dimensional K L]

theorem simple_classification :
  is_simple K L ↔
  ((L ≅ₗ⁅K⁆ g₂ K) ∨
   (L ≅ₗ⁅K⁆ f₄ K) ∨
   (L ≅ₗ⁅K⁆ e₆ K) ∨
   (L ≅ₗ⁅K⁆ e₇ K) ∨
   (L ≅ₗ⁅K⁆ e₈ K) ∨
   (∃ l, (L ≅ₗ⁅K⁆ sl l K) ∧ 1 < l) ∨
   (∃ l, (L ≅ₗ⁅K⁆ sp l K) ∧ 2 < l) ∨
   (∃ l, (L ≅ₗ⁅K⁆ so l K) ∧ 4 < l ∧ l ≠ 6)) := sorry

-- TODO (probably) state in terms of Lie-algebra version of `direct_sum.submodule_is_internal`.
theorem semisimple_classification :
  is_semisimple K L ↔
  ∃ n (I : fin n → lie_ideal K L), (L ≅ₗ⁅K⁆ (⨁ i, I i)) ∧ ∀ i, is_simple K (I i) := sorry

[Oliver Nash]

cf https://gist.github.com/ocfnash/f3e3ca8eb24689dc3cb7b48de70439e6

[Johan Commelin]

Awesome! A very nice milestone!

[Eric Wieser]

Huh, I didn't see docs#direct_sum.lie_ring slip in!

[Oliver Nash]

I think it might have been before your time!

[Adam Topaz]

Oof, my mobile zulip is angry with about 95% of the Unicode in this code block...

[Oliver Nash]

Adam Topaz said:

Oof, my mobile zulip is angry with about 95% of the Unicode in this code block...

image.png

[Johan Commelin]

And we aren't even using 𝔣𝔯𝔞𝔨𝔱𝔲𝔯 for the lie algebras!

[Adam Topaz]

Good question!

[Adam Topaz]

Does vscode allow you to write $\mathfrak{sl}$?

[Gabriel Ebner]

Paste it in a lean file and hover over it. Then vscode will tell you how to type it. If it can't, then you can add a setting (abbreviations I think it is called), and post a PR.

[Oliver Nash]

It looks like \Mfa in VS Code gives 𝔞, \Mfb gives 𝔟 etc.

[Johan Commelin]

Clearly we need abbreviations \sl, \so, \sp :smiley:

[Heather Macbeth]

It is very nice to be at a point where we need these abbreviations!

[Kevin Buzzard]

@Adam Topaz recently someone from Zulip got in touch with me and basically said "hi, we love that you love Zulip, do you have any comments about how we could work better for you?" and I told them that I loved them back but wished I could see Lean code on my Android phone, and they seem to be now actively discussing how to fix this.

[Eric Wieser]

When this came up in #Zulip meta we concluded it was an OS-wide problem on Android, right? I have the same problem with github in Android chrome.

[Kevin Buzzard]

Yes, but they seemed to be talking about shipping a font for the Zulip app which might fix the problem for that at least. I also have problems with github but for me this is less of an issue because I tend not to use github on my phone.

[Oliver Nash]

Isn’t Android the Wild West of mobile where you can ssh in to your phone and just install some fonts manually system-wide?

[Kevin Buzzard]

My current phone isn't rooted and I suspect that to root it I'd have to factory reset it, which I just can't be bothered to deal with.

[Oliver Nash]

Fair enough

[Adam Topaz]

Oliver Nash said:

Isn’t Android the Wild West of mobile where you can ssh in to your phone and just install some fonts manually system-wide?

If only things likke https://puri.sm/products/librem-5/ were useable...

[Adam Topaz]

Eric Wieser said:

When this came up in #Zulip meta we concluded it was an OS-wide problem on Android, right? I have the same problem with github in Android chrome.

The fonts work perfectly fine for me on firefox on android. In fact, if I copy Oliver's link to the gist, and open it in firefox, it works just fine.