Zulip Chat Archive

Stream: new members

Topic: How do I tell Lean that a subclass is a kind of the supercla


view this post on Zulip Lars Ericson (Dec 17 2020 at 16:57):

I'm working on this:

import measure_theory.lebesgue_measure

open measure_theory

noncomputable theory

class probability_space (α : Type*) extends measure_space α :=
(is_probability_measure:  probability_measure volume)

class random_variable (α β : Type*) :=
(domain : probability_space α )
(codomain : measurable_space β )
(outcome : α  β)
(is_measurable_outcome : @measurable α  β domain codomain outcome)

I am trying to say that a random variable is a measurable function from a probability space to a measurable space. Even though the function is declared α → β and I have proofs that domain is a probability_space and codomain is a measurable_space, I still guess that I need to add a proof that outcome is a measurable function. Or is it obvious? I'm unsure.

Anyway, if I do have to do the extra step of proving that outcome is measurable, I need to get this type right:

@measurable α  β domain codomain outcome

However, it is complaining

type mismatch at application
  measurable
term
  domain
has type
  probability_space α
but is expected to have type
  measurable_space α

even though

class probability_space (α : Type*) extends measure_space

and

class measure_space (α : Type*) extends measurable_space α

How do I tell Lean that a subclass is a kind of the superclass?

view this post on Zulip Adam Topaz (Dec 17 2020 at 17:04):

I would use something approximately like this:

import measure_theory.lebesgue_measure

open measure_theory

noncomputable theory

class probability_space (α : Type*) extends measure_space α :=
(is_probability_measure:  probability_measure volume)

structure random_variable (α β : Type*) [probability_space α] [measurable_space β] :=
(outcome : α  β)
(is_measurable_outcome : measurable outcome)

view this post on Zulip Lars Ericson (Dec 17 2020 at 17:06):

Thanks! Why structure and not class in this case? random_variable is a class of function, it seems possible people might want to create instances.

view this post on Zulip Reid Barton (Dec 17 2020 at 17:06):

This is more sensible yes, but also in the original formulation you can just write is_measurable_outcome : measurable outcome--if you don't try to do Lean's work for it, it will do it correctly.

view this post on Zulip Adam Topaz (Dec 17 2020 at 17:08):

Oh it looks like measurable is not a class, so I should use regular parens. (fixed code)

view this post on Zulip Adam Topaz (Dec 17 2020 at 17:10):

Does mathlib have bundled measurable functions?

view this post on Zulip Lars Ericson (Dec 17 2020 at 17:51):

Please help me take it a little further. To the random variable I want to add an inverse. So if X(ω) is a random variable, then
inverse(y) = {ω : X(ω) = y}. I tried this:

class random_variable (α β : Type*) [probability_space α] [measurable_space β] :=
(outcome : α  β)
(is_measurable_outcome : measurable outcome)
(inverse : β  set α := { ω : α //  y : β, y = outcome ω }) // ERROR

I got this error message, which I don't know how to fix:

invalid let-expression, term
  {ω //  (y : β), y = outcome ω}
has type
  Type ? : Type (max 1 (?+1))
but is expected to have type
  β  set α : Type (max ? ?)

From there I want to do this, to say that the distribution space is a probability space induced by X with probability measure volumeX : β→ [0,1] such that volumeX = volume ∘ (X^-1) is the pushforward measure and volumeX is called the distribution of X:

instance distribution_space (α β : Type*) (V: random_variable α β) (ΩAP: probability_space α ):  probability_space β :=
(volume : ΩAP.volume  V.generalize_inverse)
(is_probability_measure := sorry)

I'm not sure how to get this all right in Lean, but the ideas are there.

"pushforward" sounds categorical. If there were a category Prob there may be some categorical way to express what I'm trying to do here. I don't know category theory though. For now I'm just trying to get this part right.

view this post on Zulip Lars Ericson (Dec 17 2020 at 19:07):

OK I found something in the guts of measure_space but it doesn't show up in docs#pushforward for in Lean which is all category theory related:

/-- The pushforward of a measure. It is defined to be `0` if `f` is not a measurable function. -/
def map (f : α  β) : measure α →ₗ[ennreal] measure β :=
if hf : measurable f then
  lift_linear (outer_measure.map f) $ λ μ s hs t,
    le_to_outer_measure_caratheodory μ _ (hf hs) (f ⁻¹' t)
else 0

view this post on Zulip Adam Topaz (Dec 17 2020 at 20:20):

import measure_theory.lebesgue_measure

open measure_theory

noncomputable theory

class probability_space (α : Type*) extends measure_space α :=
(is_probability_measure :  probability_measure volume)

structure random_variable (α β : Type*) [probability_space α] [measurable_space β] :=
(outcome : α  β)
(is_measurable_outcome : measurable outcome)

variables {α β : Type*} [probability_space α] [measurable_space β]

def induced (X : random_variable α β) : probability_space β :=
{ volume := measure.map X.outcome volume,
  is_probability_measure := begin
    constructor,
    rw measure_theory.measure.map_apply X.is_measurable_outcome is_measurable.univ,
    apply probability_space.is_probability_measure.measure_univ,
  end }

One thing to note, as we discussed somewhere before, one should really make an API for probability_space so that the proof in is_probability_measure becomes essentially a one-liner.

view this post on Zulip Adam Topaz (Dec 17 2020 at 20:21):

The structure random_variable needs an API as well.

view this post on Zulip Adam Topaz (Dec 17 2020 at 20:21):

But I hope the code above helps you get started :)

view this post on Zulip Lars Ericson (Dec 17 2020 at 20:52):

Thank you @Adam Topaz that is extremely helpful. I have been looking at the API of measure.map:

import measure_theory.measure_space

open measure_theory

variables α β : Type*
variable MS1 : measurable_space α
variable MS2 : measurable_space β
variable μ_α : α  β
variable m_α : measure α

#check @measure_theory.measure.map α β MS1 MS2 μ_α m_α
#check measure_theory.measure.map μ_α m_α

This is the pushforward measure in Wikipedia: https://en.wikipedia.org/wiki/Pushforward_measure

There is also a comap in measure_space:

/-- Pullback of a `measure`. If `f` sends each `measurable` set to a `measurable` set, then for each
measurable set `s` we have `comap f μ s = μ (f '' s)`. -/
def comap (f : α  β) : measure β →ₗ[ennreal] measure α :=

What are the aesthetics of calling these map and comap versus pushforward and pullback? This would provide a conceptual link to various pushforward definitions in Topand category_theory: docs#pushforward. I'm just asking, pure curiosity, not a criticism.

view this post on Zulip Lars Ericson (Dec 17 2020 at 23:24):

Here is the last bit I want to get to before thinking about the overall API. Please take a look at Definition 7:

Screenshot-from-2020-12-17-18-23-57.png

view this post on Zulip Lars Ericson (Dec 17 2020 at 23:25):

Now take a look at section 1.1 B:
Screenshot-from-2020-12-17-18-24-10.png

view this post on Zulip Adam Topaz (Dec 17 2020 at 23:26):

What's the question? What is it precisely you want to get?

view this post on Zulip Yakov Pechersky (Dec 17 2020 at 23:30):

Are you asking about inverses? You could have:

class random_variable (α β : Type*) [probability_space α] [measurable_space β] :=
(outcome : α  β)
(is_measurable_outcome : measurable outcome)
(surj: function.surjective outcome)

and for the inverse use
docs#function.surj_inv

view this post on Zulip Lars Ericson (Dec 17 2020 at 23:30):

Here it comes, trying to type faster. Here's the first part:

So Mark Dean defines a notion of a distribution and a distribution function (when the random variable is into ℝ). Kloeden&co give an expression for the distribution function: FX(x) = PX((-∞ ,x)) = P({ω ∈ Ω : X(ω) ≤ x}).

They are both assuming that the random variable is into ℝ. I don't see any reason for this, because this: X(ω) ≤ x only requires that there be a preorder ≤ on the type β that the preorder is into.

view this post on Zulip Adam Topaz (Dec 17 2020 at 23:30):

Oh so you want the distribution then?

view this post on Zulip Lars Ericson (Dec 17 2020 at 23:31):

No, we have the distribution, I want to define the distribution_function in case β has a preorder in this sketch:

import measure_theory.lebesgue_measure
import measure_theory.measure_space

open measure_theory
noncomputable theory

class probability_space (α : Type*) extends measure_space α :=
(is_probability_measure :  probability_measure volume)

def probability_space.distribution (α : Type*) [ps: probability_space α] :=
  ps.volume

def probability_space.distribution_function  (X : random_variable α β ) [ps: probability_space β ]  [preorder β] :=
  sorry

structure random_variable (α β : Type*) [probability_space α] [measurable_space β] :=
(outcome : α  β)
(is_measurable_outcome : measurable outcome)

variables {α β : Type} [probability_space α] [measurable_space β]

instance distribution_space  (X : random_variable α β) : probability_space β :=
{ volume := measure.map X.outcome volume,
  is_probability_measure := begin
    constructor,
    rw measure_theory.measure.map_apply X.is_measurable_outcome is_measurable.univ,
    apply probability_space.is_probability_measure.measure_univ,
  end }

instance {α} {p : α  Prop} [m : measure_space α] : measure_space (subtype p) :=
{ volume := measure.comap (coe : _  α) volume }

theorem subtype.volume_apply {α} {p : α  Prop} [measure_space α]
  (hp : is_measurable {x | p x}) {s : set (subtype p)} (hs : is_measurable s) :
  volume s = volume ((coe : _  α) '' s) :=
measure.comap_apply _ subtype.coe_injective (λ _, is_measurable.subtype_image hp) _ hs

namespace Steinhaus

instance P : probability_measure (volume : measure (set.Icc (0 : ) 1)) :=
{ measure_univ := begin
    refine (subtype.volume_apply is_measurable_Icc is_measurable.univ).trans _,
    suffices : volume (set.Icc (0 : ) 1) = 1, {simpa},
    rw [real.volume_Icc], simp
  end }

instance ΩAP : probability_space (set.Icc (0 : ) 1) :=
{ is_probability_measure := Steinhaus.P }

#check Steinhaus.ΩAP
#check Steinhaus.ΩAP.volume -- volume : measure ↥(set.Icc 0 1)

end Steinhaus

view this post on Zulip Lars Ericson (Dec 17 2020 at 23:32):

So we have probability space, random variable, distribution space induced by random variable on probability space, and the final icing on the cake is to show that if I have a preorder on the measurable space that the random variable is into, then I have a distribution function.

view this post on Zulip Lars Ericson (Dec 17 2020 at 23:33):

Why this is at all interesting is because everybody in the world only defines distribution_function when the random variable is into . Nobody seems to care about the case where it is into a measurable space with a preorder. I just think it's an interesting generalization.

view this post on Zulip Lars Ericson (Dec 17 2020 at 23:34):

But it's only possible for me to talk about whether it is interesting or definable in the presence of something like Lean.

view this post on Zulip Mario Carneiro (Dec 17 2020 at 23:35):

@Yakov Pechersky There aren't any inverses involved in those snippets. That's a preimage you see

view this post on Zulip Lars Ericson (Dec 17 2020 at 23:37):

What I'm working on is this generalization of the distribution function in the Kloeden snippet, which Dean defines only if the RV is into the reals:

def probability_space.distribution_function  (X : random_variable α β ) (y: β)  \[ps: probability_space β ]  [preorder β] :=
  ps.volume({ω  α : X(ω)  y})

view this post on Zulip Yakov Pechersky (Dec 17 2020 at 23:37):

Ah, misread. Gotcha. So the clean wya to state that is outcome.preimage?

view this post on Zulip Mario Carneiro (Dec 17 2020 at 23:37):

Well, the whole measure is measure.comap I think

view this post on Zulip Mario Carneiro (Dec 17 2020 at 23:38):

actually measure.map

view this post on Zulip Lars Ericson (Dec 17 2020 at 23:40):

That's another question I had about terminology, why measure_space uses map and comap but in the comments it uses pushforward and pullback which comments match terminology used in Top and category_theory.

view this post on Zulip Mario Carneiro (Dec 17 2020 at 23:40):

so there isn't really anything to do in definition 7. measure.map x volume is a measure, check

view this post on Zulip Mario Carneiro (Dec 17 2020 at 23:40):

because there is a clash of terminology from multiple fields

view this post on Zulip Mario Carneiro (Dec 17 2020 at 23:41):

lean uses map and comap for regularity, but this gets instantiated in category theory and topology and algebra and measure theory and mathematicians in these areas all have their own ideas about what to call it

view this post on Zulip Lars Ericson (Dec 17 2020 at 23:41):

OK thanks. The above sketch works fine. @Adam Topaz worked out how to derive a distribution space from a random variable on a probability space:

instance distribution_space  (X : random_variable α β) : probability_space β :=
{ volume := measure.map X.outcome volume,
  is_probability_measure := begin
    constructor,
    rw measure_theory.measure.map_apply X.is_measurable_outcome is_measurable.univ,
    apply probability_space.is_probability_measure.measure_univ,
  end }

The only thing I have left to complete the functionality is generalized distribution function.

view this post on Zulip Mario Carneiro (Dec 17 2020 at 23:42):

I think you are missing a lemma there

view this post on Zulip Mario Carneiro (Dec 17 2020 at 23:42):

you just proved the map of a probability measure is a probability measure

view this post on Zulip Mario Carneiro (Dec 17 2020 at 23:42):

that's a lemma

view this post on Zulip Adam Topaz (Dec 17 2020 at 23:43):

import measure_theory.lebesgue_measure

open measure_theory

noncomputable theory

class probability_space (α : Type*) extends measure_space α :=
(is_probability_measure :  probability_measure volume)

namespace probability_space

lemma volume_univ {α : Type*} [probability_space α] : volume (set.univ : set α) = 1 :=
  is_probability_measure.measure_univ

def prob {α : Type*} [probability_space α] {S : set α} (h : is_measurable S) : ennreal :=
  volume S

end probability_space

structure random_variable (α β : Type*) [probability_space α] [measurable_space β] :=
(outcome : α  β)
(is_measurable_outcome : measurable outcome)

variables {α β : Type*} [probability_space α] [measurable_space β]

namespace random_variable

instance : has_coe_to_fun (random_variable α β) := _,outcome

lemma measurable (X : random_variable α β) : measurable X := X.is_measurable_outcome

def induced (X : random_variable α β) : probability_space β :=
{ volume := measure.map X volume,
  is_probability_measure := begin
    constructor,
    erw measure_theory.measure.map_apply X.measurable is_measurable.univ,
    exact probability_space.volume_univ
  end }

def distribution_function (X : random_variable α ) :   ennreal := λ x,
  @probability_space.prob _ X.induced {c | c  x} is_measurable_Iic

end random_variable

view this post on Zulip Mario Carneiro (Dec 17 2020 at 23:43):

why is prob an ennreal?

view this post on Zulip Adam Topaz (Dec 17 2020 at 23:43):

Because I'm lazy

view this post on Zulip Adam Topaz (Dec 17 2020 at 23:44):

One should change it to \R.

view this post on Zulip Adam Topaz (Dec 17 2020 at 23:44):

Same with distribtion_function.

view this post on Zulip Lars Ericson (Dec 17 2020 at 23:44):

Well that's what I'm trying to generalize. I want to replace ℝ with β where β has a preorder. What do you think?

view this post on Zulip Adam Topaz (Dec 17 2020 at 23:45):

Sure you could do that.

view this post on Zulip Mario Carneiro (Dec 17 2020 at 23:45):

I don't think that's a good idea, it's not general enough

view this post on Zulip Mario Carneiro (Dec 17 2020 at 23:46):

the sets {c | c ≤ x} in a preorder don't generate all borel sets

view this post on Zulip Mario Carneiro (Dec 17 2020 at 23:46):

you will have to work with the preimages of general sets, at which point it's not clear what the CDF gets you

view this post on Zulip Lars Ericson (Dec 17 2020 at 23:47):

It would be a really wonderful solution to a Math StackExchange question I posed in August, i.e. exactly what kind of order does β have to have for this to go through in Lean.

view this post on Zulip Lars Ericson (Dec 17 2020 at 23:48):

For one thing you know by construction of the random_variable that β is a measurable_space.

view this post on Zulip Lars Ericson (Dec 18 2020 at 00:51):

Mario Carneiro said:

you just proved the map of a probability measure is a probability measure, that's a lemma

It could be that makes it a category, which is something to think about. I.e. if you were building a probability library from scratch would you want to make it as category theory-ish as possible or just express the main ideas on their own. There seems to be big interest in category theory here, but it seems that using it in practice like for GCD/Fibonacci example is quite hard. So then the question is whether the generalization that it provides is productive for particular applications, or is it just nice to think about on its own. The fact that there is map/comap and pullback/pushthrough in different parts of the library shows that there is not a unified view among all the mathlib contributors. Not that there should be, I'm just slowly learning the "style guide" and "make it a category" doesn't seem to be one of the style imperatives.

view this post on Zulip Lars Ericson (Dec 18 2020 at 00:59):

Regarding this expression for the distribution_function, which is on single points in the codomain of the RV, as opposed to the distribution, which is on subsets of the domain of the RV: F(x) = P({ω ∈ Ω : X(ω) ≤ x}). We can see by inspection, since P is a probability measure, that it will be in [0,1]. If the codomain of the RV is some kind of partially ordered set, the distribution function might not behave in the same way as if it were a linearly ordered dense set. But the result will still be a CDF. I will Google "generalized distribution function" and see what I come up with. In any event, it seems well defined for any order relation .

view this post on Zulip Mario Carneiro (Dec 18 2020 at 01:03):

The fact that there is map/comap and pullback/pushthrough in different parts of the library shows that there is not a unified view among all the mathlib contributors

To clarify: map and comap are used consistently in lean names, while "pullback" and "pushforward" are used in comments to help connect names to things in the literature (which are all over the place, as one would expect)

view this post on Zulip Mario Carneiro (Dec 18 2020 at 01:06):

It could be that makes it a category, which is something to think about. I.e. if you were building a probability library from scratch would you want to make it as category theory-ish as possible or just express the main ideas on their own.

I would not suggest adding additional layers unless it gives you an advantage in proving theorems. Instantiating a category is a thing you can do, but it's not particularly helpful on its own. There are lots of things in mathlib that could potentially be instantiations of the category library, but generally it's just another layer on an existing theorem. I would say prove the theorem and add the instantiation if and when you need it for a theorem

view this post on Zulip Lars Ericson (Dec 18 2020 at 01:08):

OK so my main concern, all abstraction aside, is whether any measurable_set S with ≤ for which this expression: F(x: S) = P({ω ∈ Ω : X(ω) ≤ x}) makes sense is necessarily linearly ordered, dense and isomorphic to ℝ, or whether any measurable_set with any ≤ defined on it will do.

view this post on Zulip Adam Topaz (Dec 18 2020 at 01:09):

Just to clarify, whenever you have a random variable X with codomain A, and some function from A to the type of all measurable sets in A, you can define something like a distribution function on A. The question is whether this function determines the probability density on A induced by X, and this is certainly not true in general.

view this post on Zulip Mario Carneiro (Dec 18 2020 at 01:10):

I think instead of formalizing definitions, you should try to get to the actual theorems, because we can work backward from there to the abstractions that are useful for formalizing the theorem. So far, I don't see any value in the definition random_variable, or distribution, or prob or distribution_function, they are all just wrappers around other things. So let's get to theorems where you really need some probability vocabulary to prove the theorem effectively

view this post on Zulip Lars Ericson (Dec 18 2020 at 01:11):

Random variable, distribution, distribution function and probability space are probability vocabulary.

view this post on Zulip Mario Carneiro (Dec 18 2020 at 01:11):

yes I'm aware

view this post on Zulip Mario Carneiro (Dec 18 2020 at 01:11):

a wrapper doesn't help you prove theorems

view this post on Zulip Lars Ericson (Dec 18 2020 at 01:11):

Google gave me this, maybe it's of some use: https://www.ams.org/journals/tran/1957-084-02/S0002-9947-1957-0085326-5/S0002-9947-1957-0085326-5.pdf

view this post on Zulip Mario Carneiro (Dec 18 2020 at 01:13):

more words to express things you could already express are not helpful. The power of a definition is when it abbreviates a nontrivial combination of things, like "group" meaning "associative binary operation with a neutral element"

view this post on Zulip Mario Carneiro (Dec 18 2020 at 01:13):

the latter expression is more cumbersome than the former, so the definition pulls its weight

view this post on Zulip Mario Carneiro (Dec 18 2020 at 01:14):

there are also a bunch of theorems about groups that are not theorems about monoids or associative operations on their own

view this post on Zulip Lars Ericson (Dec 18 2020 at 01:14):

I'm not really trying to prove a theorem, I'm just trying to get the type classes straight to describe the usual vocabulary of probability theory. That's all. Because even though that vocabulary is just sugar for things that are already inmathlib in one way or another, they are still challenging for me. I can't go tomathlib and see the usual vocabulary of probability theory. It's a modest exercise.

view this post on Zulip Mario Carneiro (Dec 18 2020 at 01:15):

So what's the raison d'etre of probability vocabulary? What fact about probability measures is not true about general measures? I have no doubt that such theorems exist, but nothing interesting will happen until you start trying to prove one of them

view this post on Zulip Mario Carneiro (Dec 18 2020 at 01:18):

It is really important to find and at least start trying to prove one of these theorems because it guides the structure of definitions around the whole topic. Without it I see all these definitions and they are all useless cruft with negative utility

view this post on Zulip Lars Ericson (Dec 18 2020 at 01:21):

My longer range goal is to understand say the construction of the stochastic Taylor series approximation of the Ito or Stratonovich integral. I am not trying to prove any new theorems about this topic. I'm trying to build up the language used in a textbook that goes through that topic. The textbook doesn't use the measure-theoretic equivalent of probability_space. It uses probability_space. I don't think I should feel bad about, for my own purposes in reading that book, providing a definition of probability_space.

Along the way I noticed that F(x: S) = P({ω ∈ Ω : X(ω) ≤ x} could possibly be generalized. @Adam Topaz expresses this as whether the random variable X "determines the probability density on A induced by X". It seems that "determines the probability density on A induced by X" is something that could be written in Lean and expressed as a condition that the order relation ≤ has to satisfy. So, for my own tastes and ambitions, I think it would be interesting to say formalize "determines the probability density on A induced by X" and see where that leads. It could lead to the requirement that the codomain of the random variable be isomorphic to the reals, which would be an interesting and natural explanation for why every text I can find restricts distribution_function to random variables into the reals.

view this post on Zulip Mario Carneiro (Dec 18 2020 at 01:22):

The textbook doesn't use the measure-theoretic equivalent of probability_space. It uses probability_space. I don't think I should feel bad about, for my own purposes in reading that book, providing a definition of probability_space.

The point isn't to feel bad about it, it is to build the theory of probability spaces by looking at how it is used

view this post on Zulip Mario Carneiro (Dec 18 2020 at 01:23):

The question to answer isn't what is a probability space, it is what do people do with probability spaces

view this post on Zulip Mario Carneiro (Dec 18 2020 at 01:24):

the purpose of a library is to make it easier to write proofs in the area

view this post on Zulip Mario Carneiro (Dec 18 2020 at 01:24):

so you have to look at the proofs to understand how to help

view this post on Zulip Mario Carneiro (Dec 18 2020 at 01:27):

Regarding what you would need to make the exact definition F(x: S) = P({ω ∈ Ω : X(ω) ≤ x}) generalize, I would expect that you need the sets {a | a < x} to generate the topology and hence the entire borel algebra. That is, you need an orderable_topology on the codomain

view this post on Zulip Mario Carneiro (Dec 18 2020 at 01:29):

oops it's called docs#order_closed_topology now

view this post on Zulip Mario Carneiro (Dec 18 2020 at 01:30):

I think you will need to get to some really interesting theorems before the codomain starts to be constrained to look anything like the reals

view this post on Zulip Adam Topaz (Dec 18 2020 at 01:45):

Law of large numbers might be a nice goal.

view this post on Zulip Lars Ericson (Dec 18 2020 at 02:09):

In terms of "what do people do with probability spaces", and the book I am reading, I have some very simple applications that I want to proof-check in Lean:

  • A one-size-fits-all probability space:([0,1], B([0,1]), [a,b] -> b-a). That's done. Cruft is to name this the Steinhaus space
  • Some basic language: Random variable, distribution, distribution function
  • Distribution function for a two-point RV with codomain {0,1} and probabilities p and 1-p
  • Uniform distribution U[a,b]
  • Exponential distribution
  • Gaussian distribution

For each of these I want to:

  • Start with Steinhaus as the domain of the random variable X,
  • Define the codomain as either a finite measurable space for a continuous random variable or the appropriate continuous codomain which could be ereal or ennreal or a real interval
  • Define the corresponding random variable X
  • From X derive the distribution function FX

This is not the usual order. The book and most presentations tend to start with the distribution function. I just like doing it in this order because it appeals to me. I'm not proving theorems really, just trying to create language for a sequence that appeals to me for presenting these different discrete and continuous distributions in a consistent kind of top-down way. Also, I am annoyed that the book introduces probability_space on page 3 and then drops it thereafter and just presents the distribution_function for each distribution. I think if you define something you should use it, so I'm spending my time doing it in this direction. It's just a personal choice.

view this post on Zulip Mario Carneiro (Dec 18 2020 at 02:16):

well the main issue I have with that list is that every single one is a definition, there are no theorems

view this post on Zulip Mario Carneiro (Dec 18 2020 at 02:17):

you need at least some sanity checks on the definitions

view this post on Zulip Mario Carneiro (Dec 18 2020 at 02:20):

Perhaps your goal might be to have a way to prove that a real function (which is what the books will give in order to define a distribution) yields a probability distribution, that's not completely obvious from the definitions

view this post on Zulip Mario Carneiro (Dec 18 2020 at 02:22):

you can then use that to get the exponential distribution and gaussian distribution

view this post on Zulip Mario Carneiro (Dec 18 2020 at 02:23):

I think you already did the uniform distribution earlier

view this post on Zulip Lars Ericson (Dec 18 2020 at 03:07):

The interesting (to me) part, which I already did by hand, is when they give a distribution function, to back out what the random variable is that has that distribution function. It's not always easy to get it right. So my work is to take the RV that I backed out and prove that if you grind it through the Lean distribution_function construction, that I get the same function. So that's a proof.

Regarding the generalized disrtibution function, I am trying to generalize

def distribution_function (X : random_variable α ) :   ennreal := λ x,

to

def distribution_function (X : random_variable α β ) [preorder α] : β  (set.Icc (0 : ) 1) := λ x,

Adam's distribution function full definition is

def distribution_function (X : random_variable α ) :   ennreal := λ x,
  @probability_space.prob _ X.induced {c | c  x} is_measurable_Iic

I am trying to understand the application of @probability_space.prob. I've got this:

import measure_theory.lebesgue_measure

open measure_theory

noncomputable theory

class probability_space (α : Type*) extends measure_space α :=
(is_probability_measure :  probability_measure volume)

namespace probability_space

lemma volume_univ {α : Type*} [probability_space α] : volume (set.univ : set α) = 1 :=
  is_probability_measure.measure_univ

def prob {α : Type*} [probability_space α] {S : set α} (h : is_measurable S) : ennreal :=
  volume S

end probability_space

structure random_variable (α β : Type*) [probability_space α] [measurable_space β] :=
(outcome : α  β)
(is_measurable_outcome : measurable outcome)

variables {α β : Type*} [probability_space α] [measurable_space β]

namespace random_variable

instance : has_coe_to_fun (random_variable α β) := _,outcome

lemma measurable (X : random_variable α β) : measurable X := X.is_measurable_outcome

def induced (X : random_variable α β) : probability_space β :=
{ volume := measure.map X volume,
  is_probability_measure := begin
    constructor,
    erw measure_theory.measure.map_apply X.measurable is_measurable.univ,
    exact probability_space.volume_univ
  end }

variable MSα : measurable_space α
variable  : probability_space α
variable  : probability_space  β
variable  : set α
variable  : set β

lemma SMα : is_measurable  := sorry
lemma SMβ : is_measurable  := sorry
def Xαβ : random_variable α β := sorry

#check Xαβ.induced -- X.induced : probability_space β

#check @probability_space.prob α   (SMα  )
#check @probability_space.prob β   (SMβ ) -- FAILS

def distribution_function (X : random_variable α β ) [preorder α] : β  (set.Icc (0 : ) 1) := λ x, sorry
--  @probability_space.prob _ X.induced {c | c ≤ x} is_measurable_Iic

end random_variable

Even though the one before it works, this fails:

#check @probability_space.prob β   (SMβ ) -- FAILS

I don't fully understand why the type of SMα is Mα : ∀ (Sα : set ?M_1), is_measurable Sα, so I have to re-supply Sα when I use it even though it's declared

lemma SMα : is_measurable  := sorry

So

#check @probability_space.prob α   (SMα  )

works with type

probability_space.prob _ : ennreal

But

#check @probability_space.prob β   (SMβ )

gives

synthesized type class instance is not definitionally equal to expression inferred by typing rules, synthesized
  _inst_2
inferred
  measure_space.to_measurable_space

I am using @ to avoid this kind of mystery but it's not helping in this case. Any suggestions? This is a problem because in this line

@probability_space.prob _ X.induced {c | c  x} is_measurable_Iic

the term X.induced is going to have type probability_space β. So I need to understand how to fill out each of the arguments to @probability_space.prob but I can't even #check it in the β case, it only works for α.

The other minor issue is that probability_space.prob has return type ennreal when I know that in the end it will be constrained to (set.Icc (0 : ℝ) 1) by probability_measure volume. I'd rather just say it in the return type rather than ennreal, but that doesn't go through.

view this post on Zulip Mario Carneiro (Dec 18 2020 at 03:14):

So my work is to take the RV that I backed out and prove that if you grind it through the Lean distribution_function construction, that I get the same function. So that's a proof.

Can you state this theorem?

view this post on Zulip Mario Carneiro (Dec 18 2020 at 03:15):

it's not entirely clear to me what you mean by it

view this post on Zulip Mario Carneiro (Dec 18 2020 at 03:17):

I'm not sure there is anything to be gained with the #checks, all those variables are tripping you up. Just state a def or theorem and try to get the assumptions and the statement of the theorem right

view this post on Zulip Mario Carneiro (Dec 18 2020 at 03:18):

lemma SMα is false, it asserts all sets are measurable

view this post on Zulip Mario Carneiro (Dec 18 2020 at 03:18):

lemma SMβ is the same as lemma SMα

view this post on Zulip Lars Ericson (Dec 18 2020 at 05:03):

The point of the #checks was simply to check the type of the arguments to the expression, I was trying to figure out what kind of thing to fill in the blank for each of the slots in probability_space.prob. I know that it just applies the volume function, but in the explicit @ form there are a lot of things that need to be in place for the application to go through, and I was trying to understand their types.

The theorem to prove is as follows (for the type of random variables in the text, which is the usual type, not the generalized type I want):

  • We are given, in the text F_X: ℝ → [0,1] , the distribution_function for the random_variable named X: [0,1] → ℝ.
  • I construct, by inspection, a definition myX for the random variableX.
  • There is a distribution, μ_X : borel ℝ → [0,1], which is implicit.
  • In the Steinhaus space we have uniform probability measure 'P: borel ℝ → [0,1]`.
  • By construction (this is already proven out of the by the machinery in the cruft above), we have that μ_X = P ∘ X⁻¹
  • To prove: that myX = λ x, μ_X (set.Icc -∞ x)

For example, consider the two point distribution:
Screenshot-from-2020-12-18-00-03-15.png

view this post on Zulip Lars Ericson (Dec 18 2020 at 05:21):

Let x₁, x₂ ∈ ℝ and p₁ be the probability of drawing x₁. Then we can define X(ω) = if ω < p₁ then x₁ else x₂ or

def myX(ω: set.Icc (0 : ) 1) := if ω < p₁ then x₁ else x₂

also, the text is telling us that

def FX (x:  ) := if x<x₁ then 0 else if x₁  x < x₂ then p₁ else 1

and then the proof to achieve is

example : FX = λ x, (Steinhaus.volume  myX.induced) (set.Icc  x) := sorry

I find this interesting and a little bit tricky. It's not rocket science but it does seem to take some effort to get all the pieces in place. It's also not the generalized distribution function I was going on about, but it sketches out the path through the woods I am looking to take.

view this post on Zulip Mario Carneiro (Dec 18 2020 at 05:26):

I don't think X(ω) = if ω < p₁ then x₁ else x₂ is correct. What you need is for the probability that X = x1 to equal p1, meaning that the event space is bool or perhaps a general probability space on which you posit an event A whose probability is p1

view this post on Zulip Lars Ericson (Dec 18 2020 at 14:45):

On the index space [0,1] I am defining an eventA=[0,p1). According to Kloeden et al's book, I(A)(ω)= if ω∈A then x₁ else x₂ is a random variable on this space, for x₁=0 and x₂=1. Please let me know if I'm reading this wrong:
Screenshot-from-2020-12-18-09-43-54.png

view this post on Zulip Lars Ericson (Dec 18 2020 at 14:58):

Note instead of clumping the events in [0,p1) I could have defined A to be the union of a bunch of more randomly scattered subsets. That's not necessary for the definitions to work. There is no inherent "randomness" in random_variable in that sense. A random_variable is a fully determined function from a sample space to a measurable space.

view this post on Zulip Mario Carneiro (Dec 18 2020 at 16:44):

You don't need to define A to be anything in particular, it can be a hypothesis

view this post on Zulip Mario Carneiro (Dec 18 2020 at 16:44):

it's more general this way anyway because you don't know what event space is needed in order to match all the other constraints in a downstream theorem

view this post on Zulip Lars Ericson (Dec 18 2020 at 17:37):

The Kloeden book brings in (briefly) the idea of probability space, so I want to demonstrate it when explaining things to myself. I can use (Ω,A,P)= ([0,1],B([0,1]),[a,b]↦ b-a) as a "one sits fits all" probability space. Then I want to define a random variable on that space, obtain it's distribution D, and then obtain the distribution function F, which results in a new distribution (probability) space like (S,Σ,D)=(R, B(R), D) with CDF F. I want to do that in Lean for the 6 particular cases in the book. I'm not trying to make the most general Lean probability theory module, or prove old or new theorems. I'm just trying to demonstrate a little piece of mechanism, to myself, because it seems pretty to me. I don't expect anybody else to find it interesting. Think of it as me doing beginner-level gardening in my back yard. It's a hobby, not a calling.

On the task of describing stochastic integration at a Lean level of detail, Wilfrid Kendall has done a lot of work, 21 years ago, which seems easily adaptable. (Adapting old stuff to new contexts is also more hobby gardening, not necessarily of general interest.) Kendall worked in Reduce, then Axiom with fine details, then Mathematica. (Note, his .ps.gz files are really just .ps files, they aren't zipped.) His Axiom papers provide the most detail. Axiom has a much richer type system than Mathematica, so the Axiom implementation is an improvement on it's successor.

view this post on Zulip Mario Carneiro (Dec 18 2020 at 17:49):

I can use (Ω,A,P)= ([0,1],B([0,1]),[a,b]↦ b-a) as a "one sits fits all" probability space.

It's not, though, as soon as you have more than one variable. What if you have two {0,1} variables X and Y with probabilities p and q to be 1, which are independent? This model will not help there.

view this post on Zulip Lars Ericson (Dec 18 2020 at 18:52):

These 6 examples are all univariate. Steinhaus space is a good enough indexing space for univariate examples whether continuous or discrete. I'm not sure that what's in the sketch above (aside from my desire to generalize distribution_function) excludes product measures. Baby steps!

view this post on Zulip Mario Carneiro (Dec 18 2020 at 19:00):

it's generally easier to not commit to particular example spaces if you can help it. Define a gaussian distributed RV over any event space

view this post on Zulip Mario Carneiro (Dec 18 2020 at 19:00):

you are doing lean on hard mode for some reason I don't understand

view this post on Zulip Mario Carneiro (Dec 18 2020 at 19:01):

The use of [0,1] is AFAICT entirely superfluous, and your proofs and definitions will be smaller and easier without it

view this post on Zulip Mario Carneiro (Dec 18 2020 at 19:03):

certainly the book you are reading from has made no such commitment to an event space

view this post on Zulip Lars Ericson (Dec 18 2020 at 19:40):

These are toy examples for exposition of a small point. Before I can generalize these toy examples I have to be able to do them first. I'm not there yet. I can't generalize something I don't know how to do in a smaller context.

In terms of a grander design, the above sketch has

def prob {α : Type*} [probability_space α] {S : set α} (h : is_measurable S) : ennreal :=
  volume S

I would like to be able to say

def prob {α : Type*} [probability_space α] {S : set α} (h : is_measurable S) : (set.Icc (0 : ) 1) :=
  volume S

because probability measures by definition have as codomain [0,1]. Here's something I need to prove, but I don't know how to say it correctly in Lean:

lemma volume_type_01 {α : Type*}  [probability_space α] (X: set α) :
  ((volume X) : (set.Icc (0 : ) 1)) := sorry

I can say

lemma volume_gt_0_lt_1 {α : Type*}  [probability_space α] (X: set α) :
  0  (volume X)  (volume X)  1 := sorry

but that doesn't give me a way to replace ennreal with (set.Icc (0 : ℝ) 1).

view this post on Zulip Adam Topaz (Dec 18 2020 at 19:43):

I suggest using docs#ennreal.to_real

view this post on Zulip Mario Carneiro (Dec 18 2020 at 19:57):

These are toy examples for exposition of a small point. Before I can generalize these toy examples I have to be able to do them first.

The general case is easier than the specific case. I know this is counterintuitive, but it's true. The toy examples are way harder than general theorems about all measure spaces or all probability spaces, because the contingent details of the example don't get in the way

view this post on Zulip Lars Ericson (Dec 18 2020 at 20:24):

OK. The other thing I want to prove, to get the generalized distribution function, is something I at least know how to state:

lemma is_measurable_measurable_with_le (xx: β) [measurable_space β] [has_le β] : is_measurable {c | c  xx} :=
  sorry

With this, the following #check works fine:

variable XX: random_variable α β
variable xx : β
variable Xlte : has_le β

#check @probability_space.prob β XX.induced {c | c  xx} _  -- probability_space.prob ?M_1 : ennreal

However the exact same expression preceded by a def f := instead of a #check results in a fail:

def generalized_distribution_function := @probability_space.prob β XX.induced {c | c  xx} _ -- ERROR

The fail is:

failed to synthesize type class instance for
α : Type u_1,
β : Type u_2,
_inst_1 : probability_space α,
_inst_2 : measurable_space β,
XX : random_variable α β,
xx c : β
 has_le β

where the whole file is:

import measure_theory.lebesgue_measure
open measure_theory
noncomputable theory

class probability_space (α : Type*) extends measure_space α :=
(is_probability_measure :  probability_measure volume)

namespace probability_space

lemma volume_univ {α : Type*} [probability_space α] : volume (set.univ : set α) = 1 :=
  is_probability_measure.measure_univ

def prob {α : Type*} [probability_space α] {S : set α} (h : is_measurable S) : ennreal :=
  volume S

end probability_space

structure random_variable (α β : Type*) [probability_space α] [measurable_space β] :=
(outcome : α  β)
(is_measurable_outcome : measurable outcome)

variables {α β : Type*} [probability_space α] [measurable_space β]

namespace random_variable
instance : has_coe_to_fun (random_variable α β) := _,outcome
lemma measurable (X : random_variable α β) : measurable X := X.is_measurable_outcome

def induced (X : random_variable α β) : probability_space β :=
{ volume := measure.map X volume,
  is_probability_measure := begin
    constructor,
    erw measure_theory.measure.map_apply X.measurable is_measurable.univ,
    exact probability_space.volume_univ
  end }

def distribution_function (X : random_variable α ) :   ennreal := λ x,
  @probability_space.prob _ X.induced {c | c  x} is_measurable_Iic

lemma is_measurable_measurable_with_le (xx: β) [measurable_space β] [has_le β] : is_measurable {c | c  xx} :=
  sorry

variable XX: random_variable α β
variable xx : β
variable Xlte : has_le β

#check @probability_space.prob β XX.induced {c | c  xx} _  -- probability_space.prob ?M_1 : ennreal

def generalized_distribution_function := @probability_space.prob β XX.induced {c | c  xx} _ -- ERROR

end random_variable

view this post on Zulip Kevin Buzzard (Dec 18 2020 at 20:27):

As you can see, your variable Xlte is nowhere in your local context. has_le is a typeclass, so you need to use square brackets. Note that has_le is just an arbitrary relation, and whilst I know nothing about probability theory or measure theory, assuming [has_le \beta] is a very weak statement.

view this post on Zulip Lars Ericson (Dec 19 2020 at 00:38):

Thanks @Kevin Buzzard I figured out how to state things in a way that typechecks. Not quite done yet, I want to replace ennreal with real interval [0,1] following @Adam Topaz 's hint. Here is how it is with ennreal. There is just no sorry. Instead I introduced a new structure is_measurable_with_le to hold the proof that the set is measurable. It's a punt, but a more well-defined punt:

import measure_theory.lebesgue_measure
open measure_theory
noncomputable theory

class probability_space (α : Type*) extends measure_space α :=
(is_probability_measure :  probability_measure volume)

namespace probability_space

lemma volume_univ {α : Type*} [probability_space α] : volume (set.univ : set α) = 1 :=
  is_probability_measure.measure_univ

def prob {α : Type*} [probability_space α] {S : set α} (h : is_measurable S) : ennreal :=
  volume S

end probability_space

structure random_variable (α β : Type*) [probability_space α] [measurable_space β] :=
(outcome : α  β)
(is_measurable_outcome : measurable outcome)

variables {α β : Type*} [probability_space α] [measurable_space β]

namespace random_variable
instance : has_coe_to_fun (random_variable α β) := _,outcome
lemma measurable (X : random_variable α β) : measurable X := X.is_measurable_outcome

def induced (X : random_variable α β) : probability_space β :=
{ volume := measure.map X volume,
  is_probability_measure := begin
    constructor,
    erw measure_theory.measure.map_apply X.measurable is_measurable.univ,
    exact probability_space.volume_univ
  end }

def distribution_function (X : random_variable α ) :   ennreal := λ x,
  @probability_space.prob _ X.induced {c | c  x} is_measurable_Iic

structure is_measurable_with_le (β: Type*) (b: β) [measurable_space β] [preorder β] :=
 (proof: is_measurable {c: β | c  b})

def generalized_distribution_function (α β : Type*) [probability_space α] [mb: measurable_space β]
          [po: preorder β] (X: random_variable α β) (b: β) [im: @is_measurable_with_le β b mb po]  :=
    @probability_space.prob β X.induced {c | c  b} im.proof

end random_variable

view this post on Zulip Mario Carneiro (Dec 19 2020 at 01:46):

Here are some theorems. Try filling the sorries at the end.

import measure_theory.lebesgue_measure
open measure_theory
noncomputable theory

class probability_space (α : Type*) extends measure_space α :=
(is_probability_measure :  probability_measure volume)

namespace probability_space
variables {α : Type*} [probability_space α]

lemma volume_univ : volume (set.univ : set α) = 1 :=
is_probability_measure.measure_univ

lemma volume_le_one (S : set α) : volume S  1 :=
by rw  @volume_univ α; exact measure_mono (set.subset_univ _)

def prob (S : set α) :  := (volume S).to_real

def nnprob (S : set α) : nnreal := (volume S).to_nnreal

theorem volume_eq_nnprob (S : set α) : volume S = nnprob S :=
(ennreal.coe_to_nnreal $ ne_top_of_le_ne_top (by rintro ⟨⟩) (volume_le_one S)).symm

theorem prob_eq_nnprob (S : set α) : prob S = nnprob S := rfl

theorem nnprob_le_one (S : set α) : nnprob S  1 :=
ennreal.coe_le_coe.1 $ by rw  volume_eq_nnprob; exact volume_le_one S

theorem prob_le_one (S : set α) : prob S  1 := nnprob_le_one _

theorem zero_le_prob (S : set α) : 0  prob S := nnreal.zero_le_coe

theorem nnprob_mono {S T : set α} (h : S  T) : nnprob S  nnprob T :=
ennreal.coe_le_coe.1 $ by simpa only [ volume_eq_nnprob] using measure_mono h

theorem prob_mono {S T : set α} (h : S  T) : prob S  prob T :=
nnreal.coe_le_coe.2 $ nnprob_mono h

end probability_space

theorem measurable.map_probability_measure {α β} [probability_space α] [measurable_space β]
  {f : α  β} (hf : measurable f) :
  probability_measure (measure.map f volume) :=
by rw measure_theory.measure.map_apply hf is_measurable.univ;
    exact probability_space.volume_univ

structure random_variable (α β : Type*) [probability_space α] [measurable_space β] :=
(outcome : α  β)
(is_measurable_outcome : measurable outcome)

variables {α β : Type*} [probability_space α] [measurable_space β]

namespace random_variable
instance : has_coe_to_fun (random_variable α β) := _,outcome
variable (X : random_variable α β)
lemma measurable : measurable X := X.is_measurable_outcome

def induced (X : random_variable α β) : probability_space β :=
{ volume := measure.map X volume,
  is_probability_measure := X.measurable.map_probability_measure }

variables [preorder β]

def CDF (x : β) :  := @probability_space.prob _ X.induced {c | c  x}

theorem zero_le_CDF (x : β) : 0  X.CDF x := sorry
theorem CDF_le_one (x : β) : X.CDF x  1 := sorry
theorem CDF_mono {x y : β} (h : x  y) : X.CDF x  X.CDF y := sorry

variables [topological_space β] [order_closed_topology β] [opens_measurable_space β]

example (b : β) : is_measurable {c | c  b} := is_closed.is_measurable is_closed_Iic

end random_variable

view this post on Zulip Lars Ericson (Dec 19 2020 at 02:14):

Thank you @Mario Carneiro I will work on that.

view this post on Zulip Lars Ericson (Dec 19 2020 at 18:23):

I was able to prove zero_le_CDF and CDF_le_one. I am stuck on CDF_mono. I have it reduced to a proposition of form A implies B where I know B. I have a lemma for A. I don't know how to introduce the results of A into the hypothesis set. That's a simple Lean thing but I don't know how to do it. Then if I had that I could finish. Also I have to prove A which also seems simple but I don't know how to get started. Where

  • A is{c : β | c ≤ x} ⊆ {c : β | c ≤ y}
  • B is @probability_space.prob_mono β X.induced {c : β | c ≤ x} {c : β | c ≤ y} to hp

Here is the sketch so far. The part where I'm stuck as at the bottom:

import measure_theory.lebesgue_measure
import tactic

noncomputable theory

open measure_theory

class probability_space (α : Type*) extends measure_space α :=
(is_probability_measure :  probability_measure volume)

namespace probability_space
variables {α : Type*} [probability_space α]

lemma volume_univ : volume (set.univ : set α) = 1 :=
is_probability_measure.measure_univ

lemma volume_le_one (S : set α) : volume S  1 :=
by rw  @volume_univ α; exact measure_mono (set.subset_univ _)

def prob (S : set α) :  := (volume S).to_real

def nnprob (S : set α) : nnreal := (volume S).to_nnreal

theorem volume_eq_nnprob (S : set α) : volume S = nnprob S :=
(ennreal.coe_to_nnreal $ ne_top_of_le_ne_top (by rintro ⟨⟩) (volume_le_one S)).symm

theorem prob_eq_nnprob (S : set α) : prob S = nnprob S := rfl

theorem nnprob_le_one (S : set α) : nnprob S  1 :=
ennreal.coe_le_coe.1 $ by rw  volume_eq_nnprob; exact volume_le_one S

theorem prob_le_one (S : set α) : prob S  1 := nnprob_le_one _

theorem zero_le_prob (S : set α) : 0  prob S := nnreal.zero_le_coe

theorem nnprob_mono {S T : set α} (h : S  T) : nnprob S  nnprob T :=
ennreal.coe_le_coe.1 $ by simpa only [ volume_eq_nnprob] using measure_mono h

theorem prob_mono {S T : set α} (h : S  T) : prob S  prob T :=
nnreal.coe_le_coe.2 $ nnprob_mono h

end probability_space

theorem measurable.map_probability_measure {α β} [probability_space α] [measurable_space β]
  {f : α  β} (hf : measurable f) :
  probability_measure (measure.map f volume) :=
by rw measure_theory.measure.map_apply hf is_measurable.univ;
    exact probability_space.volume_univ

structure random_variable (α β : Type*) [probability_space α] [measurable_space β] :=
(outcome : α  β)
(is_measurable_outcome : measurable outcome)

variables {α β : Type*} [probability_space α] [measurable_space β]

namespace random_variable
instance : has_coe_to_fun (random_variable α β) := _,outcome
variable (X : random_variable α β)
lemma measurable : measurable X := X.is_measurable_outcome

def induced (X : random_variable α β) : probability_space β :=
{ volume := measure.map X volume,
  is_probability_measure := X.measurable.map_probability_measure }

variables [preorder β]

def CDF (x : β) :  := @probability_space.prob _ X.induced {c | c  x}

variables [topological_space β] [order_closed_topology β] [opens_measurable_space β]

example (b : β) : is_measurable {c | c  b} := is_closed.is_measurable is_closed_Iic

lemma prob_eq_CDF (x : β) : X.CDF x = @probability_space.prob β X.induced {c | c  x} := rfl

theorem zero_le_CDF (x : β) : 0  X.CDF x :=
begin
  rw prob_eq_CDF,
  exact (@probability_space.zero_le_prob β X.induced {c : β | c  x}),
end

theorem CDF_le_one (x : β) : X.CDF x  1 :=
begin
  rw prob_eq_CDF,
  exact (@probability_space.prob_le_one β X.induced {c : β | c  x}),
end

lemma factoid (x y : β ): {c : β | c  x}  {c : β | c  y} :=
begin
  sorry   -- STUCK
end

theorem CDF_mono {x y : β} (h : x  y) : X.CDF x  X.CDF y :=
begin
  repeat { rw prob_eq_CDF },
  -- introduce hp: factoid(x y)  -- STUCK
  -- apply @probability_space.prob_mono β X.induced {c : β | c ≤ x} {c : β | c ≤ y}  to hp
  sorry
end

end random_variable

view this post on Zulip Mario Carneiro (Dec 19 2020 at 18:31):

The factoid is false, because you forgot the essential assumption x <= y! Do you see why this theorem should be true mathematically?

view this post on Zulip Mario Carneiro (Dec 19 2020 at 18:37):

also you changed the theorems I wrote by moving them after the variables [topological_space beta]... line. They were written before that line because they don't require any of that stuff to be proven

view this post on Zulip Mario Carneiro (Dec 19 2020 at 18:39):

In fact, I think that line is wrong; indeed there shouldn't be any measurable space structure on beta, because the theorems are all about X.induced which uses only the measurable structure on alpha

view this post on Zulip Lars Ericson (Dec 19 2020 at 19:03):

I moved those up just to put the sorry parts the bottom. I will move back down. How is this for factoid:

lemma factoid [preorder β] (x y : β ) (h : x  y) : {c : β | c  x}  {c : β | c  y} :=
begin
  sorry
end

Given factoid what's the proof language to introduce the result of a lemma into the hypothesis set? If I have revised factoid then I need that to apply here:

theorem CDF_mono {x y : β} (h : x  y) : X.CDF x  X.CDF y :=
begin
  repeat { rw prob_eq_CDF },
  -- introduce hp: factoid(x y)
  -- apply @probability_space.prob_mono β X.induced {c : β | c ≤ x} {c : β | c ≤ y}  to hp
  sorry
end

The revised sketch is

import measure_theory.lebesgue_measure
import tactic

noncomputable theory

open measure_theory

class probability_space (α : Type*) extends measure_space α :=
(is_probability_measure :  probability_measure volume)

namespace probability_space
variables {α : Type*} [probability_space α]

lemma volume_univ : volume (set.univ : set α) = 1 :=
is_probability_measure.measure_univ

lemma volume_le_one (S : set α) : volume S  1 :=
by rw  @volume_univ α; exact measure_mono (set.subset_univ _)

def prob (S : set α) :  := (volume S).to_real

def nnprob (S : set α) : nnreal := (volume S).to_nnreal

theorem volume_eq_nnprob (S : set α) : volume S = nnprob S :=
(ennreal.coe_to_nnreal $ ne_top_of_le_ne_top (by rintro ⟨⟩) (volume_le_one S)).symm

theorem prob_eq_nnprob (S : set α) : prob S = nnprob S := rfl

theorem nnprob_le_one (S : set α) : nnprob S  1 :=
ennreal.coe_le_coe.1 $ by rw  volume_eq_nnprob; exact volume_le_one S

theorem prob_le_one (S : set α) : prob S  1 := nnprob_le_one _

theorem zero_le_prob (S : set α) : 0  prob S := nnreal.zero_le_coe

theorem nnprob_mono {S T : set α} (h : S  T) : nnprob S  nnprob T :=
ennreal.coe_le_coe.1 $ by simpa only [ volume_eq_nnprob] using measure_mono h

theorem prob_mono {S T : set α} (h : S  T) : prob S  prob T :=
nnreal.coe_le_coe.2 $ nnprob_mono h

end probability_space

theorem measurable.map_probability_measure {α β} [probability_space α] [measurable_space β]
  {f : α  β} (hf : measurable f) :
  probability_measure (measure.map f volume) :=
by rw measure_theory.measure.map_apply hf is_measurable.univ;
    exact probability_space.volume_univ

structure random_variable (α β : Type*) [probability_space α] [measurable_space β] :=
(outcome : α  β)
(is_measurable_outcome : measurable outcome)

variables {α β : Type*} [probability_space α] [measurable_space β]

namespace random_variable
instance : has_coe_to_fun (random_variable α β) := _,outcome
variable (X : random_variable α β)
lemma measurable : measurable X := X.is_measurable_outcome

def induced (X : random_variable α β) : probability_space β :=
{ volume := measure.map X volume,
  is_probability_measure := X.measurable.map_probability_measure }

variables [preorder β]

def CDF (x : β) :  := @probability_space.prob _ X.induced {c | c  x}

lemma prob_eq_CDF (x : β) : X.CDF x = @probability_space.prob β X.induced {c | c  x} := rfl

theorem zero_le_CDF (x : β) : 0  X.CDF x :=
begin
  rw prob_eq_CDF,
  exact (@probability_space.zero_le_prob β X.induced {c : β | c  x}),
end

theorem CDF_le_one (x : β) : X.CDF x  1 :=
begin
  rw prob_eq_CDF,
  exact (@probability_space.prob_le_one β X.induced {c : β | c  x}),
end

lemma factoid [preorder β] (x y : β ) (h : x  y) : {c : β | c  x}  {c : β | c  y} :=
begin
  sorry
end

theorem CDF_mono {x y : β} (h : x  y) : X.CDF x  X.CDF y :=
begin
  repeat { rw prob_eq_CDF },
  -- introduce hp: factoid(x y)
  -- apply @probability_space.prob_mono β X.induced {c : β | c ≤ x} {c : β | c ≤ y}  to hp
  sorry
end

variables [topological_space β] [order_closed_topology β] [opens_measurable_space β]

example (b : β) : is_measurable {c | c  b} := is_closed.is_measurable is_closed_Iic

end random_variable

view this post on Zulip Mario Carneiro (Dec 19 2020 at 19:32):

Have you read #tpil or played the natural number game? They introduce all the tools you need to write proofs. In this case, you need have := factoid x y h.

view this post on Zulip Lars Ericson (Dec 19 2020 at 19:59):

Yes I did both but in their examples the have is usually something like have hp : p, from h.left so a labelled proposition from a tactic applied to the existing goal state. I didn't find any examples in #tpil of have := with a term. In #tpil and the number game, lemmas and theorems are used into introduce equalities that get applied with rw tactic or implications that get applied with apply or exact.

view this post on Zulip Lars Ericson (Dec 19 2020 at 19:59):

Anyway, DONE:

import measure_theory.lebesgue_measure
import tactic

noncomputable theory

open measure_theory

class probability_space (α : Type*) extends measure_space α :=
(is_probability_measure :  probability_measure volume)

namespace probability_space
variables {α : Type*} [probability_space α]

lemma volume_univ : volume (set.univ : set α) = 1 :=
is_probability_measure.measure_univ

lemma volume_le_one (S : set α) : volume S  1 :=
by rw  @volume_univ α; exact measure_mono (set.subset_univ _)

def prob (S : set α) :  := (volume S).to_real

def nnprob (S : set α) : nnreal := (volume S).to_nnreal

theorem volume_eq_nnprob (S : set α) : volume S = nnprob S :=
(ennreal.coe_to_nnreal $ ne_top_of_le_ne_top (by rintro ⟨⟩) (volume_le_one S)).symm

theorem prob_eq_nnprob (S : set α) : prob S = nnprob S := rfl

theorem nnprob_le_one (S : set α) : nnprob S  1 :=
ennreal.coe_le_coe.1 $ by rw  volume_eq_nnprob; exact volume_le_one S

theorem prob_le_one (S : set α) : prob S  1 := nnprob_le_one _

theorem zero_le_prob (S : set α) : 0  prob S := nnreal.zero_le_coe

theorem nnprob_mono {S T : set α} (h : S  T) : nnprob S  nnprob T :=
ennreal.coe_le_coe.1 $ by simpa only [ volume_eq_nnprob] using measure_mono h

theorem prob_mono {S T : set α} (h : S  T) : prob S  prob T :=
nnreal.coe_le_coe.2 $ nnprob_mono h

end probability_space

theorem measurable.map_probability_measure {α β} [probability_space α] [measurable_space β]
  {f : α  β} (hf : measurable f) :
  probability_measure (measure.map f volume) :=
by rw measure_theory.measure.map_apply hf is_measurable.univ;
    exact probability_space.volume_univ

structure random_variable (α β : Type*) [probability_space α] [measurable_space β] :=
(outcome : α  β)
(is_measurable_outcome : measurable outcome)

variables {α β : Type*} [probability_space α] [measurable_space β]

namespace random_variable
instance : has_coe_to_fun (random_variable α β) := _,outcome
variable (X : random_variable α β)
lemma measurable : measurable X := X.is_measurable_outcome

def induced (X : random_variable α β) : probability_space β :=
{ volume := measure.map X volume,
  is_probability_measure := X.measurable.map_probability_measure }

variables [preorder β]

def CDF (x : β) :  := @probability_space.prob _ X.induced {c | c  x}

lemma prob_eq_CDF (x : β) : X.CDF x = @probability_space.prob β X.induced {c | c  x} := rfl

theorem zero_le_CDF (x : β) : 0  X.CDF x :=
begin
  rw prob_eq_CDF,
  exact (@probability_space.zero_le_prob β X.induced {c : β | c  x}),
end

theorem CDF_le_one (x : β) : X.CDF x  1 :=
begin
  rw prob_eq_CDF,
  exact (@probability_space.prob_le_one β X.induced {c : β | c  x}),
end

lemma factoid [preorder β] (x y : β ) (h : x  y) : {c : β | c  x}  {c : β | c  y} :=
  set.Iic_subset_Iic.mpr h

theorem CDF_mono {x y : β} (h : x  y) : X.CDF x  X.CDF y :=
begin
  repeat { rw prob_eq_CDF },
  have h1 := factoid x y h,
  have h2 := @probability_space.prob_mono β X.induced {c : β | c  x} {c : β | c  y},
  exact h2 h1,
end

variables [topological_space β] [order_closed_topology β] [opens_measurable_space β]

example (b : β) : is_measurable {c | c  b} := is_closed.is_measurable is_closed_Iic

end random_variable

view this post on Zulip Mario Carneiro (Dec 19 2020 at 20:21):

In your example h.left is a term

view this post on Zulip Mario Carneiro (Dec 19 2020 at 20:22):

Note that have := (which is part of the less abbreviated have h : t := term) is the tactic mode version; the term mode version is have h : t, from term,.

view this post on Zulip Mario Carneiro (Dec 19 2020 at 20:26):

It looks like have is introduced in https://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game/?world=5&level=3

view this post on Zulip Lars Ericson (Dec 19 2020 at 20:36):

Thanks you are correct! In terms of my original generalized distribution_function goal, the above can be trimmed down to the assumption that a random variable is from a probability space α to a measurable space β which is a preorder. CDF is from β to ℝ. Ideally it should be to set.Icc (0: ℝ) 1. I guess the additional theorems will help me prove that and restate def CDF (x : β) : ℝ as def CDF (x : β) : set.Icc (0: ℝ) 1? The example at the end shows how to prove that {c | c ≤ b} is measurable for a type which is a topological space, an order closed topology and a measurable space. Bu those don't seem to be conditions required by the factoid, which only needs preorder. Are all these properties needed for anything or just measurable space with preorder?

view this post on Zulip Mario Carneiro (Dec 19 2020 at 20:55):

Ideally it should be to set.Icc (0: ℝ) 1.

As you can see, we have theorems that it is between zero and one. This is generally preferable up until you actually need to put it into a structure that expects set.Icc (0: ℝ) 1, which you don't currently have

view this post on Zulip Mario Carneiro (Dec 19 2020 at 20:57):

The example at the end shows how to prove that {c | c ≤ b} is measurable for a type which is a topological space, an order closed topology and a measurable space. Bu those don't seem to be conditions required by the factoid, which only needs preorder. Are all these properties needed for anything or just measurable space with preorder?

I put it as an example to show that it is derivable, but so far nothing actually needs those assumptions. You haven't done anything that requires {c | c ≤ b} to be measurable yet, but if you do those are the assumptions you will need (at that point, and not before)

view this post on Zulip Lars Ericson (Dec 19 2020 at 21:00):

Can you help me with the mechanics of this:

def distribution_function (x: β) :  set.Icc (0: ) 1 := (CDF x).to_set_Icc_01

It seems I would need to define

def nat.to_set_Icc_01 (x: ) := sorry

but that doesn't use the 0/1 theorems and doesn't seem right.

view this post on Zulip Mario Carneiro (Dec 19 2020 at 21:02):

def CDF_in_01 (x: β) : set.Icc (0 : ) 1 := X.CDF x, X.zero_le_CDF x, X.CDF_le_one x

view this post on Zulip Mario Carneiro (Dec 19 2020 at 21:02):

to reiterate, don't use this unless you need it

view this post on Zulip Lars Ericson (Dec 19 2020 at 21:03):

It's in the nature of CDF, what would be the aesthetic or practical reason not to constrain the codomain in this way?

view this post on Zulip Mario Carneiro (Dec 19 2020 at 21:04):

because real has operations on it, like addition, while set.Icc 0 1 doesn't

view this post on Zulip Lars Ericson (Dec 19 2020 at 21:05):

Anyway isn't it exciting to know that CDF can be generalized to any measurable space with a preorder? It's maybe a useless fact but I've never seen it in any presentation of CDF.

view this post on Zulip Mario Carneiro (Dec 19 2020 at 21:06):

Sure, this kind of "trivial generalization" comes up all the time in mathlib. It makes you consider questions the original authors hadn't thought about, like what closure properties are needed to prove that the CDF is left-continuous?

view this post on Zulip Mario Carneiro (Dec 19 2020 at 21:07):

You just read what the authors say, delete all the assumptions, and then just add the assumptions if they become necessary and not before

view this post on Zulip Mario Carneiro (Dec 19 2020 at 21:08):

A nonzero proportion of the time you never add some of them back

view this post on Zulip Mario Carneiro (Dec 19 2020 at 21:08):

In fact mathlib has a linter which will do this for you

view this post on Zulip Lars Ericson (Dec 19 2020 at 21:12):

If you don't mind my quoting your proof above, I can now close my old Stack Exchange question with a definitive answer.


view this post on Zulip Mario Carneiro (Dec 19 2020 at 21:17):

It seems that you got an answer in that question already:

CDFs are defined only for R\mathbb{R} (even for Rn\mathbb{R}^n) and are used for convenience. The push-forward is of a measure μ\mu by a Random variable X:(Ω,F,μ)(S,Σ)X:(\Omega,\mathscr{F},\mu)\rightarrow(S,\Sigma), μX(A):=μ(XA)\mu_X(A):=\mu(X\in A) is the object of interest and it is as general as it can be, since (S,Σ)(S,\Sigma) has no structure other than being a measurable space.

view this post on Zulip Mario Carneiro (Dec 19 2020 at 21:18):

This is another way to say that in a more general context we stop talking about the CDF because the pushforward measure is more general

view this post on Zulip Mario Carneiro (Dec 19 2020 at 21:19):

A CDF is only useful to the extent that it determines the pushforward measure

view this post on Zulip Lars Ericson (Dec 19 2020 at 21:27):

CDF is defined on points in S. The convention is that only the case S=R has any use. What we showed is that if S is any measurable space with a preorder, CDF can still be computed and give back a number in [0,1]. So I can define a preorder on a domain like binary expression trees of depth at most n and compute the CDF of a tree in the space of all binary trees depth at most n. I can say that and say that it is interesting to me because it is. This has nothing to do with using CDF to determine the pushforward measure. So that comment doesn't make any sense to me. I got the result I was looking for, and it doesn't seem to be relevant to that comment. That or it's not possible to put a preorder on binary trees, and continuing on in the vein, maybe the claim is that any measurable set with preorder is isomorphic to . Is that the case?

view this post on Zulip Mario Carneiro (Dec 19 2020 at 21:28):

Yes you can compute a number, but the question is what does that number mean? It's not true for a general preorder that giving the CDF of the random variable uniquely determines the distribution of the variable

view this post on Zulip Mario Carneiro (Dec 19 2020 at 21:29):

maybe the claim is that any measurable set with preorder is isomorphic to ℝ. Is that the case?

This is certainly not the case

view this post on Zulip Mario Carneiro (Dec 19 2020 at 21:31):

you have a function called CDF, but that doesn't on its own mean much. Here's another function called CDF:

def CDF' (X : random_variable α β) (x : β) :  := 0

This one doesn't even need a preorder structure on beta, so it's a clear improvement. It's also monotone, between 0 and 1, and right continuous

view this post on Zulip Lars Ericson (Dec 19 2020 at 21:36):

Except our CDF is proven to be a probability_measure on a measurable_space with preorder, by construction. I'll take that. It's not 0.

view this post on Zulip Mario Carneiro (Dec 19 2020 at 21:36):

Our CDF is no such thing

view this post on Zulip Mario Carneiro (Dec 19 2020 at 21:36):

it's a real function

view this post on Zulip Mario Carneiro (Dec 19 2020 at 21:36):

I can put all those assumptions on CDF' too

view this post on Zulip Mario Carneiro (Dec 19 2020 at 21:37):

Obviously CDF' is a silly function, but the point is that we haven't shown anything about CDF that makes it meaningfully different from CDF'

view this post on Zulip Mario Carneiro (Dec 19 2020 at 21:38):

And my claim is that the real theorem of interest that will distinguish the two doesn't hold on arbitrary preorders

view this post on Zulip Lars Ericson (Dec 19 2020 at 21:38):

Obtained by running prob, where prob was supplied as a probability_measure when building the initial probability space, and then running it through induced on the random_variable. As long as you have a meaningful and correct probability_space to begin with, and a meaningful and correct random_variable, the CDF will be meaningful and correct and derived from the original probability_space and the supplied random_variable. There is nothing trivial about it at all.

view this post on Zulip Mario Carneiro (Dec 19 2020 at 21:39):

How do you know it is meaningful and correct?

view this post on Zulip Mario Carneiro (Dec 19 2020 at 21:39):

That's what theorems are for

view this post on Zulip Mario Carneiro (Dec 19 2020 at 21:39):

and we don't have any

view this post on Zulip Mario Carneiro (Dec 19 2020 at 21:39):

except the obvious ones that are true also for CDF'

view this post on Zulip Lars Ericson (Dec 19 2020 at 21:40):

If I start out with say the Steinhaus space and the definition of the random variable for the 2 point-distribution and crank it through I will get the distribution and distribution function for the 2-point random variable. What's missing?

view this post on Zulip Mario Carneiro (Dec 19 2020 at 21:41):

well that's over real

view this post on Zulip Mario Carneiro (Dec 19 2020 at 21:41):

I thought you wanted arbitrary preorders?

view this post on Zulip Lars Ericson (Dec 19 2020 at 21:42):

As another example we could compute distributions of binary trees of depth n. This is something people actually think about. Why can't I have a CDF of those?

view this post on Zulip Mario Carneiro (Dec 19 2020 at 21:42):

The main theorem here is that two random variables with the same CDF are the same random variable

view this post on Zulip Mario Carneiro (Dec 19 2020 at 21:42):

that's not true for CDF'

view this post on Zulip Mario Carneiro (Dec 19 2020 at 21:42):

and it's not true for CDF on some preorders

view this post on Zulip Mario Carneiro (Dec 19 2020 at 21:43):

Really, I think it's not worth thinking about the CDF in the more unusual codomains. Just call X.induced CDF if it makes you feel better

view this post on Zulip Lars Ericson (Dec 19 2020 at 21:46):

So what you proved at the bottom required that S be a topological space, an order closed topology and an opens measurable space. I don't need those assumptions for def CDF. If I delete variables [preorder β], then def CDF crashes. It doesn't rely however on being topological space, order closed topology and opens measurable space. Are you saying that I will crash if I try to define a random variable into binary trees of length N with a preorder, because of something I'm not understanding?

view this post on Zulip Mario Carneiro (Dec 19 2020 at 21:46):

In measure theory, a distribution is no more or less than a measure. It takes all subsets of X as its input, and it doesn't need to be boiled down to a function on X

view this post on Zulip Mario Carneiro (Dec 19 2020 at 21:49):

I don't need those assumptions for def CDF. If I delete variables [preorder β], then def CDF crashes. It doesn't rely however on being topological space, order closed topology and opens measurable space. Are you saying that I will crash if I try to define a random variable into binary trees of length N with a preorder, because of something I'm not understanding?

This is why you need to prove theorems about your definitions. It's perfectly possible that a definition can be made in some tremendous generality but it doesn't make sense without some more assumptions. In fact def CDF works using only has_le beta, it doesn't even need preorder, but it certainly doesn't make sense in that generality; we already have a theorem that will detect this nonsense, namely CDF_mono. WIthout that theorem you might well think that there are no problems with that definition

view this post on Zulip Mario Carneiro (Dec 19 2020 at 21:49):

But you haven't tried to prove anything more complicated about CDF yet, and when you do you will find that preorder beta isn't good enough either

view this post on Zulip Mario Carneiro (Dec 19 2020 at 21:51):

It all comes back to the thing I mentioned earlier: how do people use the definition?

view this post on Zulip Mario Carneiro (Dec 19 2020 at 21:51):

making definitions doesn't tell you any deep truths about it, because you can very easily write nonsense without noticing

view this post on Zulip Mario Carneiro (Dec 19 2020 at 21:52):

but once you try to use the definition it all falls down

view this post on Zulip Lars Ericson (Dec 19 2020 at 21:56):

Which brings me back to trees. A long time ago I helped a mathematician counting trees to write a paper making some probabiliistic arguments about operations on trees. Conceivably, while doing that, in a practical sense, I might want to define a preorder on trees and compute the percentage of trees in the entire space of trees of size n which were "less than" a single particular tree, or an equivalence class of trees. So that would be the CDF of a single tree. It might be boring nonsense to almost everybody in the world, but for the two people in that room, it might be helpful. So then the question, how much of this will fall down if my trees have a preorder but do not constitute a type which is a topological space, order closed topology and opens measurable space? All of it, some of it or none of it? And if it is all of it, can we go further and say that there is a 1-1 onto map between the reals and any such space?

view this post on Zulip Reid Barton (Dec 19 2020 at 22:06):

Even in this hypothetical scenario, you could just write down "the probability that a random tree is 'less than' the particular tree in question" and not bother with this CDF terminology stuff.

view this post on Zulip Lars Ericson (Dec 20 2020 at 15:37):

Yes, I could write "the probability that a random tree is 'less than' the particular tree in question" as CDF T after defining a preorder on trees, following the development of the generalized distribution function above, which establishes that I can do so in a well-typed way. This is very helpful for me. Thanks!

view this post on Zulip Lars Ericson (Dec 20 2020 at 16:36):

But I think the answer to the question of why distribution function is only defined by the literature for R is in this comment by Oliver Diaz in the Wikipedia article:

"If (𝑌,𝑑) is s Borel space (a Polish space for instance) then it is measurable isomorphic to (0,1) and one can define an order in 𝑌. The isomorphism however is not explicit, it is based on constructions that use the axiom of choice."

"Measurable isomorphic to (0,1)" is what I was looking for, it gives motivation for only talking about R, in the sense that talking about Y would be redundant under the isomorphism.

view this post on Zulip Mario Carneiro (Dec 20 2020 at 17:27):

I don't think that is true at all

view this post on Zulip Mario Carneiro (Dec 20 2020 at 17:28):

Y can easily be something like bool with the preorder formulation

view this post on Zulip Mario Carneiro (Dec 20 2020 at 17:30):

you need a lot more assumptions to make it look like real. Borel won't cut it, Polish might but it's not clear what the reason for such an assumption is


Last updated: May 15 2021 at 02:11 UTC