## Stream: maths

### Topic: What's new in Lean maths?

#### Kevin Buzzard (Sep 09 2018 at 11:31):

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

#### Kevin Buzzard (Sep 09 2018 at 11:38):

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

#### Kevin Buzzard (Sep 09 2018 at 11:43):

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

#### Johannes Hölzl (Sep 09 2018 at 11:56):

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

#### Patrick Massot (Sep 09 2018 at 18:34):

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

#### Patrick Massot (Sep 09 2018 at 18:35):

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

#### Mario Carneiro (Sep 09 2018 at 21:17):

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

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


Since when did we have the near tactic?

#### Patrick Massot (Sep 09 2018 at 21:18):

I was about to try to find this

#### Patrick Massot (Sep 09 2018 at 21:18):

But I was never able to use it :(

#### Mario Carneiro (Sep 09 2018 at 21:19):

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

#### Johannes Hölzl (Sep 10 2018 at 01:54):

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

#### Mario Carneiro (Sep 10 2018 at 07:36):

Cross reference: abel tactic

#### Kevin Buzzard (Sep 10 2018 at 09:25):

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

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

#### Johan Commelin (Sep 21 2018 at 05:10):

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

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

#### Johan Commelin (Oct 02 2018 at 14:03):

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

#### Johan Commelin (Oct 02 2018 at 14:03):

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

#### Johan Commelin (Oct 02 2018 at 14:04):

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

#### Johan Commelin (Oct 02 2018 at 14:05):

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

#### Johan Commelin (Oct 02 2018 at 14:06):

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

#### Rob Lewis (Oct 02 2018 at 14:06):

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

#### Patrick Massot (Oct 02 2018 at 14:24):

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

#### Kevin Buzzard (Oct 08 2018 at 16:56):

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

#### Mario Carneiro (Oct 08 2018 at 16:58):

next stop characteristic polynomials?

#### Johan Commelin (Oct 08 2018 at 16:59):

Done in kbb

#### Kevin Buzzard (Oct 08 2018 at 17:01):

My birthday present just keeps on giving

#### Johan Commelin (Oct 08 2018 at 17:01):

You only turn 50 once...

#### Johan Commelin (Oct 15 2018 at 16:45):

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

#### Johan Commelin (Oct 15 2018 at 16:45):

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

#### Johan Commelin (Oct 15 2018 at 16:46):

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

#### Patrick Massot (Oct 15 2018 at 17:43):

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

#### Patrick Massot (Oct 15 2018 at 17:46):

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

#### Johannes Hölzl (Oct 17 2018 at 07:25):

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

#### Kenny Lau (Oct 17 2018 at 07:32):

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

fixed

thanks

#### Johannes Hölzl (Oct 18 2018 at 07:44):

each PID is a UFD is now in mathlib

#### Johan Commelin (Nov 05 2018 at 19:24):

Ok, who is up for a summary of today?

#### Johan Commelin (Nov 05 2018 at 19:24):

First of all: the module refactor landed!

#### Johan Commelin (Nov 05 2018 at 19:24):

Second: Perfect closure has been merged.

#### Kevin Buzzard (Nov 05 2018 at 19:25):

This is a green light for algebraic closure and Galois theory

#### Johan Commelin (Nov 05 2018 at 19:26):

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

#### Johan Commelin (Nov 05 2018 at 19:27):

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

#### Johan Commelin (Nov 05 2018 at 19:27):

We have Stone-Cech compactification.

#### Patrick Massot (Nov 19 2018 at 21:42):

Simon's monotonicity tactic has been merged in mathlib.

import tactic.monotonicity

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


#### Patrick Massot (Nov 19 2018 at 21:47):

We can combine with norm_num too:

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


#### Johan Commelin (Nov 20 2018 at 04:27):

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

#### Simon Hudon (Nov 20 2018 at 04:30):

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

#### Scott Morrison (Dec 02 2018 at 22:40):

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

#### Scott Morrison (Dec 02 2018 at 22:40):

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

#### Scott Morrison (Dec 02 2018 at 22:42):

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

#### Patrick Massot (Jan 05 2019 at 10:46):

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

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

#### Sebastien Gouezel (Jan 05 2019 at 10:59):

Thanks a lot Mario, this is awesome!

#### Johannes Hölzl (Jan 18 2019 at 15:24):

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

#### Johannes Hölzl (Jan 18 2019 at 15:25):

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

#### Simon Hudon (Jan 18 2019 at 20:17):

Can you use it in the category types?

#### Kevin Buzzard (Jan 18 2019 at 23:34):

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

#### Luca Gerolla (Jan 19 2019 at 10:42):

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

#### Johannes Hölzl (Jan 19 2019 at 16:48):

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

#### Johannes Hölzl (Jan 19 2019 at 16:49):

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

#### Simon Hudon (Jan 19 2019 at 18:25):

Doesn't that limit the applicability to writing programs?

#### Johannes Hölzl (Jan 20 2019 at 00:38):

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

#### Simon Hudon (Jan 20 2019 at 17:22):

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

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


#### Simon Hudon (Jan 20 2019 at 17:27):

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

#### Kevin Buzzard (Jan 20 2019 at 18:19):

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

The category of schemes has finite products. In short, if $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 (Jan 20 2019 at 23:13):

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

#### Johannes Hölzl (Jan 20 2019 at 23:16):

@Kevin Buzzard I want to construct the usual product of the shape measure A -> measure B -> measure (A x B). This would be the expected product from measure theory (assuming sigma finite measures). Here the Giry monad allows a factored proof.

(deleted)

#### Patrick Massot (Jan 22 2019 at 16:37):

Johannes and Sander defined the rank of a linear map!

#### Johannes Hölzl (Jan 23 2019 at 11:43):

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

#### Johannes Hölzl (Jan 23 2019 at 11:43):

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

#### Johannes Hölzl (Jan 23 2019 at 13:25):

seqeuence spaces (PR #440) is merged

#### Johannes Hölzl (Jan 24 2019 at 15:07):

Measures form a complete lattice now

#### Johannes Hölzl (Jan 28 2019 at 19:30):

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

#### Johannes Hölzl (Jan 29 2019 at 12:21):

@Chris Hughes splitting polynomials and clear_aux_decl are in mathlib now

#### Johan Commelin (Jan 29 2019 at 19:01):

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

#### Johannes Hölzl (Jan 29 2019 at 19:06):

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

#### Kevin Buzzard (Jan 29 2019 at 20:16):

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

#### Kevin Buzzard (Jan 29 2019 at 20:17):

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

#### Johannes Hölzl (Jan 30 2019 at 08:50):

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

Thanks!

#### Kevin Buzzard (Jan 30 2019 at 12:14):

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

#### Johannes Hölzl (Feb 06 2019 at 10:13):

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

#### Johan Commelin (Feb 06 2019 at 12:09):

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

Thanks! :D

#### Johannes Hölzl (Feb 07 2019 at 12:34):

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

#### Kevin Buzzard (Feb 07 2019 at 13:40):

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

#### Sebastien Gouezel (Feb 07 2019 at 13:59):

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

#### Kenny Lau (Feb 16 2019 at 21:28):

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

#### Kevin Buzzard (Feb 16 2019 at 21:43):

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

#### Kevin Buzzard (Feb 16 2019 at 21:43):

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

#### Rob Lewis (Mar 01 2019 at 15:51):

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

#### Patrick Massot (Mar 29 2019 at 20:22):

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

#### Johan Commelin (Mar 29 2019 at 20:29):

@Abhimanyu Pallavi Sudhir defined the hyperreals

#### Johan Commelin (Apr 08 2019 at 07:27):

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

#### Johan Commelin (Apr 08 2019 at 11:31):

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

#### Kevin Buzzard (Apr 08 2019 at 11:46):

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

#### Johan Commelin (Apr 08 2019 at 11:48):

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

#### Ramon Fernandez Mir (Apr 10 2019 at 19:54):

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

The main novelties are:

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

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

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

#### Kevin Buzzard (Apr 10 2019 at 19:55):

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

#### Scott Morrison (Apr 10 2019 at 21:41):

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

This includes the definition of scheme, right?

#### Scott Morrison (Apr 10 2019 at 21:45):

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

#### Scott Morrison (Apr 10 2019 at 21:45):

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

#### Scott Morrison (Apr 11 2019 at 02:34):

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

#### Scott Morrison (Apr 11 2019 at 02:34):

Hopefully it is not actually that much work.

#### Mario Carneiro (Apr 11 2019 at 02:46):

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

#### Johan Commelin (Apr 17 2019 at 09:12):

We now have omega! Kudos to @Seul Baek!

#### Moses Schönfinkel (Apr 17 2019 at 10:27):

This should also be in #general! :)

Thanks! :)

#### Patrick Massot (Jul 04 2019 at 11:38):

Some catching up for this thread:

Don't hesitate to add things I missed!

#### Johan Commelin (Sep 28 2019 at 02:46):

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

#### Johan Commelin (Sep 28 2019 at 02:47):

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

#### Patrick Massot (Sep 28 2019 at 07:44):

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

#### Kevin Buzzard (Sep 28 2019 at 12:48):

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

#### Patrick Massot (Jul 10 2020 at 08:27):

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

#### Patrick Massot (Aug 11 2020 at 08:22):

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

#### Kevin Buzzard (Aug 11 2020 at 08:29):

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

#### Scott Morrison (Aug 11 2020 at 10:02):

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

#### Patrick Massot (Aug 11 2020 at 10:07):

Kevin probably meant he wants Fourier transform.

#### Patrick Massot (Aug 11 2020 at 10:08):

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

#### Scott Morrison (Aug 11 2020 at 10:09):

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

#### Scott Morrison (Aug 11 2020 at 10:10):

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

#### Patrick Massot (Aug 11 2020 at 10:12):

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

#### Kevin Buzzard (Aug 11 2020 at 13:17):

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

#### Kenny Lau (Aug 12 2020 at 18:35):

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 (Aug 12 2020 at 19:09):

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

#### Floris van Doorn (Aug 13 2020 at 01:35):

Patrick Massot said:

How far are we from having Fubini's theorem? With FTC+Fubini we could say that we have integration in mathlib (maybe we would need completeness of $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 (Aug 13 2020 at 01:35):

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

#### Kenny Lau (Aug 13 2020 at 07:16):

Kevin Buzzard said:

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

that's is_alg_closed right; and inhabited implies nonempty?

#### Patrick Massot (Aug 13 2020 at 21:28):

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

#### Kevin Buzzard (Aug 13 2020 at 23:02):

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

#### Adam Topaz (Aug 13 2020 at 23:04):

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

#### Adam Topaz (Aug 13 2020 at 23:05):

And sounds like isabelle doesn't have it :)

#### Aaron Anderson (Aug 13 2020 at 23:21):

You mean to construct the real closure?

#### Aaron Anderson (Aug 13 2020 at 23:22):

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

#### Adam Topaz (Aug 13 2020 at 23:30):

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

#### Adam Topaz (Aug 13 2020 at 23:30):

Artin-Schreier would be great!

#### Gabriel Ebner (Aug 14 2020 at 08:30):

@Chris Hughes That looks like a password.

#### Gabriel Ebner (Aug 14 2020 at 08:31):

@Rob Lewis Can you delete Chris' post?

#### Johan Commelin (Aug 14 2020 at 09:39):

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

#### Johan Commelin (Aug 14 2020 at 09:39):

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

#### Kevin Buzzard (Aug 14 2020 at 09:40):

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

#### Kevin Buzzard (Aug 14 2020 at 09:41):

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

#### Kevin Buzzard (Aug 14 2020 at 09:42):

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

#### Johan Commelin (Aug 14 2020 at 09:52):

Thanks, I hope transcendental will be PR'd?

#### Johan Commelin (Aug 14 2020 at 09:53):

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

#### Kevin Buzzard (Aug 14 2020 at 09:57):

Oh I just meant the PR queue :-)

#### Kevin Buzzard (Aug 14 2020 at 09:58):

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

#### Kevin Buzzard (Aug 14 2020 at 09:59):

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

#### Yury G. Kudryashov (Aug 14 2020 at 16:21):

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

#### Johan Commelin (Aug 14 2020 at 16:25):

Yes, please. That would be great.

#### Rob Lewis (Aug 15 2020 at 13:39):

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

#### Patrick Massot (Aug 15 2020 at 16:34):

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

#### Yury G. Kudryashov (Aug 16 2020 at 21:52):

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

#### Yury G. Kudryashov (Aug 16 2020 at 21:53):

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

#### Kenny Lau (Aug 19 2020 at 06:31):

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

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 (Aug 19 2020 at 12:47):

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

#### Anatole Dedecker (Aug 19 2020 at 13:15):

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

#### Johan Commelin (Aug 19 2020 at 13:16):

There is no hurry with adding things to that list

#### Johan Commelin (Aug 19 2020 at 13:17):

So let's wait for the infty version

#### Patrick Massot (Aug 19 2020 at 20:28):

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

#### Mario Carneiro (Aug 19 2020 at 20:41):

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

#### Mario Carneiro (Aug 19 2020 at 20:42):

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

#### Johan Commelin (Aug 20 2020 at 02:57):

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

#### Johan Commelin (Aug 25 2020 at 03:47):

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>

#### Johan Commelin (Aug 25 2020 at 03:47):

We finally have graphs!

#### Johan Commelin (Aug 25 2020 at 03:48):

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

#### Kenny Lau (Aug 31 2020 at 06:45):

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 (Sep 01 2020 at 22:46):

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

import tactic.slim_check
import data.nat.prime

open nat

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


#### Johan Commelin (Sep 02 2020 at 03:36):

@Simon Hudon You're a boss!

:bow:

#### Simon Hudon (Sep 02 2020 at 03:42):

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

#### Kevin Buzzard (Sep 02 2020 at 06:27):

That's a great showcase example Scott :-)

#### Scott Morrison (Sep 02 2020 at 06:57):

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

#### Kenny Lau (Sep 07 2020 at 11:47):

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 (Sep 07 2020 at 11:48):

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

#### Johan Commelin (Sep 07 2020 at 11:57):

Thanks a lot @Kenny Lau

#### Kevin Buzzard (Sep 07 2020 at 12:15):

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

#### Kevin Buzzard (Sep 07 2020 at 12:15):

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

#### Kevin Buzzard (Sep 07 2020 at 12:15):

@Kenny Lau is it accessible?

#### Scott Morrison (Sep 07 2020 at 12:49):

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

#### Reid Barton (Sep 07 2020 at 13:08):

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

#### Kevin Buzzard (Sep 07 2020 at 13:31):

Is global sections a functor?

#### Kevin Buzzard (Sep 07 2020 at 13:31):

Spec being a functor doesn't sound hard

#### Kenny Lau (Sep 07 2020 at 13:31):

do we have morphisms yet?

#### Kevin Buzzard (Sep 07 2020 at 13:31):

In which category?

#### Kevin Buzzard (Sep 07 2020 at 13:32):

The category of locally ringed spaces I guess

#### Adam Topaz (Sep 07 2020 at 13:32):

Morphisms of schemes are there.

#### Adam Topaz (Sep 07 2020 at 13:32):

As a full subcat of locally ringed spaces

#### Kevin Buzzard (Sep 07 2020 at 13:33):

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

#### Adam Topaz (Sep 07 2020 at 13:33):

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

#### Kevin Buzzard (Sep 07 2020 at 13:33):

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

#### Johan Commelin (Sep 07 2020 at 13:34):

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

#### Johan Commelin (Sep 07 2020 at 13:34):

Uuh, maybe only on objects

#### Johan Commelin (Sep 07 2020 at 13:34):

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

#### Adam Topaz (Sep 07 2020 at 13:35):

Johan Commelin said:

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

Oh?

Oh I see!

Wait

#### Kevin Buzzard (Sep 07 2020 at 13:35):

I'm not sure i believe you

#### Johan Commelin (Sep 07 2020 at 13:35):

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

#### Johan Commelin (Sep 07 2020 at 13:36):

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

#### Johan Commelin (Sep 07 2020 at 13:36):

Huh, now I'm confused

#### Johan Commelin (Sep 07 2020 at 13:36):

How did we define Spec as LRS before this PR?

LRS should be RS

#### Adam Topaz (Sep 07 2020 at 13:37):

That's how it was done before.

#### Johan Commelin (Sep 07 2020 at 13:38):

Yup, you're right

Aah got it

#### Johan Commelin (Sep 07 2020 at 13:45):

I have no idea how hard Spec as functor will be

#### Johan Commelin (Sep 07 2020 at 13:45):

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

#### Johan Commelin (Sep 07 2020 at 13:45):

As in... another PR of 200 lines?

#### Adam Topaz (Sep 07 2020 at 13:50):

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

#### Adam Topaz (Sep 07 2020 at 13:51):

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 (Sep 07 2020 at 13:51):

as ringed spaces, that is.

#### Kenny Lau (Sep 13 2020 at 10:48):

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 (Sep 14 2020 at 09:48):

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 (Sep 14 2020 at 09:51):

Galois theory is looming around the corner

#### Scott Morrison (Sep 14 2020 at 09:55):

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

#### Johan Commelin (Sep 14 2020 at 09:57):

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

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

#### Kenny Lau (Sep 14 2020 at 10:14):

Tentative plan:

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

#### Kevin Buzzard (Sep 14 2020 at 10:17):

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

#### Thomas Browning (Sep 14 2020 at 17:24):

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

#### Kevin Buzzard (Sep 14 2020 at 17:28):

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

#### Johan Commelin (Sep 27 2020 at 03:27):

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 (Sep 27 2020 at 03:28):

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 (Sep 27 2020 at 03:28):

feat(analysis/convex/integral): Jensen's inequality for integrals (#4…
feat(analysis/convex/integral): Jensen's inequality for integrals (#4225)

#### Johan Commelin (Sep 27 2020 at 03:28):

That was a good day for mathlib (-;

#### Heather Macbeth (Oct 01 2020 at 23:10):

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 (Oct 01 2020 at 23:54):

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

#### Heather Macbeth (Oct 01 2020 at 23:54):

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

#### Heather Macbeth (Oct 01 2020 at 23:55):

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

#### Heather Macbeth (Oct 01 2020 at 23:55):

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

#### Scott Morrison (Oct 01 2020 at 23:56):

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

#### Heather Macbeth (Oct 01 2020 at 23:58):

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

#### Heather Macbeth (Oct 01 2020 at 23:59):

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

#### Heather Macbeth (Oct 02 2020 at 00:04):

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

Oh! :-)

#### Scott Morrison (Oct 02 2020 at 00:05):

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

#### Scott Morrison (Oct 02 2020 at 00:06):

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

#### Heather Macbeth (Oct 02 2020 at 00:10):

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

#### Frédéric Dupuis (Oct 02 2020 at 00:53):

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

#### Heather Macbeth (Oct 02 2020 at 00:58):

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

#### Frédéric Dupuis (Oct 02 2020 at 01:00):

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

#### Alexander Bentkamp (Oct 02 2020 at 07:24):

@Frédéric Dupuis said:

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

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

#### Frédéric Dupuis (Oct 02 2020 at 13:39):

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

#### Scott Morrison (Oct 03 2020 at 00:31):

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

#### Scott Morrison (Oct 03 2020 at 00:31):

It's on the bell branch.

I'll PR soon.

#### Frédéric Dupuis (Oct 03 2020 at 01:22):

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

#### Scott Morrison (Oct 03 2020 at 01:29):

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

#### Scott Morrison (Oct 03 2020 at 01:30):

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

#### Frédéric Dupuis (Oct 03 2020 at 01:44):

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

#### Frédéric Dupuis (Oct 03 2020 at 01:45):

(Until today I guess!)

#### Patrick Massot (Jan 04 2021 at 08:39):

Since #4945, we have:

import measure_theory.interval_integral

open interval_integral

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


#### Patrick Massot (Jan 04 2021 at 08:40):

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

#### Kevin Buzzard (Jan 04 2021 at 09:03):

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

#### Bryan Gin-ge Chen (Jan 04 2021 at 09:14):

(Almost) the same proof works:

import measure_theory.interval_integral

open interval_integral

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


#### Patrick Massot (Jan 04 2021 at 10:24):

import measure_theory.interval_integral
import analysis.special_functions.trigonometric

open interval_integral real
open_locale real

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


#### Patrick Massot (Jan 04 2021 at 10:26):

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

#### Rob Lewis (Jan 04 2021 at 10:34):

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

#### Patrick Massot (Jan 04 2021 at 10:36):

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

#### Sebastien Gouezel (Jan 04 2021 at 10:42):

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

#### Patrick Massot (Jan 04 2021 at 10:43):

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

#### Rob Lewis (Jan 04 2021 at 10:48):

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

#### Sebastien Gouezel (Jan 04 2021 at 10:51):

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

#### Gabriel Ebner (Jan 04 2021 at 10:56):

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

import measure_theory.interval_integral
import analysis.special_functions.trigonometric

open interval_integral real set
open_locale real

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

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


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

#### Rob Lewis (Jan 04 2021 at 10:58):

simp doesn't do norm_num but norm_num does simp!

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


#### Rob Lewis (Jan 04 2021 at 10:59):

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

#### Kenny Lau (Jan 04 2021 at 11:00):

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

#### Patrick Massot (Jan 04 2021 at 11:00):

Gabriel Ebner said:

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

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

#### Kevin Buzzard (Jan 04 2021 at 11:02):

Kenny Lau said:

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

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

#### Sebastien Gouezel (Jan 04 2021 at 11:04):

lemma continuous_sin : continuous sin


is missing a continuity attribute, indeed.

#### Sebastien Gouezel (Jan 04 2021 at 11:08):

I wonder why

attribute [continuity] continuous_sin

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


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

#### Sebastien Gouezel (Jan 04 2021 at 11:14):

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

attribute [continuity] continuous_sin

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


works fine.

#### Kevin Buzzard (Jan 04 2021 at 11:37):

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

#### Benjamin Davidson (Jan 07 2021 at 06:49):

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

#### Yury G. Kudryashov (Jan 07 2021 at 07:57):

#5647 drops some measurability assumptions in FTC-2

#### Floris van Doorn (Jan 07 2021 at 08:01):

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

Yes

#### Heather Macbeth (Jan 08 2021 at 06:18):

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

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

#### Heather Macbeth (Jan 08 2021 at 06:20):

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

#### Floris van Doorn (Jan 08 2021 at 06:20):

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

#### Floris van Doorn (Jan 08 2021 at 06:21):

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

#### Heather Macbeth (Jan 08 2021 at 06:26):

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 (Jan 08 2021 at 06:31):

Heather Macbeth said:

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

(or someone on Kevin's discord server?)

#### Andrew Souther (Jan 08 2021 at 06:34):

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

#### Kevin Buzzard (Jan 08 2021 at 10:31):

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

#### James Arthur (Jan 08 2021 at 10:47):

Heather Macbeth said:

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

working on it...

#### Heather Macbeth (Jan 09 2021 at 00:15):

@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 (Jan 09 2021 at 22:36):

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

#### Marc Masdeu (Jan 13 2021 at 15:29):

Benjamin Davidson said:

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

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

#### Heather Macbeth (Jan 13 2021 at 15:34):

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

#### Benjamin Davidson (Feb 23 2021 at 07:50):

Heather Macbeth said:

With #5300, we have the derivative of arcsin. Therefore by #4945 we have the integral of sqrt (1 - x ^ 2) (which is $\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 (Feb 23 2021 at 07:53):

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

#### Benjamin Davidson (Feb 23 2021 at 07:56):

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

#### Johan Commelin (Feb 23 2021 at 08:01):

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

#### Ruben Van de Velde (Feb 23 2021 at 08:26):

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

#### Benjamin Davidson (Feb 23 2021 at 08:54):

I believe @Floris van Doorn is working on it.

#### Benjamin Davidson (Feb 23 2021 at 08:55):

Let me link this discussion for reference.

#### Benjamin Davidson (Mar 02 2021 at 04:26):

Pertaining to the earlier discussion in this topic about integration...

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 (Mar 09 2021 at 18:19):

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

#### Johan Commelin (Mar 19 2021 at 10:30):

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

It was not

#### Johan Commelin (Mar 19 2021 at 10:42):

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

#### Mario Carneiro (Mar 19 2021 at 21:31):

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

#### Kevin Buzzard (Mar 19 2021 at 21:32):

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

#### Thomas Browning (Mar 19 2021 at 23:20):

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

#### Thomas Browning (Mar 19 2021 at 23:22):

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

#### Heather Macbeth (Mar 19 2021 at 23:27):

Thomas Browning said:

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

This is an intermediate value theorem argument, right?

#### Heather Macbeth (Mar 19 2021 at 23:27):

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

#### Thomas Browning (Mar 19 2021 at 23:36):

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

#### Thomas Browning (Mar 19 2021 at 23:38):

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

#### Heather Macbeth (Mar 19 2021 at 23:51):

Thomas Browning said:

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

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

#### Heather Macbeth (Mar 19 2021 at 23:53):

The transposition argument sounds unpleasant :)

#### Kevin Buzzard (Mar 20 2021 at 00:53):

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

#### Yury G. Kudryashov (Mar 20 2021 at 01:55):

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

#### Yury G. Kudryashov (Mar 20 2021 at 01:56):

(on a given interval of ereal)

#### Yury G. Kudryashov (Mar 20 2021 at 01:59):

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

#### Johan Commelin (Mar 20 2021 at 04:13):

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

#### Mario Carneiro (Mar 20 2021 at 04:19):

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

#### Thomas Browning (Mar 20 2021 at 04:20):

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

#### Alex J. Best (Mar 20 2021 at 04:48):

Johan Commelin said:

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

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

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

namespace polynomial
/-- pairs up consecutive elements of a list applies f and returns a list of length one less -/
def map_adjacent {α β : Type*} (f : α → α → β) (l : list α) : list β :=
l.zip_with f l.tail
#eval map_adjacent (+) [1, 2, 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
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,
congr' 3,
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),
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 (Mar 20 2021 at 04:52):

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

#### Heather Macbeth (Mar 20 2021 at 04:52):

Mario Carneiro said:

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

To rephrase this slightly: consider the three intervals $(-\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 (Mar 20 2021 at 04:53):

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

#### Mario Carneiro (Mar 20 2021 at 11:39):

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 (Mar 20 2021 at 12:33):

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

#### Kevin Buzzard (Mar 20 2021 at 12:34):

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

#### Yury G. Kudryashov (Mar 26 2021 at 22:40):

Poincaré recurrence theorem #2311 is now merged to master

#### Kevin Buzzard (Mar 28 2021 at 21:12):

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

Another lofty goal I always have at the back of my mind is the theory of automorphic forms and automorphic representations. The pre-adelic definition of these things involves $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 (Mar 28 2021 at 21:25):

$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 (Mar 28 2021 at 23:04):

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

#### Kevin Buzzard (Mar 28 2021 at 23:09):

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

#### Kevin Buzzard (Mar 28 2021 at 23:10):

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

#### Scott Morrison (Mar 28 2021 at 23:11):

Unit octonions form a Lie loop? :-)

#### Bryan Gin-ge Chen (Mar 28 2021 at 23:11):

Kevin Buzzard said:

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

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

#### Heather Macbeth (Mar 28 2021 at 23:24):

Bryan Gin-ge Chen said:

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

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

#### David Michael Roberts (Mar 29 2021 at 00:01):

Scott Morrison said:

Unit octonions form a Lie loop? :-)

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

#### Scott Morrison (Mar 29 2021 at 00:26):

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

#### Bryan Gin-ge Chen (Mar 29 2021 at 00:27):

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

#### Bryan Gin-ge Chen (Mar 29 2021 at 00:32):

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

#### Scott Morrison (Mar 29 2021 at 00:46):

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

#### Scott Morrison (Mar 29 2021 at 00:46):

I agree we should have some mechanism!

#### Oliver Nash (Mar 29 2021 at 10:00):

Kevin Buzzard said:

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

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

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

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

#### Nicolò Cavalleri (Mar 30 2021 at 12:06):

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 (Mar 30 2021 at 21:03):

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

#### Yury G. Kudryashov (Mar 30 2021 at 21:03):

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

#### Yury G. Kudryashov (Mar 30 2021 at 21:04):

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

#### Bhavik Mehta (Mar 30 2021 at 21:08):

Yury G. Kudryashov said:

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

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

#### Yury G. Kudryashov (Mar 30 2021 at 21:11):

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

#### Yury G. Kudryashov (Mar 30 2021 at 21:16):

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

#### Heather Macbeth (Mar 30 2021 at 21:16):

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

#### Heather Macbeth (Mar 30 2021 at 21:17):

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

#### Yury G. Kudryashov (Mar 30 2021 at 21:17):

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

#### Yury G. Kudryashov (Mar 30 2021 at 21:19):

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

#### Heather Macbeth (Mar 30 2021 at 21:21):

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

#### Bhavik Mehta (Mar 30 2021 at 21:22):

Yury G. Kudryashov said:

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

Right - does this not work?

#### Yury G. Kudryashov (Mar 30 2021 at 21:22):

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

#### Yury G. Kudryashov (Mar 30 2021 at 21:23):

And I did the other proof in 1 morning.

#### Yury G. Kudryashov (Mar 30 2021 at 21:23):

And in less than 500 LOC including comments.

#### Bhavik Mehta (Mar 30 2021 at 21:24):

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

#### Yury G. Kudryashov (Mar 30 2021 at 21:25):

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

#### David Wärn (Mar 30 2021 at 21:37):

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

#### Yury G. Kudryashov (Mar 30 2021 at 22:00):

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

#### Yury G. Kudryashov (Mar 31 2021 at 19:07):

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

#### Gihan Marasingha (May 07 2021 at 18:25):

Kevin Buzzard said:

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

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

#### Kevin Buzzard (May 07 2021 at 19:22):

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

Last updated: May 09 2021 at 09:11 UTC