# Zulip Chat Archive

## Stream: general

### Topic: measure theory

#### Mario Carneiro (Jul 19 2018 at 20:30):

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 (Jul 19 2018 at 20:32):

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 (Jul 19 2018 at 20:32):

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

#### Kevin Buzzard (Jul 19 2018 at 20:32):

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

#### Mario Carneiro (Jul 19 2018 at 20:33):

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 (Jul 19 2018 at 20:34):

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

#### Kevin Buzzard (Jul 19 2018 at 20:34):

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

#### Mario Carneiro (Jul 19 2018 at 20:35):

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 (Jul 19 2018 at 20:35):

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

#### Kevin Buzzard (Jul 19 2018 at 20:35):

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

#### Patrick Massot (Jul 19 2018 at 20:35):

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

#### Kevin Buzzard (Jul 19 2018 at 20:36):

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

#### Kevin Buzzard (Jul 19 2018 at 20:36):

Just make it 0 :-)

#### Mario Carneiro (Jul 19 2018 at 20:37):

actually `ennreal`

is surprisingly nice as an ordered semiring

#### Mario Carneiro (Jul 19 2018 at 20:37):

the fact that it is a complete lattice really helps

#### Patrick Massot (Jul 19 2018 at 20:37):

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

#### Mario Carneiro (Jul 19 2018 at 20:39):

a basis of your 1-dimensional vector space

It's not a vector space

#### Patrick Massot (Jul 19 2018 at 20:39):

affine space I should say

#### Mario Carneiro (Jul 19 2018 at 20:39):

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

#### Mario Carneiro (Jul 19 2018 at 20:40):

there are no negatives

#### Kevin Buzzard (Jul 19 2018 at 20:40):

I am amazed that this is not already in Lean

#### Patrick Massot (Jul 19 2018 at 20:40):

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

#### Kevin Buzzard (Jul 19 2018 at 20:40):

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

#### Mario Carneiro (Jul 19 2018 at 20:40):

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

#### Kevin Buzzard (Jul 19 2018 at 20:41):

actually maybe that's a commutative monoid

#### Mario Carneiro (Jul 19 2018 at 20:42):

A nat-semi-module is a commutative monoid

#### Mario Carneiro (Jul 19 2018 at 20:42):

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

#### Patrick Massot (Jul 19 2018 at 21:16):

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 (Jul 20 2018 at 06:16):

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 (Jul 20 2018 at 06:17):

you were the one who mentioned the issue with `meaure'_union`

, right? I may have gone a bit overboard. :)

#### Sean Leather (Jul 20 2018 at 06:18):

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 (Jul 20 2018 at 07:05):

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 (Jul 20 2018 at 07:06):

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

#### Sean Leather (Jul 20 2018 at 07:06):

This is the `Mario`

variation of the `ᛗᛃᛟᛚᚾᛁᚱ`

tactic.

#### Johan Commelin (Jul 20 2018 at 07:08):

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

#### Kevin Buzzard (Jul 20 2018 at 07:08):

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

#### Kenny Lau (Jul 20 2018 at 07:09):

should have told me to write it lol

#### Kevin Buzzard (Jul 20 2018 at 07:09):

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

#### Kevin Buzzard (Jul 20 2018 at 07:09):

Things are happening :-)

#### Kenny Lau (Jul 20 2018 at 07:10):

have you proved that k[X] is UFD?

#### Kevin Buzzard (Jul 20 2018 at 07:10):

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

#### Kevin Buzzard (Jul 20 2018 at 07:10):

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

#### Kenny Lau (Jul 20 2018 at 07:10):

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

#### Kenny Lau (Jul 20 2018 at 07:11):

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 (Jul 20 2018 at 07:11):

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

#### Kevin Buzzard (Jul 20 2018 at 07:12):

We need more UG maths!

#### Johan Commelin (Jul 20 2018 at 07:13):

So we need more UG's, so that we can prove things `by UG`

. You do have access to two hammers!

#### Kenny Lau (Jul 20 2018 at 07:13):

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 (Jul 20 2018 at 07:13):

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

#### Johan Commelin (Jul 20 2018 at 07:14):

That was almost there, right?

#### Kenny Lau (Jul 20 2018 at 07:14):

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

#### Johan Commelin (Jul 20 2018 at 07:14):

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

#### Johan Commelin (Jul 20 2018 at 07:15):

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

#### Kenny Lau (Jul 20 2018 at 07:16):

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

#### Johannes Hölzl (Jul 20 2018 at 09:04):

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

#### Johannes Hölzl (Jul 20 2018 at 09:07):

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 (Jul 20 2018 at 09:11):

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 (Jul 20 2018 at 09:15):

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 (Jul 20 2018 at 09:17):

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

#### Patrick Massot (Jul 20 2018 at 09:17):

But let's have normed spaces first :wink:

#### Kevin Buzzard (Jul 20 2018 at 09:20):

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 `distrib`

s? 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 (Jul 20 2018 at 09:23):

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 (Jul 20 2018 at 09:25):

`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 (Jul 20 2018 at 18:26):

there is no integral in mathlibs measure theory, yet.

FYI I started working on that yesterday

#### Kenny Lau (Jul 20 2018 at 18:26):

nice

#### Patrick Massot (Jul 20 2018 at 18:26):

Does it mean you'll do derivatives as well?

#### Mario Carneiro (Jul 20 2018 at 18:27):

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

#### Mario Carneiro (Jul 20 2018 at 18:27):

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

#### Patrick Massot (Jul 20 2018 at 18:28):

There are indeed completely unrelated except for their fundamental relation

#### Patrick Massot (Jul 20 2018 at 18:28):

Anyway, it's already great to work on integrals

#### Mario Carneiro (Jul 20 2018 at 18:28):

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 (Jul 20 2018 at 18:29):

sure

#### Mario Carneiro (Jul 20 2018 at 18:29):

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 (Jul 20 2018 at 18:30):

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

#### Patrick Massot (Jul 20 2018 at 18:30):

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

#### Mario Carneiro (Jul 20 2018 at 18:31):

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

#### Mario Carneiro (Jul 20 2018 at 18:31):

they are related, but not fundamentally

#### Mario Carneiro (Jul 20 2018 at 18:32):

in the foundational sense

#### Patrick Massot (Jul 20 2018 at 18:32):

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

#### Mario Carneiro (Jul 20 2018 at 18:33):

Well, measure theory isn't quite analysis

#### Mario Carneiro (Jul 20 2018 at 18:33):

Let's put it next on the list

#### Mario Carneiro (Jul 20 2018 at 18:34):

that will set us up for derivatives

#### Kenny Lau (Oct 14 2018 at 12:56):

there is no integral in mathlibs measure theory, yet.

FYI I started working on that yesterday

how is it now?

#### Mario Carneiro (Oct 14 2018 at 12:58):

Johannes has taken over on that development

#### Mario Carneiro (Oct 14 2018 at 12:58):

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

#### Patrick Massot (Oct 14 2018 at 12:58):

#### Kenny Lau (Oct 14 2018 at 12:59):

ok

Last updated: May 08 2021 at 19:11 UTC