# Zulip Chat Archive

## Stream: new members

### Topic: Probability theory

#### Kalle Kytölä (Apr 03 2021 at 22:45):

I definitely agree that it would be great to have much of formal ML in mathlib. It seems like a fantastic addition to probability theory and I wasn't aware of it before. Thank you Joao for pointing it out! And of course thanks to Martin Zinkevich for the whole thing!

(Btw, I think it might be best to rename this discussion's topic to something more accurately descriptive, e.g. "probability theory", maybe starting from Floris' message. Renaming topics seems to require admin rights, though.)

#### Bryan Gin-ge Chen (Apr 03 2021 at 23:03):

(I've renamed the thread.)

#### Bryan Gin-ge Chen (Apr 03 2021 at 23:07):

I think @Koundinya Vajjha's repo at https://github.com/jtristan/stump-learnable has some material on probability theory as well.

#### Greg Price (Apr 06 2021 at 04:42):

Heather Macbeth said:

I am not sure what the etiquette here is, not to mention the ethics and the law -- if a person writes a Lean package under an open-source license (as Martin did with FormalML), is it ok for someone else to PR parts of it, keeping the copyright and authorship intact?

As far as ethics and law is concerned, the answer is yes and this is common practice in software.

It's necessary that the licenses be compatible -- that is, the original license and that of the project the material is then contributed to must not have conditions that conflict with each other -- but it looks like Formal ML uses exactly the same license as mathlib, so that's not an issue here.

(And of course it's essential to be explicit about the original authorship, essential ethically and also legally under typical open-source licenses.)

#### Greg Price (Apr 06 2021 at 04:42):

That doesn't answer the question of etiquette. I think the central question there is usually how the original author is likely to feel about it.

#### Hunter Monroe (Apr 17 2021 at 16:19):

I just sent an email to Martin Zinkevich asking his permission to integrate FormalML into mathlib. Attached is a first attempt to integrate his file probability_space.lean into mathlib. Here is an immediate issue. He defines a probability space (see https://github.com/google/formal-ml/blob/master/src/formal_ml/probability_space.lean) as follows:

```
class probability_space (α: Type*) extends measure_theory.measure_space α :=
(univ_one:volume.measure_of (set.univ) = 1)
```

whereas mathlib already has

```
class probability_measure (μ : measure α) : Prop := (measure_univ : μ univ = 1)
```

How should these be reconciled? probability_space.lean Also measurable_setB needs a better name.

#### Mario Carneiro (Apr 17 2021 at 16:20):

Those are the same? A probability space is a measure space where the designated "`volume`

" measure is a probability measure

#### Hunter Monroe (Apr 17 2021 at 16:32):

@Mario Carneiro Repeating "=1" seems redundant--one definition could rely on the other, i.e., a probability_space is a measure_space with a measure that is a probability_measure.

#### Mario Carneiro (Apr 17 2021 at 16:32):

That's what I just said

#### Mario Carneiro (Apr 17 2021 at 16:34):

I don't think it matters too much whether the field is ` (univ_one:volume.measure_of (set.univ) = 1)`

or `[prob : probability_measure volume]`

#### Mario Carneiro (Apr 17 2021 at 16:35):

the former is probably a bit more convenient when constructing probability spaces

#### Mario Carneiro (Apr 17 2021 at 16:35):

but you can have constructors for both versions

#### Eric Wieser (Apr 18 2021 at 11:19):

Judging by your first PR to attempt to integrate formalML into mathlib, it may make sense to first integrate mathlib into formalML; despite depending on mathlib, the library seems to repeat lots of our lemmas.

#### Eric Wieser (Apr 18 2021 at 11:20):

I guess how viable that is depends on whether Martin has the time to accept pull requests.

#### Scott Morrison (Apr 18 2021 at 11:28):

Or simply fork.

#### Hunter Monroe (May 21 2021 at 15:33):

@Eric Wieser @Mario Carneiro I have created a branch probability_theory with the new file probability_space.lean based on @Martin Zinkevich's formal-ml (https://github.com/leanprover-community/mathlib/blob/probability_theory/src/probability_theory/probability_theory.lean). This has nearly 700 lines of code, as a first step, from 3300 in the formal-ml file. I wanted to touch base before I submit a pull request. There are no repeated lemmas from mathlib that I could see. How does this look?

#### Eric Wieser (May 21 2021 at 15:52):

A quick skim:

`probability_space.to_measurable_space`

should be automatic; in general, when adding an instance you can check if it's needed by first trying to define it with`by apply_instance`

`measurable_set_sub`

looks like a bad idea to me. Why not skip straight to`event`

, and define it as`abbreviation event : Type* := {x : set Ω // measurable_set x}`

. That's likely to remove the need for most of the lemmas in the first 100 lines.`to_ennreal_monotonic`

exists already as docs#ennreal.coe_mono.`library_search`

tells me that. In general, if you put all the arguments before the colon,`library_search`

will have an easier time finding it. If you write a lemma`lemma foo : A → B := begin intro a, ... end`

then really you should have written`lemma foo (a : A) : B := begin ... end`

#### Eric Wieser (May 21 2021 at 15:54):

- I don't think you should even be writing
`volume.measure_of x`

- the canonical spelling should be`volume x`

#### Eric Wieser (May 21 2021 at 16:10):

- Instead of
`{Ω : Type*} {P : probability_space Ω} (X : event P)`

you probably want`{Ω : Type*} [probability_space Ω] (X : event Ω)`

#### Eric Wieser (May 21 2021 at 16:14):

@Mario Carneiro, thoughts on renaming docs#measurable_set to `is_measurable`

so that `measurable_set`

can be used to instead mean `subtype is_measurable`

?

#### Hunter Monroe (May 21 2021 at 16:34):

@Eric Wieser thanks. If I skip straight to `abbreviation event : Type* := {x : set Ω // measurable_set x}`

, how do I address the error 'unknown identifier Ω'--does that not require a def? How would I modify the code to use the automatic instance? When I drop `measure_of`

, how do I address the error "invalid field notation, volume does not have explicit argument with type ...". Your patience is appreciated.

#### Eric Wieser (May 21 2021 at 16:36):

See my edited message

#### Eric Wieser (May 21 2021 at 16:36):

```
def event (Ω : Type*) [measurable_space Ω] : Type* := {x : set Ω // measurable_set x}
```

#### Eric Wieser (May 21 2021 at 16:37):

Then your lemmas below become something like:

```
lemma Pr_le_one {Ω : Type*} [probability_space Ω] {E : event Ω} : Pr[E] ≤ 1 :=
```

#### Eric Wieser (May 21 2021 at 16:37):

invalid field notation, volume does not have explicit argument with type ...

Change it from `P.volume.measure_of x`

to `volume x`

. You need to drop the `P.`

too

#### Eric Wieser (May 21 2021 at 16:52):

I made a start on a very rough start on some of those changes here, which should be enough to answer some of your questions: https://gist.github.com/eric-wieser/1f119d6c22a9d14f5200f2be7b7ce511

#### Sebastien Gouezel (May 24 2021 at 08:13):

I am not really convinced by the design choice to try to hide as much as measure theory as possible, because I have the impression it will lead to a lot of code duplication. The branch uses `event`

for a measurable set, and then formulates everything in terms of events. But this means that you will need to recreate all the set API for events (unions, intersections, diffs, Unions, sum over a finite event, and so on), and also all measure theory library (Lebesgue dominated convergence theorem, Fatou's lemma, and so on, and so on. It would feel to me much more economical to use standard terminology with measurability assumptions. And ideally one would craft a `measurability`

tactic that one would use as a default tactic to fill all measurability fields when one applies lemmas.

#### Eric Wieser (May 24 2021 at 08:26):

To me it seems the key change being proposed by this code is "a bundled version of`measurable_set`

would be useful"

#### Eric Wieser (May 24 2021 at 08:26):

Along with lots of noise duplicating API

#### Eric Wieser (May 24 2021 at 09:07):

I made a PR providing some instances in #7702

#### Sebastien Gouezel (May 24 2021 at 09:07):

Also, we already have `probability_measure`

, so I don't think `probability_space`

is useful. Just using `(Pr : measure \alpha) [probability_measure Pr]`

should be enough.

#### Eric Wieser (May 24 2021 at 09:07):

docs#measure_theory.probability_measure ~~seems not to exist~~

#### Eric Wieser (May 24 2021 at 09:10):

Presumably `[probability_measure (volume : measure_theory.measure α)]`

would also work? (and be a direct substitution for the typeclass Hunter is proposing)

#### Sebastien Gouezel (May 24 2021 at 09:13):

Thinking of standard probability measure changes arguments à la Girsanov, I think keeping the probability measure explicit can only help.

#### Sebastien Gouezel (May 24 2021 at 09:16):

The only drawback of this is that a measure is `ennreal`

-valued, while here we would want to use mainly the real-valued version. We should probably introduce something like `measure.fin \mu (A) = (\mu A).to_real`

, and use `Pr_ennreal`

for the full measure and a notation for `Pr = Pr_ennreal.fin`

.

#### Sebastien Gouezel (May 24 2021 at 11:47):

Another issue I have with the `event`

idea is that very often there are several sigma-algebras playing together (martingales are a basic probabilistic object built precisely around this idea, but it also shows up all the time in Markov chains). So one would need to define a bunch of "events" for these different sigma-algebras, but it is well known that doing operations on bundled objects is painful (like, if you have `A`

which is an event for the sigma algebra `B`

, and `A'`

which is an event for the sigma algebra `B'`

, then what is `A \cap A'`

? With plain sets, you just have a set, and then depending on the relationships between `B`

and `B'`

you can argue that this intersection belongs to `B`

, or to `B'`

, or maybe to yet another natural sigma-algebra, depending on the situation at hand).

#### Eric Wieser (May 24 2021 at 11:49):

but it is well known that doing operations on bundled objects is painful

Sure, but also mathlib seems to have fallen into a convention of bundling them anyway. A similar case comes up with "what is `x + y`

" when `x`

and `y`

are from different add_subgroups. You can always escape to unbundled land with coercions, and an API around `event`

(aka `subtype measuable_set`

) could behave just the same

#### Sebastien Gouezel (May 24 2021 at 11:55):

Eric Wieser said:

but it is well known that doing operations on bundled objects is painful

Sure, but also mathlib seems to have fallen into a convention of bundling them anyway.

I am not so sure about that: I'd rather say that mathlib is pragmatic, and tries to make the most common operation the easiest possible. Adding elements of different add_subgroups is not really common, while intersecting measurable sets coming from different sigma-algebras will happen all the time.

#### Sebastien Gouezel (May 24 2021 at 11:59):

Maybe a difficulty here is that elementary probability theory, as taught to undergrads say, is mostly taking finite intersections of sets within a fixed sigma-algebra, and never needs anything fancy in measure theory. While more advanced probability theory is very different from this naive point of view.

#### Eric Wieser (May 24 2021 at 12:00):

I think I can see the argument for why you need the unbundled approach, but it's not clear to me why you can't also have the bundled approach for convenience in the simple cases. Ignoring the "more accessible to undergrads" argument, the "does boring book-keeping for you" argument still holds

#### Eric Wieser (May 24 2021 at 12:02):

Any by "have the bundled approach for convenience", I guess I really just mean "provide a `[measurable_space α] : boolean_algebra (subtype (measurable_set : set α → Prop))`

instance somewhere".

#### Sebastien Gouezel (May 24 2021 at 12:11):

Except that one also takes a lot of countable intersections, preimages under measurable functions, and so on. That's why a tactic seems to me to be more suited for the job (there is such a tactic in Isabelle, and 99% of the time you don't need to mention measurability, it's just taken care of transparently).

#### Eric Wieser (May 24 2021 at 12:23):

Preimages don't sound like aren't a major obstacle, we have docs#submonoid.comap etc. Countable intersections I guess are problematic as mathlib only has lemmas about countable intersections of sets, not on arbitrary lattices?

#### Kalle Kytölä (May 24 2021 at 16:06):

My inexperienced but interested user's opinion so far matches well with many of the things Sebastien has said here. But I don't intend that as an opinion about implementation (I am not yet in a position to have one).

I have played a bit with Lean's probability theory (i.e., measure theory) as a first formalization exercise for myself after some tutorials (NNG of course, Kevin's "Formalizing math" course, and some parts of "Lean together"). I feel parts of the library are quite mature, and I can (painfully slowly) do things I would hope to.

I in particular agreed with Sebastien about all of the following:

- One very often wants to use many probability measures; whether in coupling arguments, or convergence in distribution, or in change-of-measure arguments (e.g., Girsanov's theorem).
- It seems essential in probability theory and stochastic processes to be able to work with many (sub)sigma-algebras on the same set; conditional expected values and martingales being probably the most prominent cases.
- Every now and then coercions between
`ennreal`

s and either`nnreal`

s or`ℝ`

get me stuck quite badly. For probabilities, these difficulties feel like they should not be there, but for expected values they are essentially as unavoidable as with integrals against general measures. - Settling measurability questions by hand is sometimes indeed a pain (in Lean and to some extent on pen and paper). This seems to correspond to maths students' experience with measure-theoretic probability as well: often the most tedious step in probability courses are related to verifications of measurability (or other measurability issues such as indistinguishability / versions / ...). I have no idea about tactics except that when they work, they are fantastic. So if it is possible to have a
`measurability`

tactic as Sebastien proposes, I will be super happy!

To be clear, these are just my experiences as a beginner, and not an opinion on how to develop the mathlib probability library. I am very impressed with the existing library and its implementation, so obviously the experts here (including in this thread) know what they are doing :).

#### Eric Wieser (May 24 2021 at 21:47):

@Sebastien Gouezel, I've got an approval on #7702 which I mention above. Are you against having these instances, or just claiming they're not nearly as useful as they might first look? If the latter, I'll go ahead and merge, since even if the instances aren't that helpful, they seem like the obvious instances to have available.

#### Sebastien Gouezel (May 25 2021 at 05:35):

I'm definitely fine with having this merged! We will see later if this turns out to be useful or not so much.

#### Eric Wieser (May 25 2021 at 11:22):

A follow-up question; which of these is preferable for working with `subtype (measurable_set : set α → Prop)`

?

- Give that type a new name like
`event α`

(does this make sense for non-probability spaces? Is there a better name?) - Rename
`measurable_set s`

to`is_measurable_set s`

, so that that we can repurpose`measurable_set α`

to mean `subtype (is_measurable_set : set α → Prop) - Do not introduce a new name, and require users to work with the
`subtype`

directly. The main disadvantage of this approach is a lack of an obvious namespace to put definitions and lemmas about the bundled type in.

#### Hunter Monroe (May 29 2021 at 04:05):

@Eric Wieser I have substantially updated probability_space.lean from formal-ml for inclusion in mathlib here (https://github.com/leanprover-community/mathlib/blob/1e717b785574bb153f1f3a1b3d0ff644b905751f/src/probability_theory/probability_space.lean). This now avoids creating many lemmas already in mathlib. I ran into a few roadblocks where I would appreciate your help again.. These are marked TODO. If you can help me resolve these, there are many other probability/machine learning components in formal-ml that would be good additions to mathlib.

Line 70. "def event" should replace "measurable_space" with "probability_space" but then I could not resolve all the errors when I changed this.

Line 649. Should we get rid of the alternative definition of measurable_set as measurable_setB (which I could work out how to do) or just keep it with a name like "measurable_space_sub".

Line 1068. "lemma eall_finset_empty" is commented out because I could not resolve the type mismatch.

Line 1122. I brought back "infix ` •ℕ `

:70 := nsmul" from an older version of mathlib to get this to compile. How do I get rid of it again?

Line 1148. See new definition of "noncomputable def classical.decidable_eq" which I could not eliminate

There are compile errors I could not resolve: line 1050, 1408 (Pr_exists_eq_powerset), 1492 (independent_events_not_of_independent_events), 2880 (Pr_eany_sum), 3260, 3298 (independent_events_empty), 3410 (and_mem_exists), 3521 (Pr_sum_partition), 3542 (conditional_independent_event_pair_limit), 3580 (compose_independent_pair_right).

Line 2250. Is "measurable_set_prod'" necessary given "measurable_set_prod"

Line 2326. "noncomputable def fintype.encodable" could be imported from data.equiv.list rather than being redefined here.

Line 2402. Is "singleton_prod'" needed given "set.prod_singleton_singleton"?

Line 2594. Can lemma eq_or_ne2 be dropped?

Line 2605, 3029, 3124. Move to nnreal?

Lines 2624, 2686, 2707, 2710, 2725, 2738, 2754, 2770, 2780, 2787, 2843, 2854, . Move to sum?

Lines 3043, 3061, 3076. Move to set?

Hunter

#### Eric Wieser (May 29 2021 at 06:27):

Line 70 is better with `measurable_space`

#### Eric Wieser (May 29 2021 at 06:28):

Line 649: `measurable_setB`

is not an "alternative definition", it's an identical one to `event`

. There is no reason to keep it.

#### Eric Wieser (May 29 2021 at 06:31):

Line 83: this already exists, docs#measurable_set.subtype.has_mem

#### Eric Wieser (May 29 2021 at 06:33):

Line 210: `has_emptyc_event`

already exists, it's docs#measurable_set.subtype.has_emptyc.

#### Eric Wieser (May 29 2021 at 06:44):

Line ???: eany_finset is docs#finset.sup

#### Eric Wieser (May 29 2021 at 07:32):

I don't remember if I said this before, but I don't think your current approach to trying to pull parts of formal-ml into mathlib is going to be fruitful. Here's the approach I would take if I were invested in this project:

- Make a fork of formal-ml, and in that fork: ..
- Turn on CI (like I suggested in Google/formal-ml#1)
- Fix the build. Formal_ml currently doesn't compile without any changes
- Run
`leanproject up`

. Fix the build. The community on Zulip can likely help with bits of this step, as the people here (like me) are usually responsible for the breakage I. The first place. This step is the hardest one - Look for parts of formal-ml that duplicate mathlib and remove them. Make sure the build still works by replacing their uses with mathlib equivalents. #Is there code for X? can help with (self-contained) "does mathlib already have this" questions.
- Start looking for small bits of the now-compatible formal-ml that can be added to mathlib.
- Add these to mathlib, update mathlib in formal-ml, then remove them from formal-ml

By skipping straight to this penultimate step as you are now, you're not only squashing all the hard work into one extra hard task, but you're also putting all your eggs into one basket; if your code doesn't end up in mathlib, then all your work essentially ends up discarded. With my suggestion, you still end up with a better formal-ml, even if it doesn't make it into mathlib.

#### Eric Wieser (May 29 2021 at 08:09):

(deleted)

#### Hunter Monroe (May 31 2021 at 18:09):

Thanks, I am making good progress on steps 4-5--no point in fixing broken bits that are unused or duplicate. I am primarily using `library_search`

--has anyone explored making this faster for instance through indexing?

Eric Wieser said:

- Run
`leanproject up`

. Fix the build. The community on Zulip can likely help with bits of this step, as the people here (like me) are usually responsible for the breakage I. The first place. This step is the hardest one- Look for parts of formal-ml that duplicate mathlib and remove them. Make sure the build still works by replacing their uses with mathlib equivalents. #Is there code for X? can help with (self-contained) "does mathlib already have this" questions. ```

#### Eric Wieser (May 31 2021 at 18:50):

The point in fixing formal-ml *before* updating mathlib (step 3) is to separate "this code is broken because it is wrong" and "this code is broken because the community broke it"

#### Eric Wieser (May 31 2021 at 18:56):

Ah, I see you "fixed" CI by commenting out bits you don't care about - that's probably ok

#### Eric Wieser (May 31 2021 at 18:58):

Nice job on getting it passing, anyway!

#### Hunter Monroe (May 31 2021 at 19:52):

Yes, I got formal-ml to compile before upgrading, as there were only 1-2 two issues (I commented out a few tricky-looking bits) and also discovered that #check and #print send output to the console without triggering a CI failure. After upgrading, I was able to fix almost all community-broken code by hand and using library_search (can we provide deprecated defs/thms/lemmas that point to the new ones). The big task now is finding code that duplicates mathlib relying largely on running library_search over a hundred times, and factoring it out out manually (wish I had Eclipse-like "inline/extract" refactoring tools to do this automatically). I am holding off committing until I have finished or reached a roadblock.

#### Hunter Monroe (May 31 2021 at 20:50):

Is there a way to check if a definition duplicates one already in mathlib?

#### Mario Carneiro (May 31 2021 at 20:51):

`library_search`

is probably the best automatic method, but I would recommend reading all the theorem statements in files that seem to be in the same topic as what you are porting

#### Bryan Gin-ge Chen (May 31 2021 at 20:52):

You can also ask in the #Is there code for X? stream.

#### Scott Morrison (May 31 2021 at 22:20):

There is hopefully scope to make library_search faster, but it will rely on good caching. `library_search`

under the hood is just using `apply`

, and the "problem" is that Leo did an incredible job of making `apply`

_fast_: so fast that any naive filtering you do actually makes things slower.

But in the context of running library_search relative to a fixed library (i.e. mathlib), presumably you can cache a lot of the work required to build indices, and it would be great if someone did this!

#### Eric Wieser (Jun 01 2021 at 10:37):

Eric Wieser said:

Mario Carneiro, thoughts on renaming docs#measurable_set to

`is_measurable`

so that`measurable_set`

can be used to instead mean`subtype is_measurable`

?

Huh, it used to be called `is_measurable`

but was renamed to `measurable_set`

in #6001. Perhaps `is_measurable_set`

would be a better name.

#### Hunter Monroe (Jun 02 2021 at 00:04):

How can I use the instance "measurable_set.subtype.has_emptyc" rather than the instance on the third line below? If I comment out that line, then there is a redline under the ∅ symbol.

def event (Ω : Type*) [measurable_space Ω] : Type* := {x : set Ω // measurable_set x}

def event_empty (Ω : Type*) [measurable_space Ω] : event Ω := { val := ∅, property := measurable_set.empty,}

instance has_emptyc_event {Ω : Type*} {M : measurable_space Ω} : has_emptyc (event Ω) := ⟨ @event_empty Ω M ⟩

lemma has_emptyc_emptyc_event {Ω : Type*} [probability_space Ω] : ∅ = (event_empty Ω) := sorry

#### Scott Morrison (Jun 02 2021 at 00:06):

#### Scott Morrison (Jun 02 2021 at 00:06):

In front of `def event`

write `@[derive has_emptyc]`

.

#### Scott Morrison (Jun 02 2021 at 00:06):

This is how you copy instances to a type synonym.

#### Hunter Monroe (Jun 02 2021 at 00:21):

Cool. But that does not seem to work for `@[derive has_mem]`

as there is an error "type expected at has_mem"

```
instance {Ω : Type*} [P : probability_space Ω] : has_mem Ω (event Ω) := { mem := event_mem }
lemma event_mem_val {Ω : Type*} [P : probability_space Ω] (ω : Ω) (E : event Ω) : (ω ∈ E) = (ω ∈ E.val) := rfl
```

#### Scott Morrison (Jun 02 2021 at 00:24):

`derive`

takes typeclasses with just one argument. You may need to write a lambda to tell it what the other argument of `has_mem`

should be.

#### Scott Morrison (Jun 02 2021 at 00:24):

Per #backticks, if you use triple backticks you'll get a code block, which is more readable.

#### Scott Morrison (Jun 02 2021 at 00:25):

It's also much easier to give a complete answer if you post a #mwe, so others can copy and paste your problem into Lean.

#### Scott Morrison (Jun 02 2021 at 00:25):

If they have to add imports and variables themselves they're just not going to do it, so you get vaguer answers. :-)

#### Hunter Monroe (Jun 02 2021 at 00:29):

Got it, how would you suggest proving the last below (now a mwe)

```
import measure_theory.measure_space
open measure_theory measurable_space
class probability_space (α : Type*) extends measure_space α := (volume_univ : volume (set.univ) = 1)
@[derive has_emptyc] def event (Ω : Type*) [measurable_space Ω] : Type* := {x : set Ω // measurable_set x}
def event_empty (Ω : Type*) [measurable_space Ω] : event Ω := { val := ∅, property := measurable_set.empty,}
lemma has_emptyc_emptyc_event {Ω : Type*} [probability_space Ω] : ∅ = (event_empty Ω) := sorry```
```

#### Mario Carneiro (Jun 02 2021 at 00:31):

Put a return after the ` ``` `

, or else it will eat the first line of the code block and not syntax highlight it

#### Scott Morrison (Jun 02 2021 at 00:31):

(Put a newline after the initial three backticks.)

#### Mario Carneiro (Jun 02 2021 at 00:32):

also before the final ` ``` `

, or else it will show up at the end of the code block

#### Scott Morrison (Jun 02 2021 at 00:34):

`rfl`

?

#### Hunter Monroe (Jun 02 2021 at 00:35):

Actually never mind, this lemma is not needed for what it was being used for

#### Scott Morrison (Jun 02 2021 at 00:35):

And just to demonstrate how to format this:

```
import measure_theory.measure_space
open measure_theory measurable_space
class probability_space (α : Type*) extends measure_space α :=
(volume_univ : volume (set.univ) = 1)
@[derive has_emptyc]
def event (Ω : Type*) [measurable_space Ω] : Type* :=
{x : set Ω // measurable_set x}
def event_empty (Ω : Type*) [measurable_space Ω] : event Ω :=
{ val := ∅, property := measurable_set.empty,}
lemma has_emptyc_emptyc_event {Ω : Type*} [probability_space Ω] : ∅ = (event_empty Ω) :=
rfl
```

#### Scott Morrison (Jun 02 2021 at 00:36):

As I said, the proof is just `rfl`

, and you certainly don't need this lemma because you don't need the definition `event_empty`

, because you can just use `∅`

.

#### Mario Carneiro (Jun 02 2021 at 00:38):

You missed the first line, which was `import measure_theory.measurable_space`

, although it's not needed since it is implied by the second import

#### Scott Morrison (Jun 02 2021 at 00:39):

I deleted it on purpose. :-)

#### Eric Wieser (Jun 02 2021 at 06:55):

I think it might be a good idea to replace `def event`

with `abbreviation event`

? Since that way, you get all the instances and lemmas about them for free.

#### Mario Carneiro (Jun 02 2021 at 07:00):

I don't think that would be a good idea. The space of measurable sets is quite structured (it's a sigma algebra!) so it would be better to have it be its own thing with a lattice instance (although that means that it should probably use `\bot`

instead of `\empty`

)

#### Eric Wieser (Jun 02 2021 at 08:14):

I don't see the problem - the only typeclasses we have on `subtype measurable_set`

right now are precisely the ones Hunter wants

#### Eric Wieser (Jun 02 2021 at 08:14):

So why not make `event`

, which is defined as that, reducible?

#### Eric Wieser (Jun 02 2021 at 08:15):

The lattice instance exists already as docs#measurable_set.subtype.boolean_algebra

#### Hunter Monroe (Jun 04 2021 at 04:00):

How can I make event_univ have the type of event?

```
import measure_theory.measurable_space
import measure_theory.measure_space
open measure_theory measurable_space
@[derive [has_union,has_emptyc,has_compl, has_sdiff,has_union,has_inter]]
def event (Ω : Type*) [measurable_space Ω] : Type* := {x : set Ω // measurable_set x}
class probability_space (α : Type*) extends measure_space α := (volume_univ : volume (set.univ) = 1)
def event_univ (Ω : Type*) [measurable_space Ω] : event Ω :=
{ val := set.univ, property := measurable_set.univ,}
```

#### Scott Morrison (Jun 04 2021 at 04:08):

I don't understand your question. Doesn't it have type `event Ω`

already in your code block?

#### Scott Morrison (Jun 04 2021 at 04:09):

Also --- I think you may have missed Eric's comment above that already the entire `boolean_algebra`

structure is available, you should just `derive`

that.

#### Eric Wieser (Jun 04 2021 at 07:16):

Or make `event`

reducible (via `abbreviation`

) so that you don't need to derive anything, *and* you get a handful of simp lemmas for free

#### Eric Wieser (Jun 04 2021 at 07:17):

With the `boolean_algebra`

structure, `event_univ`

is `⊤`

.

#### Hunter Monroe (Jun 06 2021 at 21:02):

Cool, so I change `def`

to `abbreviation`

in front of `event`

, but how would I define `event_univ`

as top leveraging the `boolean_algebra`

structure (or otherwise). Right now, `event_univ`

is not `event`

but a Pi type: `event_univ : Π (Ω : Type u_1) [_inst_1 : measurable_space Ω], event Ω`

. Also, if I derive `boolean_algebra`

, do I still need `has_union`

etc?

```
import measure_theory.measurable_space
import measure_theory.measure_space
open measure_theory measurable_space
@[derive [boolean_algebra,has_union,has_emptyc,has_compl, has_sdiff,has_union,has_inter]] -- is `has_union` etc needed?
abbreviation event (Ω : Type*) [measurable_space Ω] : Type* := {x : set Ω // measurable_set x}
class probability_space (α : Type*) extends measure_space α := (volume_univ : volume (set.univ) = 1)
def event_univ (Ω : Type*) [measurable_space Ω] : event Ω := { val := set.univ, property := measurable_set.univ,} -- does not work
#check event_univ --should be type event
def event_univ' (Ω : Type*) [measurable_space Ω] : event Ω := Ω.T -- ??? --how to make this "top"
```

And then, would the `boolean_algebra`

structure allow me to avoid new definitions of "and" etc for events, currently given as

```
def measurable_inter {Ω : Type*} [measurable_space Ω] (A B : event Ω) : event Ω := { val :=A.val ∩ B.val, property := measurable_set.inter A.property B.property,}
def eand {Ω : Type*} [probability_space Ω] (A B : event Ω) : event Ω := measurable_inter A B
infixr `∧` := eand
def enot {Ω : Type*} [probability_space Ω] (A : event Ω) : event Ω := { val :=(A).valᶜ, property := measurable_set.compl A.property,}
def event_eqv {Ω:Type*} {p:probability_space Ω} (A B:event Ω):event Ω := (A ∧ B) ∨ ((¬ₑ A) ∧ (¬ₑ B))
infixr `=ₑ`:100 := event_eqv
-- `measurable` is already in mathlib so `measurable_fun` seems duplicative
def measurable_fun {α:Type*} {β:Type*} (Mα:measurable_space α) (Mβ:measurable_space β):Type*:= subtype (@measurable α β _ _)
instance probability_space.to_measurable_space (α:Type*) [probability_space α]:measurable_space α := measure_theory.measure_space.to_measurable_space
def random_variable {α:Type*} (p:probability_space α) {β:Type*} (Mβ:measurable_space β):Type* := measurable_fun (probability_space.to_measurable_space α) Mβ
infixr ` →ₘ `:80 := measurable_fun
infixr ` →ᵣ `:80 := random_variable
```

#### Eric Wieser (Jun 06 2021 at 21:16):

For eand and eor, you can probably just do `infixr `∧` := has_inf.inf`

. if that doesn't work, copying the approach used by src#set.Union would probably work

#### Eric Wieser (Jun 06 2021 at 21:20):

That could look like

```
@[reducible]
def eand {Ω : Type*} [probability_space Ω] : event Ω → event Ω → event Ω := (⊓)
infixr `∧` := eand
@[reducible]
def enot {Ω : Type*} [probability_space Ω] : event Ω → event Ω := has_compl.compl
```

#### Eric Wieser (Jun 06 2021 at 21:21):

`(⊤ : event Ω)`

is how to spell `event_univ`

, but most of the time ` ⊤`

by itself will work, if you use it where lean is expecting an event.

#### Eric Wieser (Jun 06 2021 at 21:25):

You still need `has_union`

if you want to be able to write `Ea ∪ Eb`

as another spelling of `Ea ⊔ Eb`

. However, it sounds like you want to prefer a `Ea ∨ Eb`

spelling anyway, so I wouldn't bother worrying about ` ∪`

#### Mario Carneiro (Jun 07 2021 at 04:13):

Eric Wieser said:

I don't see the problem - the only typeclasses we have on

`subtype measurable_set`

right now are precisely the ones Hunter wants

I think the question to solve then is whether we intend to write this subtype as `subtype measurable_set`

or `event`

(or something else), and in either case there should be no abbreviation

#### Eric Wieser (Jun 07 2021 at 06:26):

I agree that we ought to decide on a spelling, but I can't help feeling that even if we pick `event`

as the preferred spelling, it's useful for `event`

to be reducible so that all the subtype coercion lemmas are easier to use.

#### Rémy Degenne (Jun 07 2021 at 06:51):

Would having sub-lattice, sub-boolean-algebra and such structures make working with those coercions easier? Event would be defined as a sub-boolean-algebra for example. This is a question, not a suggestion, since those aspects are not very clear to me.

We could define sub-sigma-algebra as well if we define those substructures, in order to get the properties of countable unions.

#### Rémy Degenne (Jun 07 2021 at 07:08):

Or maybe you already proved all the properties provided by `set_like`

and the usual substructure construction for `subtype measurable_set`

and it would make no difference. Turns out, I really don't know what I am talking about here, hence I'll stop. :)

#### Eric Wieser (Jun 07 2021 at 07:54):

Yes, having sublattices in some form would help here

#### Rémy Degenne (Jun 07 2021 at 07:55):

There was a start towards sublattices in #7093, but it looks abandoned.

#### Eric Wieser (Jun 07 2021 at 08:01):

Although I'm starting to consider an alternative design, with a new typeclass `subtype.closed_under`

, and have instances like:

```
import order.lattice
/-- A class indicating a property holds on `op` if it holds on both arguments -/
class subtype.closed_under₂ {α} (p : α → Prop) (op : α → α → α) :=
(closed : ∀ {a b}, p a → p b → p (op a b))
instance {α} [has_inf α] (p : α → Prop) [h : subtype.closed_under₂ p (⊓)] : has_inf (subtype p) :=
{ inf := λ a b, ⟨a ⊓ b, subtype.closed_under₂.closed _ a.2 b.2⟩}
instance subtype.semilattice_inf_of_closed_under
{α} [semilattice_inf α] (p : α → Prop) [h : subtype.closed_under₂ p (⊓)] :
semilattice_inf (subtype p) :=
subtype.semilattice_inf (@subtype.closed_under₂.closed α _ _ _)
```

#### Eric Wieser (Jun 07 2021 at 08:02):

Which means we don't need a different subtype for every combination of inf/sup/top/bot

#### Hunter Monroe (Jun 08 2021 at 18:45):

`borel_space`

used to have `measurable.ennreal_mul`

; what can I use in its place below:

```
def ennreal_measurable_is_submonoid
{Ω:Type*} [MΩ:measurable_space Ω]:
is_submonoid (@measurable Ω ennreal MΩ (borel ennreal)) := {
one_mem :=@measurable_const ennreal Ω (borel ennreal) MΩ 1,
mul_mem :=
begin
intros x y A1 A2,
apply measurable.ennreal_mul A1 A2,
end}
```

#### Eric Wieser (Jun 08 2021 at 19:28):

Is it just docs#measurable.mul?

#### Eric Wieser (Jun 08 2021 at 19:30):

Yes, it is

#### Hunter Monroe (Jun 08 2021 at 21:35):

Perfect, I should have consulted the documentation. Wonder why library_search/!, hint, suggest all missed the proof with one apply. It might be useful to have a deprecation file that proves old results with the new mathlib for each version.

#### Hunter Monroe (Jun 09 2021 at 01:56):

In the first instance defined below for nnreal, there is an error for `const_measurable_fun.has_coe`

"synthesized type class instance is not definitionally equal to expression inferred by typing rules, synthesized nnreal.measurable_space inferred borel nnreal". Note that the second instance for real does not generate an error. I cannot replace `borel nnreal`

with `nnreal.measurable_space`

in the instance definition without creating other errors in subsequent code.

```
import measure_theory.measurable_space
import measure_theory.borel_space
def measurable_fun {α:Type*} {β:Type*} (Mα:measurable_space α) (Mβ:measurable_space β):Type*:=
subtype (@measurable α β _ _)
infixr ` →ₘ `:80 := measurable_fun
lemma const_measurable {Ω:Type*} [measurable_space Ω] {β:Type*} [measurable_space β] (c:β):
(measurable (λ ω:Ω, c)) := measurable_const
def const_measurable_fun {Ω : Type*} [MΩ : measurable_space Ω] {β : Type*}
[Mβ : measurable_space β] (c : β):MΩ →ₘ Mβ :=
{ val := (λ (ω : Ω), c), property := const_measurable c,}
instance const_measurable_fun.has_coe {α:Type*} [M:measurable_space α] {Ω:Type*}
{MΩ:measurable_space Ω}:has_coe α (MΩ →ₘ M) :=
{ coe := (λ (a:α), const_measurable_fun a)}
--noncomputable
instance coe_measurable_fun_of_nnreal
{Ω : Type*} {P:measurable_space Ω}
:has_coe nnreal (measurable_fun P (borel nnreal)) := const_measurable_fun.has_coe
noncomputable instance coe_measurable_fun_of_real
{Ω : Type*} {P:measurable_space Ω}
:has_coe real (measurable_fun P (borel real)) := const_measurable_fun.has_coe
```

#### Heather Macbeth (Jun 09 2021 at 02:34):

What are the errors produced in the subsequent code? It seems like the `measure_space`

instance on `nnreal`

has indeed been changed from the borel construction to the subtype construction, but presumably there was good reason for this.

#### Heather Macbeth (Jun 09 2021 at 02:37):

The change is from #6209 (you can use git blame to track such things down)

#### Heather Macbeth (Jun 09 2021 at 02:40):

Hopefully the instance docs#subtype.borel_space will let you convert from the one construction to the other.

#### Hunter Monroe (Jun 09 2021 at 05:29):

@Heather Macbeth that worked, I just replaced `borel nnreal`

with `nnreal.measurable_space`

throughout the file. This was allow me to define expected value.

#### Hunter Monroe (Jun 09 2021 at 21:27):

@Heather Macbeth I am stuck on what to replace `borel β`

with in the sequence below as `measurable_space β`

does not work. In the instance declaration at the bottom, there is the error `SC_measurable_comm_semiring has type comm_semiring (measurable_fun MΩ (borel nnreal)) but is expected to have type comm_semiring (measurable_fun MΩ nnreal.measurable_space)`

:

```
import measure_theory.measurable_space
import measure_theory.borel_space
import topology.algebra.ring
import formal_ml.real_measurable_space
import formal_ml.semiring
import formal_ml.independent_events
def measurable_fun {α:Type*} {β:Type*} (Mα:measurable_space α) (Mβ:measurable_space β):Type*:=
subtype (@measurable α β _ _)
universes u v
def SC_sum_measurable_is_add_submonoid_from_semiring
{Ω:Type*} [MΩ:measurable_space Ω]
{β:Type*} {T:topological_space β} {SC:topological_space.second_countable_topology β}
{CSR:semiring β} {TA:topological_semiring β}:
is_add_submonoid (@measurable Ω β MΩ (borel β)) :=
(@SC_sum_measurable_is_add_submonoid Ω MΩ β T SC (add_comm_monoid.to_add_monoid β)
(topological_semiring.to_has_continuous_add))
def SC_mul_measurable_is_submonoid_from_semiring
{Ω:Type*} [MΩ:measurable_space Ω]
{β:Type*} {T:topological_space β} {SC:topological_space.second_countable_topology β}
{CSR:semiring β} {TA:topological_semiring β}:
is_submonoid (@measurable Ω β MΩ (borel β)) :=
(@SC_mul_measurable_is_submonoid Ω MΩ β T SC (monoid_with_zero.to_monoid β)
(topological_semiring.to_has_continuous_mul))
def SC_measurable_semiring_is_sub_semiring
{Ω:Type u} [MΩ:measurable_space Ω]
{β:Type v} {T:topological_space β} {SC:topological_space.second_countable_topology β}
{CSR:semiring β} {TA:topological_semiring β}:
is_sub_semiring (@measurable Ω β MΩ (borel β)) := {
..(@SC_sum_measurable_is_add_submonoid_from_semiring Ω MΩ β T SC _ TA),
..(@SC_mul_measurable_is_submonoid_from_semiring Ω MΩ β T SC _ TA),
}
def SC_measurable_comm_semiring
{Ω:Type u} [MΩ:measurable_space Ω]
{β:Type v} {T:topological_space β} {SC:topological_space.second_countable_topology β}
{CSR:comm_semiring β} {TA:topological_semiring β}:
comm_semiring (measurable_fun MΩ ( borel β)):=
@subtype.comm_semiring (Ω → β) _ (@measurable Ω β MΩ (borel β))
(@SC_measurable_semiring_is_sub_semiring Ω MΩ β T SC (comm_semiring.to_semiring β) TA)
instance nnreal_measurable_fun_comm_semiring {Ω:Type*} [MΩ:measurable_space Ω]:
comm_semiring (measurable_fun MΩ (nnreal.measurable_space)):=
@SC_measurable_comm_semiring Ω MΩ nnreal nnreal.topological_space
nnreal.topological_space.second_countable_topology nnreal.comm_semiring
nnreal.topological_semiring
```

#### Heather Macbeth (Jun 09 2021 at 21:38):

@Hunter Monroe Can you please give a #mwe? This depends on a project, `formal_ml`

, which I don't have downloaded.

#### Heather Macbeth (Jun 09 2021 at 21:41):

But, at a guess, instead of constructing all these algebraic structures using `borel β`

, you should assume

```
[topological_space β] [measurable_space β] [borel_space β]
```

#### Heather Macbeth (Jun 09 2021 at 21:42):

This is saying to Lean that, even though the *construction* of the sigma-algebra is not using docs#borel, nonetheless the sigma-algebra which results is equal to the Borel sigma-algebra.

#### Heather Macbeth (Jun 09 2021 at 22:06):

Maybe you want to do something like this:

```
import measure_theory.borel_space
universes u v
def SC_measurable_semiring_is_subsemiring
(Ω : Type*) [measurable_space Ω]
(β : Type*) [topological_space β] [topological_space.second_countable_topology β]
[measurable_space β] [borel_space β] [semiring β] [topological_semiring β] :
subsemiring (Ω → β) :=
{ carrier := {f | measurable f},
one_mem' := @measurable_const _ _ _ _ 1,
mul_mem' := λ f g hf hg, hf.mul hg ,
zero_mem' := @measurable_const _ _ _ _ 0,
add_mem' := λ f g hf hg, hf.add hg }
/-- Measurable functions from `Ω` to `nnreal` are a subsemiring of all functions. -/
noncomputable example {Ω : Type*} [measurable_space Ω] : subsemiring (Ω → nnreal) :=
SC_measurable_semiring_is_subsemiring Ω nnreal
```

#### Hunter Monroe (Jun 09 2021 at 22:19):

OK, here is a 452 line mwe, the question is focused on what to replace `borel`

with in the last two def's (SC_measurable_semiring_is_sub_semiring, SC_measurable_comm_semiring) to avoid the error in the instance at the very end nnreal_measurable_fun_comm_semiring. The repository https://github.com/hmonroe/formal-ml has partial progress in getting formal-ml to work with the latest version of mathlib, which would bring a good chunk of probability theory.

#### Hunter Monroe (Jun 09 2021 at 22:20):

Not sure the attachment came through and I am just looking at your messages. real_random_variable-copy.lean

#### Hunter Monroe (Jun 09 2021 at 22:25):

I think your example nearly works but the instance is looking for `SC_measurable_comm_semiring`

--how would tweak your example?

#### Heather Macbeth (Jun 09 2021 at 22:40):

@Hunter Monroe You don't need to do anything -- it already is a `comm_semiring`

.

```
import measure_theory.borel_space
noncomputable theory
universes u v
def SC_measurable_semiring_is_subsemiring
(Ω : Type*) [measurable_space Ω]
(β : Type*) [topological_space β] [topological_space.second_countable_topology β]
[measurable_space β] [borel_space β] [semiring β] [topological_semiring β] :
subsemiring (Ω → β) :=
{ carrier := {f | measurable f},
one_mem' := @measurable_const _ _ _ _ 1,
mul_mem' := λ f g, measurable.mul,
zero_mem' := @measurable_const _ _ _ _ 0,
add_mem' := λ f g, measurable.add }
/-- Measurable functions from `Ω` to `nnreal` are a subsemiring of all functions. -/
def foo (Ω : Type*) [measurable_space Ω] : subsemiring (Ω → nnreal) :=
SC_measurable_semiring_is_subsemiring Ω nnreal
example {Ω : Type*} [measurable_space Ω] : comm_semiring (foo Ω) := by apply_instance
```

#### Kevin Buzzard (Jun 09 2021 at 22:41):

You can post stuff like this as a gist, it saves people from having to download anything.

I can't help with Borel stuff, but you use loads of `@`

s. A use of `@`

is often an indication that something is wrong -- `@`

s can usually be avoided. For example (line 31):

```
lemma set.preimage_fst_def {α β : Type*} {Bα : set (set α)} :
(set.preimage (prod.fst : α × β → α) '' Bα) =
{U : set (α × β) | ∃ (A : set α) (H : A ∈ Bα), U = set.prod A set.univ} :=
begin
ext, split,
{ rintro ⟨A, hA, rfl⟩,
exact ⟨A, hA, by simp [set.prod]; refl⟩ },
{ rintro ⟨A, hA, rfl⟩,
exact ⟨A, hA, by simp [set.prod]; refl⟩ },
end
```

or

```
lemma measurable_fun_product_measurableh {α β:Type*}
[M1 : measurable_space α] [M2 : measurable_space β]:
prod.measurable_space = M1.comap prod.fst ⊔ M2.comap prod.snd := rfl
```

#### Hunter Monroe (Jun 09 2021 at 23:22):

@Heather Macbeth if I change the name of your def to `SC_measurable_comm_semiring`

, then I get the error `SC_measurable_comm_semiring Ω nnreal term nnreal.comm_semiring has type comm_semiring nnrea but is expected to have type measurable_space nnreal`

. Could you help me fix that?

#### Heather Macbeth (Jun 09 2021 at 23:26):

@Hunter Monroe What is the line that throws the error?

#### Hunter Monroe (Jun 09 2021 at 23:28):

In the instance, there is a red line under `SC_measurable_comm_semiring`

with the error I gave, where I renamed your definition to `SC_measurable_comm_semiring`

.

```
instance nnreal_measurable_fun_comm_semiring {Ω:Type*} [MΩ:measurable_space Ω]:
comm_semiring (measurable_fun MΩ (nnreal.measurable_space)):=
@SC_measurable_comm_semiring Ω MΩ nnreal nnreal.topological_space
nnreal.topological_space.second_countable_topology nnreal.comm_semiring
nnreal.topological_semiring
```

#### Heather Macbeth (Jun 09 2021 at 23:30):

@Hunter Monroe You ought not to need to define this explicitly as an instance! I wrote it as an `example`

to show that Lean can infer it where needed!

#### Heather Macbeth (Jun 09 2021 at 23:31):

What is the first place in the code where the `comm_semiring`

instance is needed? If you can give me that lemma, I can try to reframe the lemma so the `comm_semiring`

instance is inferred automatically.

#### Hunter Monroe (Jun 09 2021 at 23:36):

@Kevin BuzzardThanks for the tip. This is Martin Zinkevich's Formal-ML repository (over 33K lines of it), which I am trying to get to compile in the latest version of mathlib, as a way of learning Lean. Once the code compiles, I will address the @'s among other issues when refactoring for inclusion in mathlib.

#### Hunter Monroe (Jun 09 2021 at 23:49):

@Heather Macbeth one example is below, where commenting out the instance generates a "failed to synthesize instance" error. The refl proof does not go through in any case (any ideas?). If you want to download the repository using the URL above, this is from the real_random_variable.lean file.

```
infixr ` →ₘ `:80 := measurable_fun
@[simp] lemma nnreal_measurable_fun_zero_val_def {Ω:Type*} [MΩ:measurable_space Ω]: (0:MΩ →ₘ (nnreal.measurable_space)).val = 0 := refl
```

#### Eric Wieser (Jun 09 2021 at 23:58):

At a glance, `measurable_fun`

is designed with incorrect argument explicitness

#### Eric Wieser (Jun 10 2021 at 00:01):

I'd expect the two `Type`

s in `()`

not `{}`

, and the two `measurable_space`

s in `[]`

not `()`

.

#### Heather Macbeth (Jun 10 2021 at 00:32):

@Hunter Monroe The simp-lemma you provide doesn't use the commutativity, but here's how I'd do it:

```
import measure_theory.borel_space
noncomputable theory
def measurable_fun
(Ω : Type*) [measurable_space Ω]
(β : Type*) [topological_space β] [topological_space.second_countable_topology β]
[measurable_space β] [borel_space β] [semiring β] [topological_semiring β] :
subsemiring (Ω → β) :=
{ carrier := {f | measurable f},
one_mem' := @measurable_const _ _ _ _ 1,
mul_mem' := λ f g, measurable.mul,
zero_mem' := @measurable_const _ _ _ _ 0,
add_mem' := λ f g, measurable.add }
infixr `→ₘ `:80 := measurable_fun
@[simp] lemma nnreal_measurable_fun_zero_val_def {Ω : Type*} [measurable_space Ω] :
(0 : Ω →ₘ nnreal).val = 0 :=
rfl
-- not needed for anything, but just to check
example {Ω : Type*} [measurable_space Ω] : comm_semiring (Ω →ₘ nnreal) := by apply_instance
```

#### Heather Macbeth (Jun 10 2021 at 01:06):

I should say that what I wrote above is slick for this use case, but it might cause problems down the line if you want `measurable_fun`

to be a monoid when it maps into a monoid, a module when it maps into a module, etc etc.

I think the standard way to get the full suite of algebraic objects (see docs#continuous_map.monoid, docs#bounded_continuous_function.normed_group, docs#measure_theory.ae_eq_fun.monoid) is to define `measurable_fun`

to be the subtype and then equip it with successive algebraic structures by hand. This is fairly close to what you did before but, when docs#borel_space and typeclass inference are used correctly, it doesn't throw errors.

```
import measure_theory.borel_space
noncomputable theory
variables (Ω : Type*) [measurable_space Ω] (β : Type*) [measurable_space β]
def measurable_fun := {f : Ω → β // measurable f}
infixr `→ₘ `:80 := measurable_fun
instance [add_monoid β] [has_measurable_add₂ β] : add_monoid (Ω →ₘ β) :=
{ add := λ f g, ⟨f.1 + g.1, f.2.add g.2⟩,
add_assoc := λ _ _ _, subtype.ext $ add_assoc _ _ _,
zero := ⟨λ _, 0, measurable_const⟩,
zero_add := λ _, subtype.ext $ zero_add _,
add_zero := λ _, subtype.ext $ add_zero _ }
instance [monoid β] [has_measurable_mul₂ β] : monoid (Ω →ₘ β) :=
{ mul := λ f g, ⟨f.1 * g.1, f.2.mul g.2⟩,
mul_assoc := λ _ _ _, subtype.ext $ mul_assoc _ _ _,
one := ⟨λ _, 1, measurable_const⟩,
one_mul := λ _, subtype.ext $ one_mul _,
mul_one := λ _, subtype.ext $ mul_one _ }
instance [topological_space β] [topological_space.second_countable_topology β]
[borel_space β] [semiring β] [topological_semiring β] :
semiring (Ω →ₘ β) :=
{ add_comm := λ _ _, subtype.ext $ add_comm _ _,
zero_mul := λ _, subtype.ext $ zero_mul _,
mul_zero := λ _, subtype.ext $ mul_zero _,
left_distrib := λ _ _ _, subtype.ext $ left_distrib _ _ _,
right_distrib := λ _ _ _, subtype.ext $ right_distrib _ _ _,
.. measurable_fun.add_monoid Ω β,
.. measurable_fun.monoid Ω β }
instance [topological_space β] [topological_space.second_countable_topology β]
[borel_space β] [comm_semiring β] [topological_semiring β] :
comm_semiring (Ω →ₘ β) :=
{ mul_comm := λ _ _, subtype.ext $ mul_comm _ _
.. measurable_fun.semiring Ω β }
@[simp] lemma nnreal_measurable_fun_zero_val_def {Ω : Type*} [measurable_space Ω] :
(0 : Ω →ₘ nnreal).val = 0 :=
rfl
-- not needed for anything, but just to check
example {Ω : Type*} [measurable_space Ω] : comm_semiring (Ω →ₘ nnreal) := by apply_instance
```

#### Eric Wieser (Jun 10 2021 at 06:22):

I have an open PR against mathlib that does precisely that, #7833

#### Hunter Monroe (Jun 12 2021 at 01:48):

@Heather Macbeth How would you suggest adapting the random variable definition to building on your suggestion:

```
import measure_theory.borel_space
noncomputable theory
def measurable_fun
(Ω : Type*) [measurable_space Ω]
(β : Type*) [topological_space β] [topological_space.second_countable_topology β]
[measurable_space β] [borel_space β] [semiring β] [topological_semiring β] :
subsemiring (Ω → β) :=
{ carrier := {f | measurable f},
one_mem' := @measurable_const _ _ _ _ 1,
mul_mem' := λ f g, measurable.mul,
zero_mem' := @measurable_const _ _ _ _ 0,
add_mem' := λ f g, measurable.add }
infixr `→ₘ `:80 := measurable_fun
@[simp] lemma nnreal_measurable_fun_zero_val_def {Ω : Type*} [measurable_space Ω] :
(0 : Ω →ₘ nnreal).val = 0 := rfl
def random_variable' {Ω :Type*} (measurable_space Ω) {β:Type*}
(measurable_space β):Type* := measurable_fun Ω β
infixr ` →ᵣ' `:80 := random_variable'
@[simp] lemma nnreal_random_variable_add_val_def {Ω:Type*}
{measurable_space Ω} {a b:Ω →ᵣ' (nnreal)} : (a + b).val = (a.val + b.val) := rfl
```

#### Heather Macbeth (Jun 12 2021 at 01:52):

@Hunter Monroe I don't know much about probability, sorry.

By the way, it looks like you are defining the semiring structure using the quick-and-dirty method I proposed at first, but since @Eric Wieser has an open PR for a more comprehensive construction, it would be better to merge that in and base your work on that ....

#### Heather Macbeth (Jun 12 2021 at 02:05):

I guess my first thought would be not to use `random_variable`

at all -- just to refer throughout to `measurable_fun`

, or perhaps to make `random_variable`

an `abbreviation`

for `measurable_fun`

. But maybe a probabilist could draw a distinction here that I'm not seeing.

#### Heather Macbeth (Jun 12 2021 at 02:12):

Heather Macbeth said:

I guess my first thought would be not to use

`random_variable`

at all -- just to refer throughout to`measurable_fun`

This seems to be how it's done in, eg, docs#probability_theory.lintegral_mul_eq_lintegral_mul_lintegral_of_indep_fun

#### Hunter Monroe (Jun 12 2021 at 16:48):

@Heather Macbeth good point on random variables. Another question: how should I conjure up a `topological_semiring ennreal`

as required for the def at the end using your method or Eric's new method?

```
import measure_theory.borel_space
noncomputable theory
def measurable_fun
(Ω : Type*) [measurable_space Ω]
(β : Type*) [topological_space β] [topological_space.second_countable_topology β]
[measurable_space β] [borel_space β] [semiring β] [topological_semiring β] :
subsemiring (Ω → β) :=
{ carrier := {f | measurable f},
one_mem' := @measurable_const _ _ _ _ 1,
mul_mem' := λ f g, measurable.mul,
zero_mem' := @measurable_const _ _ _ _ 0,
add_mem' := λ f g, measurable.add }
def nnreal_to_ennreal_measurable_fun:measurable_fun ( nnreal) ( ennreal) := {
val := (λ x:nnreal, (x:ennreal)),
property := nnreal_to_ennreal_measurable,}
```

#### Heather Macbeth (Jun 12 2021 at 16:54):

Actually, I didn't see a `topological_space`

instance for `ennreal`

in mathlib. (Maybe I'm not looking in the right place.). Does anyone know for sure?

#### Mario Carneiro (Jun 12 2021 at 16:55):

There is definitely an instance

#### Rémy Degenne (Jun 12 2021 at 16:56):

docs#ennreal.topological_space

#### Heather Macbeth (Jun 12 2021 at 17:02):

Then maybe what's missing, if it's true, is

```
import topology.algebra.ring
import topology.algebra.ordered.basic
example {α : Type*} [canonically_ordered_comm_semiring α] [topological_space α]
[order_topology α] :
topological_semiring α :=
sorry
```

#### Rémy Degenne (Jun 12 2021 at 17:08):

are you sure that ennreal is a `topological_semiring`

? I am worried about continuity of the multiplication. What do you need that instance for?

#### Mario Carneiro (Jun 12 2021 at 17:13):

can confirm it's not a topological semiring because multiplication is not continuous at (0, infty)

#### Rémy Degenne (Jun 12 2021 at 17:24):

The multiplication is not continuous, but there is docs#ennreal.has_measurable_mul₂ and similar for add etc. All needed properties for the subsemiring definition should be there. Just don't look for continuity, but directly use measurability.

#### Hunter Monroe (Jun 12 2021 at 17:27):

In the original formal-ml repository, commenting out the instance below creates an error in proof of a lemma E[X*Y]=E[X}E[Y} for X, Y independent, nnreal-valued random variables, so the instance is likely not essential for the proof.

```
noncomputable instance ennreal_random_variable_comm_semiring {Ω:Type*} {p:probability_space Ω}: comm_semiring (random_variable p (borel ennreal)):= ennreal_measurable_fun_comm_semiring
```

#### Hunter Monroe (Jun 12 2021 at 17:47):

I need a strategic decision on whether I should continue trying to get formal-ml to compile with current mathlib--which would likely require someone much more experienced with Lean to help me for an hour or so with compile errors prioritizing the files independent_events.lean, real_random_variable, measure, finite_pi_measure, prod_measure, random_variable_identical, and radon_nikodym/dependencies. I could then continue the spadework to modify formal-ml to include key parts in mathlib: definitions of random variable, the expectation operator, and the Radon-Nikodym theorem (the jewel in the crown). This would include factoring out extra definitions for measurablesetB, measurable functions, and any lemmas already in mathlib that I have missed, while using more standard notation. Alternatively, I could create a less ambitious submission of key probability concepts, cribbing from formal-ml without getting formal-ml to compile. The repository I am working in is https://github.com/hmonroe/formal-ml.

#### Eric Wieser (Jun 12 2021 at 17:51):

I thought you got formal-ml to compile already?

#### Rémy Degenne (Jun 12 2021 at 17:55):

I am not following what you are doing with formal-ml closely, but it looks like you would benefit from writing your own code in order to gain familiarity with mathlib, rather than adapting another code which uses quite different conventions. If I were you, I would pick one goal and build towards it from mathlib, not from formal-ml. Although following the general steps of formal-ml would of course help.

The radon-nikodym theorem looks like a fun goal, and it can be written within measure theory: no need for all those events and random variable definitions. Writing theorems is more fun than coming up with definitions.

#### Eric Wieser (Jun 12 2021 at 17:58):

Part of the thing that makes formal-ml awkward is that it contains lots of definitions that are almost-but-not-quite the same as the mathlib ones

#### Kevin Buzzard (Jun 12 2021 at 18:03):

Whilst I don't know anything about how probability theory is set up in either mathlib or formal-ml, I have got a lot of experience with getting lean-beginners to the stage where they can write mathlib-ready code, and I think that an effective way to learn Lean is to do small projects yourself from scratch rather than trying to understand 600 lines of rotting code. I agree with Remy that proving theorems is more fun than making definitions -- making definitions is extremely difficult. To give a pretty solid proof of this, take a look at mathlib's definition of a group, which is nothing like what a beginner would write, it is far far more complicated, for reasons which would be difficult for a beginner to understand. I would recommend short projects which could become mathlib PRs, because the PR process is an effective way of learning.

#### Hunter Monroe (Jun 13 2021 at 01:43):

OK, I have made a pull request for the first 800 or so lines of probability_space also defining events and probability. I switched to standard set notation (union/intersection/complement) for events. https://github.com/leanprover-community/mathlib/pull/7913#partial-pull-merging.

#### Hunter Monroe (Jun 14 2021 at 23:00):

What is the purpose of making `probability_measure`

a class as opposed to for instance a subtype?

```
class probability_measure (μ : measure α) : Prop := (measure_univ : μ univ = 1)
```

#### Heather Macbeth (Jun 14 2021 at 23:04):

Do you mean, a structure rather than a subtype?

#### Heather Macbeth (Jun 14 2021 at 23:10):

Or do you mean, defining it as a `Prop`

rather than as a `measure`

plus a `Prop`

?

#### Hunter Monroe (Jun 14 2021 at 23:26):

Broadly, what are the choices and the design considerations? This would help understand how to build on top of it.

#### Heather Macbeth (Jun 14 2021 at 23:31):

Have you tried making your suggested variation on a clean copy of mathlib, and compiling it to see what breaks?

#### Yakov Pechersky (Jun 14 2021 at 23:51):

Let's say you defined "is_probability_measure mu : Prop := mu univ = 1". Then, you'd likely prove all sorts of things about such measures, having to constantly pass (h : is_probability_measure mu) around. And make definitions that require the hypothesis also. In those lemmas and definitions, you might or might not refer to h. Typeclasses allow you require that hypothesis too, but to also infer them form the context. Often, you won't care exactly about h, but lemmas derived from it. And typeclasses will make it much easier to defer to those. The same way that add_le_add doesn't require you to pass a proof of the order.

#### Hunter Monroe (Jun 16 2021 at 16:44):

The definition of `ite`

has changed so as to break this lemma statement, with error `type mismatch at application ite (classical.prop_decidable (s = ∅)) term classical.prop_decidable (s = ∅) has type decidable (s = ∅) but is expected to have type Prop`

. Can someone suggest a fix?

```
import measure_theory.measurable_space
import measure_theory.measure_space
lemma measure_theory.outer_measure.top_eq {Ω:Type*} [M:measurable_space Ω]:
⇑(⊤:measure_theory.outer_measure Ω) = (λ (s:set Ω), (@ite (s=∅) (classical.prop_decidable (s=∅)) ennreal 0 ⊤)) := sorry
```

#### Horatiu Cheval (Jun 16 2021 at 16:53):

The right order of the arguments seems to be different:

```
lemma measure_theory.outer_measure.top_eq {Ω:Type*} [M:measurable_space Ω]:
⇑(⊤:measure_theory.outer_measure Ω) = (λ (s:set Ω), (@ite ennreal (s=∅) (classical.prop_decidable (s=∅)) 0 ⊤)) := sorry
```

#### Eric Wieser (Jun 16 2021 at 16:55):

You shouldn't be using `@`

there in the first place

#### Eric Wieser (Jun 16 2021 at 16:58):

Adding `[decidable_pred (λ s : set Ω, s = ∅)]`

as an argument removes the need for the `@`

and results in a slightly more general lemma

#### Hunter Monroe (Jun 16 2021 at 17:35):

@Eric Wieser sorry but how do I get rid of the @? I could not find a variation that worked.

lemma measure_theory.outer_measure.top_eq {Ω:Type*} [M:measurable_space Ω] [decidable_pred (λ s : set Ω, s = ∅)]:

⇑(⊤:measure_theory.outer_measure Ω) = ( λ s, (@ite ennreal (s=∅) (classical.prop_decidable (s=∅)) 0 ⊤)) := sorry

#### Rémy Degenne (Jun 16 2021 at 17:39):

```
lemma measure_theory.outer_measure.top_eq {Ω : Type*} [M : measurable_space Ω]
[decidable_pred (λ s : set Ω, s = ∅)] :
⇑(⊤ : measure_theory.outer_measure Ω) = λ s, ite (s = ∅) (0 : ℝ≥0∞) ⊤ :=
sorry
```

you have to give a hint about the type of either 0 or top in the ite

#### Rémy Degenne (Jun 16 2021 at 17:41):

by the way, the standard notation for `⊤`

in ennreal (`ℝ≥0∞`

) is `∞`

#### Hunter Monroe (Jun 16 2021 at 17:57):

The Lebesgue Radon Nikodym Theorem, as extracted from formal-ml, now compiles under the current version of mathlib!!! I have a lot of work to clean it up before submitting to mathlib.

#### Hunter Monroe (Jun 21 2021 at 19:35):

The proof below works for nnreal, but I not for ennreal, where my proof required three cases statements. Am I missing something, and more generally is there a generic way to move nnreal results to ennreal where correct?

```
import data.real.nnreal
example {a b c:nnreal}: b ≤ c → ∀ a,a + b ≤ a + c := add_le_add_left
```

#### Rémy Degenne (Jun 21 2021 at 19:40):

I opened it in the online lean editor and it works fine for ennreal.

```
import data.real.ennreal
example {a b c : ennreal} : b ≤ c → ∀ a, a + b ≤ a + c := add_le_add_left
```

Is your local mathlib up to date?

#### Hunter Monroe (Jun 22 2021 at 02:23):

How can I apply `div_le_div_right`

here? The error message is not clear: `type mismatch at application div_le_div_right h₅ term h₅ has type 0 < ↑(q.denom) but is expected to have type 0 < ?m_3`

```
import data.rat
lemma rat.exists_unit_frac_le_pos {q:ℚ}:0 < q → (∃ n:ℕ, (1/((n:rat) + 1)) ≤ q) :=
begin
have h₄ : q.denom > 0 := by exact q.pos,
have h₅ : 0 < (↑(q.denom)) := by exact nat.cast_pos.mpr h₄,
have h₇ : (1:ℤ) / (↑(q.denom)) ≤ (↑(q.num) / ↑(q.denom) :=
begin
apply div_le_div_right h₅ (↑(q.denom)),
end
```

#### Heather Macbeth (Jun 22 2021 at 02:44):

Do you know about `norm_cast`

, etc?

```
import data.rat
lemma rat.exists_unit_frac_le_pos {q:ℚ} : 0 < q → (∃ n:ℕ, (1/((n:ℚ) + 1)) ≤ q) :=
begin
intros h,
have h₅ : 0 < (q.denom : ℚ) := by exact_mod_cast q.pos,
have h₇ : (1:ℚ) / q.denom ≤ (q.num : ℚ) / q.denom,
{ rw div_le_div_right h₅,
exact_mod_cast rat.num_pos_iff_pos.mpr h },
end
```

#### Heather Macbeth (Jun 22 2021 at 02:50):

I didn't check out your version in a full-featured editor, but my guess is that you should have provided explicit casts to `ℚ`

in place of some of the `↑`

.

#### Heather Macbeth (Jun 22 2021 at 02:54):

Also, have you seen that the fact you want is a lemma in mathlib? docs#exists_nat_one_div_lt

#### Hunter Monroe (Jun 22 2021 at 04:09):

Cool thanks.

#### Hunter Monroe (Jun 22 2021 at 17:38):

How can I prove the equivalence below (nnreal replaced with real). I tried `norm_cast`

and `real.to_nnreal_mono`

.

```
import data.real.nnreal
example {ε:nnreal} {n':ℕ }:0 < ε → (1 / ((n':real) + 1) < (ε:real) ↔ 1 / ((n':nnreal) + 1) < ε):= sorry
```

As background, I am trying to prove versions of the following but for nnreal and ennreal, and more generally transfer over results about reals..

```
lemma real.exists_unit_frac_lt_pos {ε:real}:0 < ε → (∃ n:ℕ, (1/((n:real) + 1)) < ε) := exists_nat_one_div_lt
```

#### Ruben Van de Velde (Jun 22 2021 at 18:20):

This works, through the magic of `simp`

:

```
import data.real.nnreal
example {ε:nnreal} {n':ℕ }:0 < ε → (1 / ((n':real) + 1) < (ε:real) ↔ 1 / ((n':nnreal) + 1) < ε):= by {
intro h,
rw ←nnreal.coe_lt_coe,
split;
{ intro H,
convert H using 1,
simp },
}
```

#### Kalle Kytölä (Jun 30 2021 at 02:22):

I'll just post also here a link to an exercise I did on weak convergence of probability measures and Portmanteau's theorem: #new members > Portmanteau theorem.

#### Hunter Monroe (Jul 11 2021 at 15:04):

I would like the statement of the existing theorem below to be `E[f*g]=E[f]*E[g]`

but I am getting the error `don't know how to synthesize placeholder`

. See a mwe below. Note this works in formal-ml but is such an elaborate approach needed?

```
import measure_theory.integration
import probability_theory.independence
noncomputable theory
open measure_theory
open_locale ennreal
variables {α : Type*}
namespace probability_theory
def expected_value [M : measurable_space α] {μ : measure α} (X : α → ℝ≥0∞)
:= ∫⁻ a, X a ∂μ
notation `E[` X `]`:= expected_value X
/-- This (roughly) proves that if `f` and `g` are independent random variables,
then `E[f * g] = E[f] * E[g]`.-/
lemma lintegral_mul_eq_lintegral_mul_lintegral_of_independent_measurable_space
{Mf : measurable_space α} {Mg : measurable_space α} [M : measurable_space α]
{μ : measure α} (hMf : Mf ≤ M) (hMg : Mg ≤ M) (h_ind : indep Mf Mg μ)
(f g : α → ℝ≥0∞) (h_meas_f : @measurable α ℝ≥0∞ Mf _ f)
(h_meas_g : @measurable α ℝ≥0∞ Mg _ g) :
∫⁻ a, f a * g a ∂μ = ∫⁻ a, f a ∂μ * ∫⁻ a, g a ∂μ :=sorry
end probability_theory
```

#### Eric Wieser (Jul 11 2021 at 15:08):

Your problem is that lean can't work out `μ`

from the notation

#### Eric Wieser (Jul 11 2021 at 15:10):

One way to resolve this would be to use docs#measure_space instead of docs#measurable_space, and the canonical `volume`

measure in place of `μ`

#### Hunter Monroe (Jul 11 2021 at 15:35):

I tried that below, replacing `μ`

with `Mf.volume`

and `Mg.volume`

, creating new definitions for `measurable`

and `indep`

based on `measure_space`

not `measurable_space`

, and now have multiple type class instance errors. Presumably I would need to rewrite the statements and proofs in integration.lean as well. Even simple changes seem to blow up in this area.

```
import measure_theory.integration
import probability_theory.independence
noncomputable theory
open measure_theory
open_locale ennreal
variables {α β : Type*}
namespace probability_theory
def expected_value [M : measure_space α] {μ : measure α} (X : α → ℝ≥0∞)
:= ∫⁻ a, X a ∂μ
notation `E[` X `]`:= expected_value X
def indep' {α} (m₁ m₂ : measure_space α) [measure_space α] (μ : measure α . volume_tac) :
Prop := indep_sets (m₁.measurable_set') (m₂.measurable_set') μ
def measurable' [measure_space α] [measure_space β] (f : α → β) : Prop :=
∀ ⦃t : set β⦄, measurable_set t → measurable_set (f ⁻¹' t)
/-- This (roughly) proves that if `f` and `g` are independent random variables,
then `E[f * g] = E[f] * E[g]`.-/
lemma lintegral_mul_eq_lintegral_mul_lintegral_of_independent_measurable_space
{Mf : measure_space α} {Mg : measure_space α} [M : measure_space α]
(hMf : Mf ≤ M) (hMg : Mg ≤ M) (h_ind : indep' Mf Mg μ)
(f g : α → ℝ≥0∞) (h_meas_f : @measurable' α ℝ≥0∞ Mf _ f)
(h_meas_g : @measurable' α ℝ≥0∞ Mg _ g) :
∫⁻ a, f a * g a ∂(Mf.volume) = ∫⁻ a, f a ∂(Mf.volume) * ∫⁻ a, g a ∂(Mf.volume) :=sorry
end probability_theory
```

#### Eric Wieser (Jul 11 2021 at 15:36):

Wait, I think I don't understand what you meant by

I would like the statement of the existing theorem below to be

`E[f*g]=E[f]*E[g]`

Can you provide the things you tried that didn't work?

#### Eric Wieser (Jul 11 2021 at 15:37):

Or are you saying you want the statement you posted to be shown using that notation, but you don't actually want to restate it?

#### Hunter Monroe (Jul 11 2021 at 15:43):

The broader goal is to introduce the expected value operator E[...], while the narrow goal is to rewrite that lemma to read: `lemma lintegral_mul_eq_lintegral_mul_lintegral_of_independent_measurable_space... : E[f*g]=E[f]*E[g] :=...`

#### Hunter Monroe (Jul 11 2021 at 15:47):

The first thing that did not work was my mwe above, but with `E[f*g]=E[f]*E[g]`

as the thing to be proved. That is, replacing `∫⁻ a, f a ∂μ`

with `E[f]`

.

#### Eric Wieser (Jul 11 2021 at 15:48):

In that case, please include in your #mwe both the version that does work *and* the version that doesn't work!

#### Eric Wieser (Jul 11 2021 at 15:48):

Don't make us try to guess what the non-working version was.

#### Hunter Monroe (Jul 11 2021 at 15:52):

Here is the nonworking mwe:

```
import measure_theory.integration
import probability_theory.independence
noncomputable theory
open measure_theory
open_locale ennreal
variables {α : Type*}
namespace probability_theory
def expected_value [M : measurable_space α] {μ : measure α} (X : α → ℝ≥0∞)
:= ∫⁻ a, X a ∂μ
notation `E[` X `]`:= expected_value X
/-- This (roughly) proves that if `f` and `g` are independent random variables,
then `E[f * g] = E[f] * E[g]`.-/
lemma lintegral_mul_eq_lintegral_mul_lintegral_of_independent_measurable_space
{Mf : measurable_space α} {Mg : measurable_space α} [M : measurable_space α]
{μ : measure α} (hMf : Mf ≤ M) (hMg : Mg ≤ M) (h_ind : indep Mf Mg μ)
(f g : α → ℝ≥0∞) (h_meas_f : @measurable α ℝ≥0∞ Mf _ f)
(h_meas_g : @measurable α ℝ≥0∞ Mg _ g) :
E[f*g]=E[f]*E[g] :=sorry
end probability_theory
```

#### Eric Wieser (Jul 11 2021 at 16:08):

This works:

```
import measure_theory.integration
import probability_theory.independence
open measure_theory
open_locale ennreal
variables {α : Type*}
namespace probability_theory
def expected_value [M : measure_space α] (X : α → ℝ≥0∞) := ∫⁻ a, X a ∂(volume)
notation `E[` X `]`:= expected_value X
/-- This (roughly) proves that if `f` and `g` are independent random variables,
then `E[f * g] = E[f] * E[g]`.-/
lemma lintegral_mul_eq_lintegral_mul_lintegral_of_independent_measurable_space
{Mf : measurable_space α} {Mg : measurable_space α} [M : measure_space α]
{μ : measure α} (hMf : Mf ≤ measure_space.to_measurable_space)
(hMg : Mg ≤ measure_space.to_measurable_space)
(h_ind : @indep _ Mf Mg measure_space.to_measurable_space (volume))
(f g : α → ℝ≥0∞) (h_meas_f : @measurable α ℝ≥0∞ Mf _ f)
(h_meas_g : @measurable α ℝ≥0∞ Mg _ g) :
E[f*g]=E[f]*E[g] :=sorry
end probability_theory
```

#### Eric Wieser (Jul 11 2021 at 16:09):

I think either you're working with this API in the wrong way, or this API isn't well thought out - the problem with this lemma is that `measurable_space`

is a typeclass, but this lemma is talking about three different instances of the same typeclass, meaning you needs `@`

s everywhere to be clear which one of the three you care about

#### Hunter Monroe (Jul 11 2021 at 16:46):

Fantastic. My aim is to rewrite integration.lean so the conclusions have the form `E[f*g]=E[f]*E[g]`

and can serve as a building block for probability theory. Are you suggesting that the lemma should be stated differently? The next lemma matters more, but uses this lemma:

```
/-- This proves that if `f` and `g` are independent random variables, then `E[f * g] = E[f] * E[g]`. -/
lemma lintegral_mul_eq_lintegral_mul_lintegral_of_indep_fun [M : measurable_space α]
(μ : measure α) (f g : α → ℝ≥0∞) (h_meas_f : measurable f) (h_meas_g : measurable g)
(h_indep_fun : indep_fun (borel ennreal) (borel ennreal) f g μ) :
∫⁻ (a : α), (f * g) a ∂μ = ∫⁻ (a : α), f a ∂μ * ∫⁻ (a : α), g a ∂μ
```

#### Kevin Buzzard (Jul 11 2021 at 16:52):

Eric is simply saying that `measurable_space`

has been designed with the idea in mind that any type should have at most one measurable space structure, and in your lemma you're putting two measurable space structures on alpha. Typeclasses are not designed to do this.

#### Hunter Monroe (Jul 11 2021 at 17:08):

Ok thanks (it is not my lemma but the one in mathlib that needs tuning up).

#### Patrick Massot (Jul 11 2021 at 17:11):

Hunter Monroe said:

My aim is to rewrite integration.lean so the conclusions have the form

`E[f*g]=E[f]*E[g]`

and can serve as a building block for probability theory.

What do you mean? We certainly don't want the integration files to be polluted with probabilistic notation. Do you mean you want to duplicate `integration.lean`

in some new file with different notations?

#### Eric Wieser (Jul 11 2021 at 17:30):

@Kevin Buzzard, I get the feeling that the lemma statement using the original notation is part of mathlib, and that there are lots of places in the measure theory library where two different measurable_space instances are put on the same type.

#### Hunter Monroe (Jul 12 2021 at 04:16):

@Patrick Massot the whole point of the file integration.lean under probability_theory according to the doc strings is to show that for independent random variables `E[f*g]=E[f]*E[g]`

, but then the theorems themselves did not use that notation.

Patrick Massot said:

What do you mean? We certainly don't want the integration files to be polluted with probabilistic notation. Do you mean you want to duplicate

`integration.lean`

in some new file with different notations?

#### Jason KY. (Jul 13 2021 at 12:40):

@Hunter Monroe I just saw this thread and I see that you are working on porting formal-ml to mathlib. I just wanted to say that I have Radon-Nikodym proved through the signed measure rout here: https://github.com/JasonKYi/probability_theory/blob/main/src/singular.lean#L479

#### Sebastien Gouezel (Jul 13 2021 at 12:45):

Radon-Nikodym even works for sigma-finite measures, as you know probably, but the hard part is the part for finite measures that you have done. Very nice! Even more motivation for me to review #8247 :-)

#### Jason KY. (Jul 13 2021 at 12:46):

I do plan to work on generalizing to sigma-finiteness later this week :)

#### Sebastien Gouezel (Jul 13 2021 at 12:55):

Awesome. Review done (well, I stopped after a few lines, because there is something I don't understand :-)

#### Jason KY. (Jul 13 2021 at 13:17):

I've now removed the extra `R`

. Certainly a surprise that a vector measures doesn't require a vector space!

#### Hunter Monroe (Jul 13 2021 at 14:23):

That is great. The Hahn decomposition theorem is already in measure_theory/decomposition--you may be introducing a duplicate version in your hahn.lean file. Note that formal-ml was not well integrated with mathlib with duplicates of many results, including its own proof of the Hahn decomposition theorem. I am no longer trying to bring formal-ml up to date with the latest mathlib, but am still working on key probability theorems, in some cases comparing against formal-ml.

Jason KY. said:

Hunter Monroe I just saw this thread and I see that you are working on porting formal-ml to mathlib. I just wanted to say that I have Radon-Nikodym proved through the signed measure rout here: https://github.com/JasonKYi/probability_theory/blob/main/src/singular.lean#L479

#### Hunter Monroe (Jul 13 2021 at 14:26):

My immediate priority is Borel-Cantelli (other direction) and basic expectation/variance results.

#### Jason KY. (Jul 13 2021 at 14:34):

Hunter Monroe said:

The Hahn decomposition theorem is already in measure_theory/decomposition--you may be introducing a duplicate version in your hahn.lean file.

The one in mathlib right now is the non-signed version while the one in mine repo is the signed version :)

#### Damiano Testa (Jul 13 2021 at 14:57):

(deleted)

#### Hunter Monroe (Jul 13 2021 at 15:00):

Good point, so you will do another PR with Radon-Nikodym and Hahn?

#### Jason KY. (Jul 13 2021 at 15:04):

Right, I will need the signed version of Hahn for Radon-Nikodym

#### Hunter Monroe (Aug 16 2021 at 23:31):

@Jason KY. have you done a PR for Radon-Nikodym?

#### Jason KY. (Aug 16 2021 at 23:48):

Radon-Nikodym should come right after #8687 :grinning:

#### Daniil Homza (Aug 22 2022 at 12:50):

Hi everyone!

I am a new member of Lean community.

For now I try to proof "Weak Law of Large Number".

I am confused on the following problem

"

How to defined all set of form {1}, {1,2}, {1,2,3}.... and say something like there exists N such that \forall n>N \sum_{i=1}^n .......

"

Can someone help with this?

Thank you in advance:)

#### Johan Commelin (Aug 22 2022 at 13:05):

Does docs#fin and/or docs#finset.range help?

#### Johan Commelin (Aug 22 2022 at 13:05):

See also docs#finset.sum.

#### Daniil Homza (Sep 14 2022 at 08:32):

Hi Lean Community,

I have some easy question to solve but I can not get it. I am interesting to proof that expected value of m r.v. is sum of m expected value of r.v. I can not find such result of summarising of two integrals in section measure_theory. Actually i have problem even in case of such result in case of two r.v. Any Help? Thanks in advance 123.PNG

#### Rémy Degenne (Sep 14 2022 at 08:36):

Hi! Helping you would be easier if you posted code instead of a picture, ideally in the form of an #mwe . But it looks like the lemma you are looking for is docs#measure_theory.integral_finset_sum

#### Rémy Degenne (Sep 14 2022 at 08:37):

for two random variables it would be docs#measure_theory.integral_add

#### Daniil Homza (Sep 14 2022 at 08:59):

o, yep, i think is that i am looking for. Sorry for picture) Thank you!

#### Joshua Banks (Feb 22 2023 at 20:02):

Does anyone have a tips for how I could go about proving this lemma? new to lean and this seems simple but struggling to formulate anything.

```
lemma sum_to_one (a : ℝ) (X : Ω → ℝ) (μ : measure Ω) [is_probability_measure μ] : μ(λx , X x > a) + μ(λx, X x <= a) = 1 :=
begin
sorry,
end
```

#### Eric Wieser (Feb 22 2023 at 20:03):

Instead of pasting an image, can you paste the code (with imports) in #backticks?

#### Joshua Banks (Feb 22 2023 at 20:07):

thank you I have changed it, still new to all this :+1:

#### Kevin Buzzard (Feb 22 2023 at 20:11):

Adding the imports to make it a #mwe is the perfect way to ask this kind of question (you can just edit the original post)

#### Kevin Buzzard (Feb 22 2023 at 20:13):

And by "tips" will you accept solutions or do you actively want to avoid being told the answer?

#### Eric Wieser (Feb 22 2023 at 20:13):

Note that the canonical way to use docs#measure_theory.measure is with sets, not lambdas; so

`μ {x | X x > a} + μ { x | X x <= a}`

not `μ(λx , X x > a) + μ(λx, X x <= a)`

#### Kevin Buzzard (Feb 22 2023 at 20:15):

I've never used the measure theory seriously library but here's my guess as to how to go about this: first locate the theorem saying measure of union of two disjoint sets is sum of measures, then invoke theorem saying measure of everything is 1, then prove that the two sets are disjoint and their union is the reals.

#### Eric Wieser (Feb 22 2023 at 20:16):

docs#measure_theory.measure_union is the first theorem Kevin mentions

#### Kevin Buzzard (Feb 22 2023 at 20:16):

These things will be called things like measure_union and measure_univ

#### Joshua Banks (Feb 22 2023 at 20:24):

Kevin Buzzard said:

And by "tips" will you accept solutions or do you actively want to avoid being told the answer?

I wouldn't mind being given maybe part of the answer and then continue to try finish it myself if anyone has any suggestions

#### Kevin Buzzard (Feb 22 2023 at 20:46):

Well start by rewriting the theorem Eric suggested! (backwards) And you'd be better off stating the theorem without lambdaa

#### Alistair Tucker (Feb 22 2023 at 21:11):

I think you'll want to assume X measurable

#### Alistair Tucker (Feb 22 2023 at 21:29):

Well you can prove an inequality without.

```
lemma one_le_sum (a : ℝ) (X : Ω → ℝ) (μ : measure Ω) [is_probability_measure μ] :
1 ≤ μ {ω | a < X ω} + μ {ω | X ω ≤ a} :=
calc 1
= μ set.univ : by rw measure_univ
... ≤ μ ({ω | a < X ω} ∪ {ω | X ω ≤ a}) : by {apply measure_mono, intros ω hω, simp [lt_or_ge], }
... ≤ μ {ω | a < X ω} + μ {ω | X ω ≤ a} : by apply measure_union_le
```

#### Eric Wieser (Feb 22 2023 at 23:16):

The first `≤`

is true as an `=`

there too

#### Joshua Banks (Feb 23 2023 at 14:02):

Thank you everyone for your help with this it has been very informative and useful for someone trying to learn

#### Joshua Banks (Feb 23 2023 at 14:04):

I am having trouble applying measure_univ in this example, having used measure_union to put into the correct form I am struggling to invoke the theorem in this example,

I currently have

```
lemma sum_to_one (a : ℝ) (X : Ω → ℝ) (μ : measure Ω) [is_probability_measure μ] [measurable X]: μ {ω | X ω > a} + μ {ω | X ω ≤ a} = 1 :=
begin
rw measure_union_reverse,
end
```

and this gives me

Image-23-02-2023-at-14.00.jpeg

any help on how I can continue from here would be appreciated

#### Eric Wieser (Feb 23 2023 at 15:01):

`convert measure_univ`

will likely make that first goal clearer

#### Kevin Buzzard (Feb 23 2023 at 22:31):

To solve a goal like `disjoint X Y`

just right click on disjoint and see how the library designers are proving such goals. Is it definitionally equal to "the intersection is empty" or do you have to do some work to get to this state, for example

#### Eric Wieser (Feb 23 2023 at 22:47):

(I changed the definition of src#disjoint recently so it's even weirder than that, I'm afraid)

#### Joshua Banks (Feb 23 2023 at 23:24):

Thanks for your help it’s really good for me to understand how a proof like this works however I’m still struggling to complete the first goal despite it seeming like something quite simple

#### Alistair Tucker (Feb 23 2023 at 23:31):

Maybe this template will help.

```
lemma sum_to_one (a : ℝ) (X : Ω → ℝ) (μ : measure Ω) [is_probability_measure μ]
(hm : measurable X) : μ {ω | a < X ω} + μ {ω | X ω ≤ a} = 1 :=
calc μ {ω | a < X ω} + μ {ω | X ω ≤ a} = μ ({ω | a < X ω} ∪ {ω | X ω ≤ a}) : by
{ rw [measure_union],
{ rw [disjoint_iff],
sorry, },
{ sorry, }, }
... = μ set.univ : by
{ congr,
ext ω,
sorry, }
... = 1 : measure_univ
```

#### Joshua Banks (Feb 24 2023 at 12:30):

thank you this was very helpful and have now been able to complete the lemma

#### Notification Bot (Feb 24 2023 at 12:30):

Joshua Banks has marked this topic as resolved.

#### Notification Bot (Feb 24 2023 at 12:30):

Joshua Banks has marked this topic as resolved.

#### Notification Bot (Feb 24 2023 at 12:30):

Joshua Banks has marked this topic as unresolved.

#### Joshua Banks (Feb 26 2023 at 21:35):

Hi, I was wondering if anyone had any idea about how to go about phrasing this lemma in lean as I understand that normal distribution has not been fully defined in mathlib as of yet. However, maybe this factor may not affect the result and could be excluded.

This lemma defines X as a random variable that is normally distributed with mean and variance.

Image-26-02-2023-at-21.34.jpeg

Any help or advice on this would be much appreciated

#### Martin Dvořák (Feb 26 2023 at 21:36):

[oic now]

#### Alistair Tucker (Feb 27 2023 at 01:16):

If you were happy to work with characteristic functions from the outset, then something like this might work

```
import probability.notation
open complex
open_locale matrix probability_theory
variables {Ω : Type*} [measurable_space Ω]
def Y (X : Ω → fin 2 → ℝ) : Ω → fin 2 → ℝ := fun ω, !![1, 1; 1, -1].mul_vec (X ω)
variables (ν : measure_theory.measure Ω) (σ_sq : ℝ)
def iid_norm (Z : Ω → fin 2 → ℝ) : Prop :=
∀ (a : fin 2 → ℝ), ν [fun ω, exp (I * (a ⬝ᵥ Z ω : ℝ))] = exp (-σ_sq / 2 * (a ⬝ᵥ a : ℝ))
theorem lem_2_3 (X : Ω → fin 2 → ℝ) (hX : iid_norm ν σ_sq X) : iid_norm ν (2 * σ_sq) (Y X) :=
sorry
```

#### Eric Wieser (Feb 27 2023 at 01:50):

I think `!![σ_sq, 0; 0, σ_sq].mul_vec a`

there is just a weird way to spell `σ_sq • a`

#### Alistair Tucker (Feb 27 2023 at 02:15):

Well the `0`

s are there to indicate independence!

#### Alistair Tucker (Feb 27 2023 at 02:17):

Edited :smile:.

#### Joshua Banks (Feb 27 2023 at 21:54):

Thank you so much for your response that is really helpful to me, I was wondering if you might be able to explain the definition of Y in your example, as I'm not sure I fully understand how that works. @Alistair Tucker

#### Alistair Tucker (Feb 27 2023 at 23:35):

So this uses a special notation for docs#matrix that was new to me as well. It's declared and documented in data/matrix/notation.lean. Here the idea is to define `Y`

so that $Y_{1}=X_{1}+X_{2}$ and $Y_{2}=X_{1}-X_{2}$.

#### Alistair Tucker (Feb 27 2023 at 23:38):

But I don't know if this approach is going to help you with the particular proof you want to formalise.

#### Dongheng Chen (Jun 20 2023 at 08:54):

Dear all,

I am a master's student at Zhejiang University specializing in mathematical logic working with Bruno Bentzen. I am interested in Probability Theory since my undergraduate studies in Pure and Applied Mathematics. I am interested in formalization work in Lean. I noticed some theorems in probability theory are missing in mathlib. For example, the Central Limit Theorem.

I would like to know if somebody is or has already worked on the Martingale Convergence Theorem? Besides, does anybody have any suggestions on places where I might get started? Any help would be greatly appreciated.

#### Rémy Degenne (Jun 20 2023 at 08:57):

Welcome!

You can find several martingale convergence theorems (almost everywhere, L1) here: https://leanprover-community.github.io/mathlib_docs/probability/martingale/convergence.html

We don't have the central limit theorem yet.

#### Rémy Degenne (Jun 20 2023 at 08:59):

To get an idea of what we have about probability, you can browse the files in the probability folder of the docs (see the link above)

Last updated: Dec 20 2023 at 11:08 UTC