Conditionally complete lattice

Stream: Is there code for X?

[Yaël Dillies]

Do we not yet have the conditionally_complete_lattice ℕ instance?

[Yaël Dillies]

In general, I am pretty bothered by the lack of API for conditionally complete orders, so maybe this is my next order project. Thanks a lot Yury for all your work on this!

[Yaël Dillies]

Do we also not have conditionally_complete_(monoid, group, semiring, ring, field)?

[Yaël Dillies]

Wait, we don't have complete_(monoid, group, semiring, ring, field) either? :sad:

[Yaël Dillies]

Is there any way to make that work with mixins?

[Johan Commelin]

@Yaël Dillies What is a complete monoid?

[Yaël Dillies]

A complete lattice with a compatible monoid structure

[Yaël Dillies]

This one is probably useless. But complete_field is definitely useful to abstract ℝ.

[Yaël Dillies]

I actually believe this is precisely what we need in measure theory.

[Yaël Dillies]

Supposedly, normed_space too coudl use such an abstraction.

[Sebastien Gouezel]

docs#nat.conditionally_complete_linear_order_bot

[Sebastien Gouezel]

Not sure what you want to abstract away in measure theory, can you elaborate?

[Yaël Dillies]

Measures are currently real-valued, right?

[Sebastien Gouezel]

They are ennreal-valued.

[Yaël Dillies]

I don't personally care much about measure theory yet. This was really a side remark. I would much more appreciate non real normed spaces.

[Yaël Dillies]

Ah sorry. This is still concrete structure-centric, though.

[Sebastien Gouezel]

Yes, definitely concrete. Otherwise, you would have to add yet another parameter to the definition of measures, the target type, and this would make the whole theory more complicated for absolutely no gain.

[Sebastien Gouezel]

In the same way that we use nat all the time, and not a generic nat-like type.

[Kevin Buzzard]

Yaël Dillies said:

This one is probably useless. But complete_field is definitely useful to abstract ℝ.

The reals are not complete in the sense of lattices.

[Alex J. Best]

In #3292 I added conditionally complete linear ordered fields, I've always wondered if you switched some results about R to take this type class what generalizations would be possible. I think that PR is basically done, it just needs splitting up

[Yaël Dillies]

Oh wait, all conditionally_complete_linear_ordered_fields are isomorphic to ℝ?

[Eric Wieser]

Sebastien Gouezel said:

Yes, definitely concrete. Otherwise, you would have to add yet another parameter to the definition of measures, the target type, and this would make the whole theory more complicated for absolutely no gain.

docs#measure_theory.vector_measure is sort of doing this, right? Except that it's 0 outside the measurable sets instead of the outer extension thing.

[Reid Barton]

But there is more than one topological additive monoid in existence, as demonstrated by the following two abbreviations

[Kevin Buzzard]

@Alex J. Best What is the status of #3292 ? Is it true that it just needs documentation (this is what the tag seems to indicate)? I ask because I am currently sitting in a room with not one but two people who have formalised the Eudoxus reals in Lean (independently!) and proved that they're complete, so maybe they're only #3292 away from showing that they're the Lean reals.

[Alex J. Best]

It just needs splitting up really

[Alex J. Best]

Probably a bit of documentation yes

[Alex J. Best]

But the stuff about ordered ring isomorphisms and homs belongs in a separate pr, I started at one point but got waylaid when I tried to prove some random general results about them. The branch probably needs a refresh too and merge to master but it's basically good to go if someone puts a little time into it

[Yaël Dillies]

Please people stop speaking about someone putting time into ordered stuff. That's the safest way to get me involved

[Yaël Dillies]

If you give me your approval, I can merge master and bump, and maybe split up properly.

[Patrick Massot]

Why do all those young people get passionate about Eudoxus reals? We also have @yannis monbru here.

[yannis monbru]

maybe we are traumatized by tales about axiom of choice

[Johan Commelin]

But then, how did that happen? Back when I was a student, we celebrated choice.