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

Stream: new members

[Lars Ericson]

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?

[Adam Topaz]

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)

[Lars Ericson]

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.

[Reid Barton]

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.

[Adam Topaz]

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

[Adam Topaz]

Does mathlib have bundled measurable functions?

[Lars Ericson]

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.

[Lars Ericson]

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

[Adam Topaz]

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.

[Adam Topaz]

The structure random_variable needs an API as well.

[Adam Topaz]

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

[Lars Ericson]

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.

[Lars Ericson]

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

[Lars Ericson]

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

[Adam Topaz]

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

[Yakov Pechersky]

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

[Lars Ericson]

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.

[Adam Topaz]

Oh so you want the distribution then?

[Lars Ericson]

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

[Lars Ericson]

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.

[Lars Ericson]

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.

[Lars Ericson]

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

[Mario Carneiro]

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

[Lars Ericson]

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})

[Yakov Pechersky]

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

[Mario Carneiro]

Well, the whole measure is measure.comap I think

[Mario Carneiro]

actually measure.map

[Lars Ericson]

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.

[Mario Carneiro]

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

[Mario Carneiro]

because there is a clash of terminology from multiple fields

[Mario Carneiro]

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

[Lars Ericson]

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.

[Mario Carneiro]

I think you are missing a lemma there

[Mario Carneiro]

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

[Mario Carneiro]

that's a lemma

[Adam Topaz]

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

[Mario Carneiro]

why is prob an ennreal?

[Adam Topaz]

Because I'm lazy

[Adam Topaz]

One should change it to \R.

[Adam Topaz]

Same with distribtion_function.

[Lars Ericson]

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

[Adam Topaz]

Sure you could do that.

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Lars Ericson]

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.

[Lars Ericson]

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

[Lars Ericson]

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.

[Lars Ericson]

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

[Mario Carneiro]

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)

[Mario Carneiro]

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

[Lars Ericson]

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.

[Adam Topaz]

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.

[Mario Carneiro]

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

[Lars Ericson]

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

[Mario Carneiro]

yes I'm aware

[Mario Carneiro]

a wrapper doesn't help you prove theorems

[Lars Ericson]

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

[Mario Carneiro]

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"

[Mario Carneiro]

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

[Mario Carneiro]

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

[Lars Ericson]

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.

[Mario Carneiro]

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

[Mario Carneiro]

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

[Lars Ericson]

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.

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

oops it's called docs#order_closed_topology now

[Mario Carneiro]

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

[Adam Topaz]

Law of large numbers might be a nice goal.

[Lars Ericson]

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.

[Mario Carneiro]

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

[Mario Carneiro]

you need at least some sanity checks on the definitions

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

I think you already did the uniform distribution earlier

[Lars Ericson]

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 Pα : probability_space α
variable Pβ : probability_space  β
variable Sα : set α
variable Sβ : set β

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

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

#check @probability_space.prob α Pα Sα (SMα Sα )
#check @probability_space.prob β Pβ Sβ (SMβ Sβ) -- 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 β Pβ Sβ (SMβ Sβ) -- 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 Sα := sorry

So

#check @probability_space.prob α Pα Sα (SMα Sα )

works with type

probability_space.prob _ : ennreal

But

#check @probability_space.prob β Pβ Sβ (SMβ Sβ)

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.

[Mario Carneiro]

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?

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

lemma SMβ is the same as lemma SMα

[Lars Ericson]

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

[Lars Ericson]

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.

[Mario Carneiro]

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

[Lars Ericson]

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

[Lars Ericson]

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.

[Mario Carneiro]

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

[Mario Carneiro]

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

[Lars Ericson]

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.

[Mario Carneiro]

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.

[Lars Ericson]

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!

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Lars Ericson]

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

[Adam Topaz]

I suggest using docs#ennreal.to_real

[Mario Carneiro]

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

[Lars Ericson]

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

[Kevin Buzzard]

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.

[Lars Ericson]

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

[Mario Carneiro]

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

[Lars Ericson]

Thank you @Mario Carneiro I will work on that.

[Lars Ericson]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Lars Ericson]

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

[Mario Carneiro]

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.

[Lars Ericson]

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.

[Lars Ericson]

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

[Mario Carneiro]

In your example h.left is a term

[Mario Carneiro]

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

[Mario Carneiro]

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

[Lars Ericson]

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?

[Mario Carneiro]

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

[Mario Carneiro]

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)

[Lars Ericson]

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.

[Mario Carneiro]

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

[Mario Carneiro]

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

[Lars Ericson]

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

[Mario Carneiro]

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

[Lars Ericson]

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.

[Mario Carneiro]

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?

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Lars Ericson]

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

[Mario Carneiro]

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

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Lars Ericson]

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?

[Mario Carneiro]

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

[Mario Carneiro]

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

This is certainly not the case

[Mario Carneiro]

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

[Lars Ericson]

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.

[Mario Carneiro]

Our CDF is no such thing

[Mario Carneiro]

it's a real function

[Mario Carneiro]

I can put all those assumptions on CDF' too

[Mario Carneiro]

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'

[Mario Carneiro]

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

[Lars Ericson]

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.

[Mario Carneiro]

How do you know it is meaningful and correct?

[Mario Carneiro]

That's what theorems are for

[Mario Carneiro]

and we don't have any

[Mario Carneiro]

except the obvious ones that are true also for CDF'

[Lars Ericson]

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?

[Mario Carneiro]

well that's over real

[Mario Carneiro]

I thought you wanted arbitrary preorders?

[Lars Ericson]

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?

[Mario Carneiro]

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

[Mario Carneiro]

that's not true for CDF'

[Mario Carneiro]

and it's not true for CDF on some preorders

[Mario Carneiro]

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

[Lars Ericson]

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?

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Lars Ericson]

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?

[Reid Barton]

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.

[Lars Ericson]

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!

[Lars Ericson]

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.

[Mario Carneiro]

I don't think that is true at all

[Mario Carneiro]

Y can easily be something like bool with the preorder formulation

[Mario Carneiro]

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