Probability theory

Stream: new members

[Kalle Kytölä]

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]

(I've renamed the thread.)

[Bryan Gin-ge Chen]

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

[Greg Price]

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]

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]

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]

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

[Hunter Monroe]

@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]

That's what I just said

[Mario Carneiro]

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]

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

[Mario Carneiro]

but you can have constructors for both versions

[Eric Wieser]

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]

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

[Scott Morrison]

Or simply fork.

[Hunter Monroe]

@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]

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]

• I don't think you should even be writing volume.measure_of x - the canonical spelling should be volume x

[Eric Wieser]

• Instead of {Ω : Type*} {P : probability_space Ω} (X : event P) you probably want {Ω : Type*} [probability_space Ω] (X : event Ω)

[Eric Wieser]

@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]

@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]

See my edited message

[Eric Wieser]

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

[Eric Wieser]

Then your lemmas below become something like:

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

[Eric Wieser]

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]

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]

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]

To me it seems the key change being proposed by this code is "a bundled version ofmeasurable_set would be useful"

[Eric Wieser]

Along with lots of noise duplicating API

[Eric Wieser]

I made a PR providing some instances in #7702

[Sebastien Gouezel]

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]

docs#measure_theory.probability_measure seems not to exist

[Eric Wieser]

Presumably [probability_measure (volume : measure_theory.measure α)] would also work? (and be a direct substitution for the typeclass Hunter is proposing)

[Sebastien Gouezel]

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

[Sebastien Gouezel]

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]

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]

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]

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]

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]

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]

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]

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]

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ä]

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 ennreals and either nnreals 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]

@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]

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]

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]

@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]

Line 70 is better with measurable_space

[Eric Wieser]

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]

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

[Eric Wieser]

Line 210: has_emptyc_event already exists, it's docs#measurable_set.subtype.has_emptyc.

[Eric Wieser]

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

[Eric Wieser]

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]

(deleted)

[Hunter Monroe]

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]

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]

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

[Eric Wieser]

Nice job on getting it passing, anyway!

[Hunter Monroe]

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]

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

[Mario Carneiro]

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]

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

[Scott Morrison]

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]

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]

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]

#backticks / #mwe

[Scott Morrison]

In front of def event write @[derive has_emptyc].

[Scott Morrison]

This is how you copy instances to a type synonym.

[Hunter Monroe]

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]

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]

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

[Scott Morrison]

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]

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

[Hunter Monroe]

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]

Put a return after the ``` , or else it will eat the first line of the code block and not syntax highlight it

[Scott Morrison]

(Put a newline after the initial three backticks.)

[Mario Carneiro]

also before the final ``` , or else it will show up at the end of the code block

[Scott Morrison]

rfl?

[Hunter Monroe]

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

[Scott Morrison]

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]

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]

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]

I deleted it on purpose. :-)

[Eric Wieser]

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]

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]

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]

So why not make event, which is defined as that, reducible?

[Eric Wieser]

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

[Hunter Monroe]

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]

I don't understand your question. Doesn't it have type event Ω already in your code block?

[Scott Morrison]

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]

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]

With the boolean_algebra structure, event_univ is ⊤.

[Hunter Monroe]

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]

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]

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]

(⊤ : 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]

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]

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]

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]

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]

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]

Yes, having sublattices in some form would help here

[Rémy Degenne]

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

[Eric Wieser]

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]

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

[Hunter Monroe]

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]

Is it just docs#measurable.mul?

[Eric Wieser]

Yes, it is

[Hunter Monroe]

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]

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]

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]

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

[Heather Macbeth]

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

[Hunter Monroe]

@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]

@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]

@Hunter Monroe Can you please give a #mwe? This depends on a project, formal_ml, which I don't have downloaded.

[Heather Macbeth]

But, at a guess, instead of constructing all these algebraic structures using borel β, you should assume

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

[Heather Macbeth]

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]

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]

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]

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

[Hunter Monroe]

I think your example nearly works but the instance is looking for SC_measurable_comm_semiring--how would tweak your example?

[Heather Macbeth]

@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]

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]

@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]

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

[Hunter Monroe]

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]

@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]

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]

@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]

@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]

At a glance, measurable_fun is designed with incorrect argument explicitness

[Eric Wieser]

I'd expect the two Types in () not {}, and the two measurable_spaces in [] not ().

[Heather Macbeth]

@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]

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]

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

[Hunter Monroe]

@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]

@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]

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]

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]

@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]

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]

There is definitely an instance

[Rémy Degenne]

docs#ennreal.topological_space

[Heather Macbeth]

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]

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]

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

[Rémy Degenne]

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]

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]

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]

I thought you got formal-ml to compile already?

[Rémy Degenne]

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]

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]

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]

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]

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]

Do you mean, a structure rather than a subtype?

[Heather Macbeth]

Or do you mean, defining it as a Prop rather than as a measure plus a Prop?

[Hunter Monroe]

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

[Heather Macbeth]

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

[Yakov Pechersky]

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]

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]

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]

You shouldn't be using @ there in the first place

[Eric Wieser]

Adding [decidable_pred (λ s : set Ω, s = ∅)] as an argument removes the need for the @ and results in a slightly more general lemma

[Hunter Monroe]

@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]

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]

by the way, the standard notation for ⊤ in ennreal (ℝ≥0∞) is ∞

[Hunter Monroe]

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]

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]

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]

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]

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]

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]

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

[Hunter Monroe]

Cool thanks.

[Hunter Monroe]

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]

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ä]

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]

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]

Your problem is that lean can't work out μ from the notation

[Eric Wieser]

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]

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]

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]

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]

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]

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]

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

[Eric Wieser]

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

[Hunter Monroe]

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]

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]

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]

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]

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]

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

[Patrick Massot]

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]

@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]

@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.]

@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]

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.]

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

[Sebastien Gouezel]

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

[Jason KY.]

I've now removed the extra R. Certainly a surprise that a vector measures doesn't require a vector space!

[Hunter Monroe]

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]

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

[Jason KY.]

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]

(deleted)

[Hunter Monroe]

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

[Jason KY.]

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

[Hunter Monroe]

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

[Jason KY.]

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

[Daniil Homza]

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]

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

[Johan Commelin]

See also docs#finset.sum.

[Daniil Homza]

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]

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]

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

[Daniil Homza]

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

[Joshua Banks]

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]

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

[Joshua Banks]

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

[Kevin Buzzard]

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]

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

[Eric Wieser]

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]

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]

docs#measure_theory.measure_union is the first theorem Kevin mentions

[Kevin Buzzard]

These things will be called things like measure_union and measure_univ

[Joshua Banks]

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]

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

[Alistair Tucker]

I think you'll want to assume X measurable

[Alistair Tucker]

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]

The first ≤ is true as an = there too

[Joshua Banks]

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

[Joshua Banks]

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]

convert measure_univ will likely make that first goal clearer

[Kevin Buzzard]

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]

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

[Joshua Banks]

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]

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]

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

[Notification Bot]

Joshua Banks has marked this topic as resolved.

[Notification Bot]

Joshua Banks has marked this topic as resolved.

[Notification Bot]

Joshua Banks has marked this topic as unresolved.

[Joshua Banks]

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]

[oic now]

[Alistair Tucker]

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]

I think !![σ_sq, 0; 0, σ_sq].mul_vec a there is just a weird way to spell σ_sq • a

[Alistair Tucker]

Well the 0s are there to indicate independence!

[Alistair Tucker]

Edited :smile:.

[Joshua Banks]

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]

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]

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

[Dongheng Chen]

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]

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]

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)