measure theory

Stream: general

[Mario Carneiro]

Hey, this is just an ad for the rather large commit I just put out. It doesn't add too much new stuff, instead it is doing what I do best, proving the same things other people did but better. :) It's focused primarily on the measure theory development, with the hope that I can bring down some of the compile times in that area. But there are some more substantive changes:

• outer_measure.trim is the truncation of an outer measure to a measurable space
• measure_space was renamed to measure. There is a good sense of what a measure space could be, and this wasn't it.
• measure and outer_measure now have coe_fn instances so you don't need to refer to the underlying measure_of function.
• measure extends outer_measure, so in particular it contains a field that is the outer measure projection, rather than containing a function only defined on measurable sets and recovering the outer measure by extension. In order to ensure we don't add extra measures, we require that a measure is trimmed in the sense above.
• is_complete asserts that a measure is complete (every null set is measurable)
• is_null_measurable is the property of differing from a measurable set by a null set. It is proven that this is a sigma algebra, and a measure extends unchanged to this larger algebra; this is the completion of the measure.
• lebesgue has mostly the same theorems but the proofs are rather different. In particular the proof that intervals are measured correctly uses compactness instead of the least upper bound property.
• Some more interval theorems were added; Icc is the closed interval

[Kevin Buzzard]

Mario do you know about Haar measure? There's a canonical measure on any locally compact Hausdorff topological group (for example the real numbers).

[Kevin Buzzard]

The proof is "do the same as for the real numbers, but with an arbitrary locally compact Hausdorff topological group".

[Kevin Buzzard]

although some details are a lot more fiddly if I'm honest...

[Mario Carneiro]

I have heard of it, but I've never done anything with it besides getting uncomfortable about "unique up to a multiplicative constant"

[Patrick Massot]

Lebesgue is also only determined up to a multiplicative constant on a finite dimensional real vector space

[Kevin Buzzard]

Well, who said [0,1] should have measure 1...

[Mario Carneiro]

Oh, I forgot to mention I added scalar multiplication of measures; they are unfortunately not a module since the base "ring" is ennreal

[Patrick Massot]

If you talk about [0,1] then you've already chosen a basis of your 1-dimensional vector space

[Kevin Buzzard]

yes, my comment was supposed to be before yours :-)

[Patrick Massot]

Too bad we miss an opportunity to enjoy module type class hell

[Kevin Buzzard]

If CS people are happy to divide by 0, why can't they multiply by infinity?

[Kevin Buzzard]

Just make it 0 :-)

[Mario Carneiro]

actually ennreal is surprisingly nice as an ordered semiring

[Mario Carneiro]

the fact that it is a complete lattice really helps

[Patrick Massot]

That's the trouble: if I understand correctly Mario is happy to multiply by infinity

[Mario Carneiro]

a basis of your 1-dimensional vector space

It's not a vector space

[Patrick Massot]

affine space I should say

[Mario Carneiro]

is there a notion of semi-vector space in the literature?

[Mario Carneiro]

there are no negatives

[Kevin Buzzard]

I am amazed that this is not already in Lean

[Patrick Massot]

You know we already don't want to talk about semirings

[Kevin Buzzard]

I guess a monoid is just a semi-module over N

[Mario Carneiro]

I find of am as well. We have semi everything else, but modules pick right up at rings

[Kevin Buzzard]

actually maybe that's a commutative monoid

[Mario Carneiro]

A nat-semi-module is a commutative monoid

[Mario Carneiro]

but if the scalar field is something else then it's different

[Patrick Massot]

I'm curious about all this integration stuff in mathlib. I never tried to use it or even looked at it. Can we do crazy things like proving the integral of id on [1, 2] is 3/2?

[Sean Leather]

Hey, this is just an ad for the rather large commit I just put out. It doesn't add too much new stuff, instead it is doing what I do best, proving the same things other people did but better. :smiley:

Thanks for that, @Mario Carneiro!

[Mario Carneiro]

you were the one who mentioned the issue with meaure'_union, right? I may have gone a bit overboard. :)

[Sean Leather]

you were the one who mentioned the issue with meaure'_union, right?

Indeed, I was.

I may have gone a bit overboard. :smiley:

No problem! As long as you think it improved things.

[Kevin Buzzard]

Actually I have a problem too -- Fermat's Last Theorem can't currently be proved by finish -- can you fix it for me Mario?

[Johan Commelin]

Kevin, the proof is by ᛗᛃᛟᛚᚾᛁᚱ

[Sean Leather]

This is the Mario variation of the ᛗᛃᛟᛚᚾᛁᚱ tactic.

[Johan Commelin]

Speaking of hammers... I would like the decomposition theorem for mixed Hodge modules.

[Kevin Buzzard]

Yeah well I would like perfectoid spaces but I spent an hour last night writing the universal property of quotient groups :-/

[Kenny Lau]

should have told me to write it lol

[Kevin Buzzard]

Can you do algebraically closed fields Kenny? Chris' polynomials in one variable got accepted

[Kevin Buzzard]

Things are happening :-)

[Kenny Lau]

have you proved that k[X] is UFD?

[Kevin Buzzard]

https://github.com/kbuzzard/lean-perfectoid-spaces/blob/master/src/for_mathlib/quotient_group.lean

[Kevin Buzzard]

Do we even have a definition of UFD? It's pretty ugly

[Kenny Lau]

also I think we need "a in L/K: a is integral over K iff K(a) is finite"

[Kenny Lau]

Do we even have a definition of UFD? It's pretty ugly

A is UFD iff (A\{0})/A* is a free monoid :)

[Kevin Buzzard]

Blair is doing fdvs. Why not ask her if you can help?

[Kevin Buzzard]

We need more UG maths!

[Johan Commelin]

So we need more UG's, so that we can prove things by UG. You do have access to two hammers!

[Kenny Lau]

let's say we've built L such that every polynomial in K[X] splits over L. How then do you show that L contains an algebraically closed field?

[Kenny Lau]

I think we should prove that K[X] is ED, that might help

[Johan Commelin]

That was almost there, right?

[Kenny Lau]

how should we prove "L is algebraically closed iff every finite extension of L is L"? that would involve building splitting fields

[Johan Commelin]

Except that the definition of ED wasn't optimal, so Chris had to work with degree + 1, or change the definition

[Johan Commelin]

I guess you want to do separable closure at the same time

[Kenny Lau]

my point is, there's a long way to go before we build algebraic closure

[Johannes Hölzl]

@Patrick Massot there is no integral in mathlibs measure theory, yet.

[Johannes Hölzl]

Oh, I forgot to mention I added scalar multiplication of measures; they are unfortunately not a module since the base "ring" is ennreal

Yeah, semimodules would be nice to have. But up to now I didn't find any literature on them.

[Patrick Massot]

Oh, I didn't even imagine that. I was concerned about the fact that we don't have derivative and that could be a problem when wanting to compute integrals.

[Johannes Hölzl]

Well, the basic theory of integrals in measure theory doesn't need derivatives. It starts with integration over the Lebesgue measure. But there is some theory to be developed up to this point.

[Patrick Massot]

Sure, that's why I though we could have integrals but no mean of computing one

[Patrick Massot]

But let's have normed spaces first :wink:

[Kevin Buzzard]

Oh, I forgot to mention I added scalar multiplication of measures; they are unfortunately not a module since the base "ring" is ennreal

Yeah, semimodules would be nice to have. But up to now I didn't find any literature on them.

Maybe that's because most mathematicians think they're about as useless as distribs? Having said that, the existence of distribs proves that computer scientists have very different opinions to mathematicians as to what is "nice to have". What would mathlib want semimodules for? Is this something to do with compile times or something?

[Kevin Buzzard]

A related story : @Chris Hughes decided to do group actions yesterday, and his first question was "wait -- there's no mention of the inverse in the definition?". "No", I replied. "Oh dear, then we'll have to make it monoid actions if we want to get it into mathlib..."

[Johannes Hölzl]

semimodules would help to abstract some basic proofs and syntax. we can abstract the scalar multiplication over measure, outer_measure, measurable functions into ennreal, integrable functions into ennreal, etc...

[Mario Carneiro]

there is no integral in mathlibs measure theory, yet.

FYI I started working on that yesterday

[Kenny Lau]

nice

[Patrick Massot]

Does it mean you'll do derivatives as well?

[Mario Carneiro]

no, like Johannes said, those two are completely unrelated except for a certain fundamental theorem

[Mario Carneiro]

obviously the fundamental theorem can't be stated until we have both parts

[Patrick Massot]

There are indeed completely unrelated except for their fundamental relation

[Patrick Massot]

Anyway, it's already great to work on integrals

[Mario Carneiro]

I don't even think they operate on the same kinds of spaces. There are spaces with integrals but no derivatives and vice versa

[Patrick Massot]

sure

[Mario Carneiro]

so it's not like they are really different sides of the same coin, as in you could use either one to define the other

[Mario Carneiro]

but I guess people care about R -> R and it's true there

[Patrick Massot]

it's an important special case, especially for teaching purposes

[Mario Carneiro]

especially when it gives people the weird impression that these things are fundamentally related

[Mario Carneiro]

they are related, but not fundamentally

[Mario Carneiro]

in the foundational sense

[Patrick Massot]

Since you seem to be in an analytical mood, what about returning to the oldest open mathlib PR?

[Mario Carneiro]

Well, measure theory isn't quite analysis

[Mario Carneiro]

Let's put it next on the list

[Mario Carneiro]

that will set us up for derivatives

[Kenny Lau]

there is no integral in mathlibs measure theory, yet.

FYI I started working on that yesterday

how is it now?

[Mario Carneiro]

Johannes has taken over on that development

[Mario Carneiro]

I think it might be merged now? I heard some talk about it but I haven't checked

[Patrick Massot]

https://leanprover.zulipchat.com/#narrow/stream/116395-maths/subject/How.20much.20of.20analysis.20is.20formalised.3F/near/135735421

[Kenny Lau]

ok

[Niclas Kupper]

Hi, I'm new to Lean and trying to learn more by implementing point processes. I'm already stuck on the first definition. I want to create a new structure for measures that only take values in \nat and I am unsure why my approach doesn't work

structure finite_point_measure (α : Type*) [measurable_space α] extends measure α :=
(in_nats (A : set α) (measurable_set A) :
  ∃ n ∈ ℕ, measure_of A = n)

any help would be appreciated. If this is the wrong place to ask please just point me in the right direction. thanks~

[Yaël Dillies]

ℕ is a type, not a set, so n ∈ ℕ does not make sense. You want n : ℕ instead.

[Niclas Kupper]

Thanks, that is already helpful, sadly that did not fix the error yet. I'll play around a bit more and come back if I still can't fix it

[Riccardo Brasca]

In any case try to post #mwe (including the imports and so on, the idea is that we can copy/paste your code and see what happens). Note that measure refers to docs#measure, that is probably not what you want.

Finally, it's probably a good idea to open a new conversation in the "new members" stream. I can move your message if you want.

[Niclas Kupper]

Yes, thanks, will keep in mind in the future. I got it working now. Yes, you can move this to the new members stream, didn't see it earlier

[Vincent Beffara]

Also, you might want your measure to take values in docs#enat instead, since many (most?) point processes used in practice are only locally finite