Zulip Chat Archive

Stream: general

Topic: measure theory


view this post on Zulip 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

view this post on Zulip 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).

view this post on Zulip 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".

view this post on Zulip Kevin Buzzard (Jul 19 2018 at 20:32):

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

view this post on Zulip 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"

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Jul 19 2018 at 20:34):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Jul 19 2018 at 20:35):

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

view this post on Zulip Patrick Massot (Jul 19 2018 at 20:35):

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

view this post on Zulip Kevin Buzzard (Jul 19 2018 at 20:36):

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

view this post on Zulip Kevin Buzzard (Jul 19 2018 at 20:36):

Just make it 0 :-)

view this post on Zulip Mario Carneiro (Jul 19 2018 at 20:37):

actually ennreal is surprisingly nice as an ordered semiring

view this post on Zulip Mario Carneiro (Jul 19 2018 at 20:37):

the fact that it is a complete lattice really helps

view this post on Zulip Patrick Massot (Jul 19 2018 at 20:37):

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

view this post on Zulip Mario Carneiro (Jul 19 2018 at 20:39):

a basis of your 1-dimensional vector space

It's not a vector space

view this post on Zulip Patrick Massot (Jul 19 2018 at 20:39):

affine space I should say

view this post on Zulip Mario Carneiro (Jul 19 2018 at 20:39):

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

view this post on Zulip Mario Carneiro (Jul 19 2018 at 20:40):

there are no negatives

view this post on Zulip Kevin Buzzard (Jul 19 2018 at 20:40):

I am amazed that this is not already in Lean

view this post on Zulip Patrick Massot (Jul 19 2018 at 20:40):

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

view this post on Zulip Kevin Buzzard (Jul 19 2018 at 20:40):

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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Jul 19 2018 at 20:41):

actually maybe that's a commutative monoid

view this post on Zulip Mario Carneiro (Jul 19 2018 at 20:42):

A nat-semi-module is a commutative monoid

view this post on Zulip Mario Carneiro (Jul 19 2018 at 20:42):

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

view this post on Zulip 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?

view this post on Zulip 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!

view this post on Zulip 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. :)

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Johan Commelin (Jul 20 2018 at 07:06):

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

view this post on Zulip Sean Leather (Jul 20 2018 at 07:06):

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

view this post on Zulip Johan Commelin (Jul 20 2018 at 07:08):

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

view this post on Zulip 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 :-/

view this post on Zulip Kenny Lau (Jul 20 2018 at 07:09):

should have told me to write it lol

view this post on Zulip Kevin Buzzard (Jul 20 2018 at 07:09):

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

view this post on Zulip Kevin Buzzard (Jul 20 2018 at 07:09):

Things are happening :-)

view this post on Zulip Kenny Lau (Jul 20 2018 at 07:10):

have you proved that k[X] is UFD?

view this post on Zulip Kevin Buzzard (Jul 20 2018 at 07:10):

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

view this post on Zulip Kevin Buzzard (Jul 20 2018 at 07:10):

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

view this post on Zulip 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"

view this post on Zulip 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 :)

view this post on Zulip Kevin Buzzard (Jul 20 2018 at 07:11):

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

view this post on Zulip Kevin Buzzard (Jul 20 2018 at 07:12):

We need more UG maths!

view this post on Zulip 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!

view this post on Zulip 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?

view this post on Zulip Kenny Lau (Jul 20 2018 at 07:13):

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

view this post on Zulip Johan Commelin (Jul 20 2018 at 07:14):

That was almost there, right?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Johan Commelin (Jul 20 2018 at 07:15):

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

view this post on Zulip Kenny Lau (Jul 20 2018 at 07:16):

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

view this post on Zulip Johannes Hölzl (Jul 20 2018 at 09:04):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Jul 20 2018 at 09:17):

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

view this post on Zulip Patrick Massot (Jul 20 2018 at 09:17):

But let's have normed spaces first :wink:

view this post on Zulip 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 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?

view this post on Zulip 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..."

view this post on Zulip 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...

view this post on Zulip Mario Carneiro (Jul 20 2018 at 18:26):

there is no integral in mathlibs measure theory, yet.

FYI I started working on that yesterday

view this post on Zulip Kenny Lau (Jul 20 2018 at 18:26):

nice

view this post on Zulip Patrick Massot (Jul 20 2018 at 18:26):

Does it mean you'll do derivatives as well?

view this post on Zulip Mario Carneiro (Jul 20 2018 at 18:27):

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

view this post on Zulip Mario Carneiro (Jul 20 2018 at 18:27):

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

view this post on Zulip Patrick Massot (Jul 20 2018 at 18:28):

There are indeed completely unrelated except for their fundamental relation

view this post on Zulip Patrick Massot (Jul 20 2018 at 18:28):

Anyway, it's already great to work on integrals

view this post on Zulip 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

view this post on Zulip Patrick Massot (Jul 20 2018 at 18:29):

sure

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jul 20 2018 at 18:30):

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

view this post on Zulip Patrick Massot (Jul 20 2018 at 18:30):

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

view this post on Zulip Mario Carneiro (Jul 20 2018 at 18:31):

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

view this post on Zulip Mario Carneiro (Jul 20 2018 at 18:31):

they are related, but not fundamentally

view this post on Zulip Mario Carneiro (Jul 20 2018 at 18:32):

in the foundational sense

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Jul 20 2018 at 18:33):

Well, measure theory isn't quite analysis

view this post on Zulip Mario Carneiro (Jul 20 2018 at 18:33):

Let's put it next on the list

view this post on Zulip Mario Carneiro (Jul 20 2018 at 18:34):

that will set us up for derivatives

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Oct 14 2018 at 12:58):

Johannes has taken over on that development

view this post on Zulip 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

view this post on Zulip Patrick Massot (Oct 14 2018 at 12:58):

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

view this post on Zulip Kenny Lau (Oct 14 2018 at 12:59):

ok


Last updated: May 08 2021 at 19:11 UTC