Zulip Chat Archive
Stream: maths
Topic: RadonNikodym Theorem
Martin Zinkevich (Sep 18 2020 at 16:28):
Hello all,
I am Martin Zinkevich, a research scientist at Google in machine learning. I was pointed to LEAN by a colleague last fall and I fell in love with it,
in a big part because of the mathlib library.
I am interested in formalizing the foundations of machine learning theory, and along those lines,
I wrote a proof of the LebesgueRadonNikodym theorem for finite, unsigned measures:
https://github.com/google/formalml/blob/master/src/formal_ml/radon_nikodym.lean
I would love to make this theorem part of mathlib, although I realize there is a lot of work on my part to be done to make that happen.
I would also like to better understand the direction of the measure_theory portion of the library.
 I notice that there are very few uses of with_density. Is there an alternative elsewhere in the library?
 The measure_theory.measure.integral was removed. What should I use to represent integration over measures?
 Are signed measures going to appear soon, or are the nonfinite signed measures too cumbersome?

Z3 is available for the vanilla version of LEAN. Are there plans to make it available for the community one? In particular, the ability to solve real
inequalities with Z3 would be awesome! 
Having read over many of the files in mathlib, I still don't feel I understand where it is currently headed. Are there any RFCs that capture how the design is evolving, especially in the direction of probability and statistics?
In the github package above, I also explored ideas like using a subtype of set to represent a measurable set or event, and using Pr[A] to represent the probability of an event A as a nonnegative real. I am new to LEAN: what is the philosophy around when a subtype is appropriate and when a propositional function such as is_measurable should be used in its raw form?
Again, big fan,
Marty
Johan Commelin (Sep 18 2020 at 16:29):
@Floris van Doorn @Yury G. Kudryashov :up:
Johan Commelin (Sep 18 2020 at 16:29):
@Martin Zinkevich Welcome! We are always happy to hear such stories!
Johan Commelin (Sep 18 2020 at 16:32):
i'm not an expert on measure theory (in or outside of lean).
Re 5: we don't have many plans. people just work on whatever they like. maybe one of the only plans that is really sort of crystallized is that we want to formalize an entire undergraduate curriculum. progress is measured at https://leanprovercommunity.github.io/overview.html
Johan Commelin (Sep 18 2020 at 16:32):
Unfortunately we don't have anything on probability/stochastics/statistics at the moment. This is mostly due to the fact that we don't have contributors interested in it.
Johan Commelin (Sep 18 2020 at 16:33):
A little while ago, Yury did a massive refactor of integration theory. If anything was removed, it must have been replaced by something more general and or more powerful.
Rob Lewis (Sep 18 2020 at 16:37):
This is an impressive amount of work! It's always exciting to see signs that Lean has a life outside of mathlib. Although, in this case, that life should definitely be absorbed at some point ;)
Bryan Ginge Chen (Sep 18 2020 at 16:37):
Here's a thread from a few months ago on probability theory (mostly the lack thereof) in Lean. Note the links to @Koundinya Vajjha's repo (and @Alex J. Best's fork which updates it to a newer version of mathlib).
Rob Lewis (Sep 18 2020 at 16:38):
Z3 is available for the vanilla version of LEAN. Are there plans to make it available for the community one? In particular, the ability to solve real
inequalities with Z3 would be awesome!
As far as I know there was never a real connection to Z3. There was some very old work on an interface without proof reconstruction but I don't think it was ever used in production.
Johan Commelin (Sep 18 2020 at 16:39):
We do have some other tactics for proving inequalities. But I have no idea how they compare to Z3.
Rob Lewis (Sep 18 2020 at 16:40):
I don't think mathlib will ever accept Z3 proofs axiomatically.
Floris van Doorn (Sep 18 2020 at 19:07):
This is great! We definitely want the RadonNikodym Theorem in mathlib. I actually talked recently with @Jeremy Avigad that we should include it at some point. PR's are very welcome (generally we encourage to start with some small PRs, so you can start my just making a PR with some supporting lemmas)!
To answer the questions that were not answered before:
with_density
is just not used very much, I'm quite sure there is no alternative (because in that case, there should at the very least be lemmas and docstrings conneting these concepts). More properties aboutwith_density
are very welcome. More generally, you will notice that in all "leaves" of mathlib, important lemmas will be missing. Integration is definitely such a leaf. I don't know what
measure_theory.measure.integral
was. Is it either docs#measure_theory.integral or docs#measure_theory.lintegral? If not, what was its type?  AFAIK there is noone currently working on signed measures. However, if someone makes a PR with signed measures, that is definitely welcome to mathlib.
Floris van Doorn (Sep 18 2020 at 19:12):
About the last question: when to use subtypes and when to use predicates: it really depends on which one is more convenient. We regularly refactor definitions going from one to the other. But generally I think it's more convenient to work with predicates on objects than to work with a subtype of these objects.
However, this changes once you want to do operations on the subtype as a whole. For example, in most of the measure theory library we talk about functions f : \a \to \b
with a predicate measurable f
: most theorems are formulated with these extra conditions. However, in some cases (like docs#measure_theory.ae_eq_fun) we want to take a quotient on all measurable functions. So then we talk about the subtype of measurable functions and take a quotient of that.
Jeremy Avigad (Sep 18 2020 at 20:46):
I agree, it will be incredibly useful to have RadonNikodym in mathlib, in particular for defining conditional expectation. I am very impressed.
Patrick Massot (Sep 18 2020 at 21:02):
Indeed it would be really nice to have this in mathlib! The good news is you won't have to PR 10000 lines, I can see thousands of lines that prove lemmas we already have in mathlib or in the core library. Your layout style is also pretty far from mathlib and adds a lot of lines, in particular lines containing only curly braces. See our contribution guide. I'm sure you'll enjoy what you'll learn while turning this work into something suitable for mathlib, even if this will be a lot of work.
Martin Zinkevich (Sep 19 2020 at 03:59):
Don't worry, I won't dump a PR with 10,000 lines. :)
The integral I was referring to was:
https://github.com/leanprovercommunity/mathlib/blob/87f8ab22d97dfa5f76be928ba3aefe7bc8da5e4e/src/measure_theory/integration.lean#L1247
It was basically a lower integral, but defined as a method of a measure. I liked it, but no big deal, there is a lot to do before I worry about what
to replace it with.
I have already started cleaning up set.lean, identifying used and unused lemmas, and trying to find similar lemmas inside of mathlib and lean. I am pretty sure I can drop a few files wholesale, as mathlib has made progress since I started this project.
I created a short PR https://github.com/leanprovercommunity/mathlib/pull/4184 with a few theorems about sets. I'll take it slow until I learn more about the group's style and expectations.
Re: learning: I had never heard of lattice theory before working in Lean, and now it seems like the solution to everything. Hopefully, I will learn more about how mathematical fields connect, as well as metaprogramming and tactics, and just formal systems in general.
Stylistically (and I know this is a can of worms I am opening), I would love a tactic that handles any system of linear inequalities over the reals, nonnegative reals, and extended nonnegative reals, rather than proving a bunch of individual theorems by hand. I don't know how to do that in Lean, but it definitely would be cool.
Marty
Johan Commelin (Sep 19 2020 at 04:01):
Do you know about linarith
and nlinarith
?
Bryan Ginge Chen (Sep 19 2020 at 04:18):
See tactic#linarith and tactic#nlinarith .
Yury G. Kudryashov (Sep 21 2020 at 07:27):
I've recently rewrote integrals API in mathlib. Now the main integral takes measure as an argument.
Yury G. Kudryashov (Sep 21 2020 at 07:28):
So, just use src#measure_theory.lintegral
Yury G. Kudryashov (Sep 21 2020 at 07:29):
Statements should use notation introduced right after the definition.
Yury G. Kudryashov (Sep 21 2020 at 07:30):
As for signed measures, as far as I understand, the main difficulty is that you can't use the trick "any measure is an outer measure" anymore.
Yury G. Kudryashov (Sep 21 2020 at 07:35):
So, you have three options: (a) make μ
take (h : is_measurable s)
as an argument; (b) define measure as a total function and introduce the equivalent relation "equivalent on measurable subsets"; (c) do (b), them take the quotient, and coerce to a function using quotient.out
Martin Zinkevich (Sep 29 2020 at 07:23):
Thank you! I started using nlinarith and linarith. I will looking into the tactic tutorials to see if I can build on those for nnreal and ennreal.
I refactored the measure theory part to use the definitions and notation suggested. I used measure_theory.simple_func.lintegral where possible.
I feel that it might be simplest to start with a related result about RadonNikodym, as it has fewer dependencies and a more obvious path.
My worry is that the digression into topology may get bogged down.
I am not sure the name of this, but it is very useful for statistics, especially when considering the expectation of continuous random variables.
lemma measure_theory.with_density.compose_eq_multiply {Ω:Type*} [M:measurable_space Ω] (μ:measure_theory.measure Ω) (f g:Ω → ennreal) (H:measurable f) (H2:measurable g):
∫⁻ a, g a ∂ (μ.with_density f) = ∫⁻ a,(f * g) a ∂ μ :=
The proof structure is straightforward, building from a simple restricted function, to a simple function, to the lemma above:
lemma measure_theory.simple_func.restrict.compose_eq_multiply {Ω:Type*} [M:measurable_space Ω] (μ:measure_theory.measure Ω) (f:Ω → ennreal) (H:measurable f) (S:set Ω) (x:ennreal):
is_measurable S →
((measure_theory.simple_func.const Ω x).restrict S).lintegral (μ.with_density f)
= (∫⁻ a:Ω, (f * ⇑((measure_theory.simple_func.const Ω x).restrict S)) a ∂ μ) :=
There is also the concept of a "piece" of a simple function, but that seems like a natural detail on the way.
lemma measure_theory.simple_func.compose_eq_multiply {Ω:Type*} [M:measurable_space Ω] (μ:measure_theory.measure Ω)
(f:Ω → ennreal) (H:measurable f) {g:measure_theory.simple_func Ω ennreal}:
g.lintegral (μ.with_density f) = ∫⁻ a, (f * ⇑g) a ∂ μ :=
This would allow me to learn more about the style in the measure theory section before going on a grand adventure.
Thanks again for the wonderful feedback!
Martin Zinkevich (Sep 29 2020 at 15:37):
Oh, and perhaps this is part of the "structure" of the proof too. I defined a piece of a restrict, but cutting that definition away, there is the theorem:
lemma measure_theory.simple_func.sum_restrict {Ω:Type*} [measurable_space Ω]
(g:measure_theory.simple_func Ω ennreal):
g = g.range.sum (λ x, (measure_theory.simple_func.const Ω x).restrict (g ⁻¹' {x})) :=
giving a connection between simple functions and VERY simple functions. Or, I could just start sending pull requests.
Yury G. Kudryashov (Sep 29 2020 at 16:24):
I think that "start sending PRs" is a good idea.
Yury G. Kudryashov (Sep 29 2020 at 16:25):
Note that it's OK to make a PR with several almost trivial defs/theorems that you're going to use in the future PR to prove something mathematically meaningful.
Martin Zinkevich (Oct 04 2020 at 19:32):
Alright PR 4350 wraps up "compose_eq_multiply" (renamed lintegral_with_density_eq_lintegral_mul).
https://github.com/leanprovercommunity/mathlib/pull/4350
That was much compacted, and turned into a dozen lines of code when it was all done (thanks urkud!).
One step for RadonNikodym (if we are focusing on unsigned measures) is the following partition theorem, similar to the Hahn decomposition theorem:
lemma hahn_unsigned_inequality_decomp' {α:Type*} [M:measurable_space α]
(μ ν:measure_theory.measure α) [A1:measure_theory.finite_measure ν]:
(∃ X:set α, is_measurable X ∧ μ.restrict X ≤ ν.restrict X ∧ ν.restrict (Xᶜ) ≤ μ.restrict (Xᶜ)) := sorry
This has independent value: it is useful in reasoning about subtraction, infimum, and supremum.
Or, we could jump to nonnegative subtraction (defined analogously to ennreal.has_sub):
noncomputable instance measure_theory.measure.has_sub {α:Type*}
[measurable_space α]:has_sub (measure_theory.measure α) := ⟨λa b, Inf {d  a ≤ d + b}⟩
lemma decomposition_nonneg_sub {Ω:Type*} [measurable_space Ω]
(μ ν:measure_theory.measure Ω) (S T:set Ω) [A1:measure_theory.finite_measure μ]:
is_measurable T → is_measurable S → μ.restrict S ≤ ν.restrict S →
ν.restrict Sᶜ ≤ μ.restrict Sᶜ →
(ν  μ) T = ν (S ∩ T)  μ (S ∩ T) := sorry
Both of these rely on showing that {Sis_measurable S ∧ μ.restrict S ≤ ν.restrict S}
is a ring of sets closed under (measurable) subset and countable union.
Marty
Last updated: May 12 2021 at 07:17 UTC