Radon-Nikodym Theorem

Stream: maths

[Martin Zinkevich]

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 Lebesgue-Radon-Nikodym theorem for finite, unsigned measures:

https://github.com/google/formal-ml/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.

1. I notice that there are very few uses of with_density. Is there an alternative elsewhere in the library?
2. The measure_theory.measure.integral was removed. What should I use to represent integration over measures?
3. Are signed measures going to appear soon, or are the non-finite signed measures too cumbersome?

4. 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!

5. 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 non-negative 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]

@Floris van Doorn @Yury G. Kudryashov :up:

[Johan Commelin]

@Martin Zinkevich Welcome! We are always happy to hear such stories!

[Johan Commelin]

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://leanprover-community.github.io/overview.html

[Johan Commelin]

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]

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]

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 Gin-ge Chen]

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]

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]

We do have some other tactics for proving inequalities. But I have no idea how they compare to Z3.

[Rob Lewis]

I don't think mathlib will ever accept Z3 proofs axiomatically.

[Floris van Doorn]

This is great! We definitely want the Radon-Nikodym 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:

1. 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 about with_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.
2. 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?
3. AFAIK there is no-one currently working on signed measures. However, if someone makes a PR with signed measures, that is definitely welcome to mathlib.

[Floris van Doorn]

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]

I agree, it will be incredibly useful to have Radon-Nikodym in mathlib, in particular for defining conditional expectation. I am very impressed.

[Patrick Massot]

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]

Don't worry, I won't dump a PR with 10,000 lines. :-)

The integral I was referring to was:
https://github.com/leanprover-community/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/leanprover-community/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 non-negative 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]

Do you know about linarith and nlinarith?

[Bryan Gin-ge Chen]

See tactic#linarith and tactic#nlinarith .

[Yury G. Kudryashov]

I've recently rewrote integrals API in mathlib. Now the main integral takes measure as an argument.

[Yury G. Kudryashov]

So, just use src#measure_theory.lintegral

[Yury G. Kudryashov]

Statements should use notation introduced right after the definition.

[Yury G. Kudryashov]

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]

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]

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 Radon-Nikodym, 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]

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]

I think that "start sending PRs" is a good idea.

[Yury G. Kudryashov]

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]

Alright PR 4350 wraps up "compose_eq_multiply" (renamed lintegral_with_density_eq_lintegral_mul).
https://github.com/leanprover-community/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 Radon-Nikodym (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 non-negative 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 {S|is_measurable S ∧ μ.restrict S ≤ ν.restrict S} is a ring of sets closed under (measurable) subset and countable union.

-Marty