# Zulip Chat Archive

## Stream: new members

### Topic: type vs set for finite measure

#### Iocta (Sep 02 2020 at 01:02):

I'm not sure if I want

```
def F (X: Ω → ℝ): ℝ → {x : nnreal | x ≤ 1} :=
λx,
let y := p {ω | X ω ≤ x}
in ⟨ y.to_nnreal, sorry ⟩
```

or to define a type `{x : nnreal // x ≤ 1}`

and use that instead. Either way I don't know how to use the definition to show that p <=1.

Context is

```
import algebra.big_operators
import algebra.big_operators.intervals
import measure_theory.measure_space
open measure_theory
open_locale big_operators
noncomputable theory
variables {Ω : Type*} [measurable_space Ω] (p : measure Ω) [probability_measure p]
def F (X: Ω → ℝ): ℝ → {x : nnreal | x ≤ 1} :=
λx,
let y := p {ω | X ω ≤ x}
in ⟨ y.to_nnreal,
begin
simp at *,
-- y: ennreal := ⇑p {ω : Ω | X ω ≤ x}
-- ⊢ y.to_nnreal ≤ 1
end
⟩
```

#### Iocta (Sep 02 2020 at 01:05):

e.g. `unfold`

doesn't seem to work on `structure`

s so idk how to expand the `set.univ = 1`

#### Kevin Buzzard (Sep 02 2020 at 06:35):

There is Icc 0 1 for the interval [0,1].

#### Iocta (Sep 02 2020 at 06:36):

How should I think about "do I want a type or a set"?

#### Kevin Buzzard (Sep 02 2020 at 06:37):

You want a type

#### Kevin Buzzard (Sep 02 2020 at 06:37):

They're a more primitive notion

#### Kevin Buzzard (Sep 02 2020 at 06:38):

Of course I'm being a bit silly here. You want a set if you want to do intersections, unions etc

#### Kevin Buzzard (Sep 02 2020 at 06:39):

But the target of a function had better be a type. There's a coercion from sets to types though, and if you keep your head it's not hard to use. A term of type weird up arrow s is a pair consisting of a term of type X and a proof that it's an element of s

#### Iocta (Sep 02 2020 at 06:49):

```
def probability : Type :=
let interval : set _ := (Icc 0 1)
in {x : _ // x ∈ interval }
```

Do I want in the `_`

real/nnreal/ennreal/complex/doesn't matter?

#### Iocta (Sep 02 2020 at 07:00):

anyway that leaves me with

```
y: ennreal := ⇑p {ω : Ω | X ω ≤ x}
⊢ ↑(y.to_nnreal) ≤ 1
```

but I can't `unfold probability_measure at p`

to get the `<= 1`

, is there a similar thing to `unfold`

but for `structure`

s?

#### Scott Morrison (Sep 02 2020 at 07:01):

~~#mwe~~ (sorry)

#### Iocta (Sep 02 2020 at 07:02):

see above

#### Iocta (Sep 02 2020 at 07:04):

(updated)

```
import algebra.big_operators
import algebra.big_operators.intervals
import measure_theory.measure_space
open measure_theory set
open_locale big_operators
noncomputable theory
variables {Ω : Type*} [measurable_space Ω] (p : measure Ω) [probability_measure p]
def probability : Type :=
let interval : set ℝ := (Icc 0 1)
in {x // x ∈ interval }
def F (X: Ω → ℝ): ℝ → probability :=
λx,
let y := p {ω | X ω ≤ x}
in ⟨ y.to_nnreal,
begin
simp,
end
⟩
```

#### Scott Morrison (Sep 02 2020 at 07:09):

The API for `probability_measure`

seems to be basically nonexistent. Someone should fix this!

#### Scott Morrison (Sep 02 2020 at 07:09):

At the moment it looks like you have argue that the measure is at most the measure of `set.univ`

, which is then equal to one.

#### Scott Morrison (Sep 02 2020 at 07:10):

Obviously there should be a one-step lemma saying exactly that.

#### Sebastien Gouezel (Sep 02 2020 at 07:15):

Note that it is probably a bad idea to let the probability take value in the set `[0, 1]`

, because we keep adding or subtracting probabilities in proofs, and this type doesn't have an addition nor a subtraction. Why not simply use the real-valued function?

#### Iocta (Sep 02 2020 at 07:18):

sometimes I will want to use that the value is <= 1, so I could put that into the type and then it would be readily available

#### Iocta (Sep 02 2020 at 07:20):

e.g. next I want to say the right-hand limit of the distribution function is 1. it seems convenient to know that it's increasing and <=1. Is that the wrong way to go?

#### Scott Morrison (Sep 02 2020 at 07:24):

Just have a separate lemma that it is at most one. Bundling that into a subtype doesn't seem to gain much.

#### Iocta (Sep 02 2020 at 07:51):

What do `h`

and `H`

mean?

```
import algebra.big_operators
import algebra.big_operators.intervals
import measure_theory.measure_space
open measure_theory set
open_locale big_operators
noncomputable theory
variables {Ω : Type*} [measurable_space Ω] (p : measure Ω) [probability_measure p]
lemma probability_1 : p univ ≤ 1 :=
begin
sorry,
end
def F (X: Ω → ℝ) : ℝ → ennreal :=
λx, p {ω | X ω ≤ x}
lemma F_le_1 (X : Ω → ℝ) : F p X ≤ 1 :=
begin
intros x pr h,
-- tactic failed, there are unsolved goals
-- state:
-- Ω : Type u_1,
-- _inst_1 : measurable_space Ω,
-- p : measure Ω,
-- _inst_2 : probability_measure p,
-- X : Ω → ℝ,
-- x : ℝ,
-- pr : nnreal,
-- h : pr ∈ 1 x
-- ⊢ ∃ (b : nnreal) (H : b ∈ F p X x), b ≤ pr
end
```

#### Iocta (Sep 02 2020 at 20:08):

How can I solve this using `measure_univ`

?

```
import algebra.big_operators
import algebra.big_operators.intervals
import measure_theory.measure_space
open measure_theory set
open_locale big_operators
noncomputable theory
variables {Ω : Type*} [measurable_space Ω] (p : measure Ω) [probability_measure p]
example : p univ = 1 := sorry
```

#### Sebastien Gouezel (Sep 02 2020 at 20:11):

```
example : p univ = 1 := measure_univ
```

#### Sebastien Gouezel (Sep 02 2020 at 20:15):

You can find this by trying `by library_search`

and following whatever advice it gives you, or by looking at the type of `measure_univ`

and noticing it has no explicit argument: the fact that the measure is a probability measure is an assumption written between `[...]`

, which means that Lean will check this assumption all by itself (through a process called typeclass inference that you don't need to understand when you start with Lean).

#### Iocta (Sep 02 2020 at 20:17):

Oh oops, not sure how I missed that.

#### Iocta (Sep 02 2020 at 20:20):

any idea what `h : pr ∈ 1 x`

means in the above snippet? what is `1 x`

? it looks like `1`

is somehow a set-returning function...

#### Reid Barton (Sep 02 2020 at 20:23):

What made you think `intros x pr h`

was a good idea?

#### Reid Barton (Sep 02 2020 at 20:23):

It looks like you've opened up the definition of `ennreal`

#### Iocta (Sep 02 2020 at 20:24):

I didn't know what else to do, and `hint`

suggested it

#### Reid Barton (Sep 02 2020 at 20:24):

I would unsuggest it

#### Iocta (Sep 02 2020 at 20:25):

ok

#### Reid Barton (Sep 02 2020 at 20:25):

Your goal is to prove an inequality--`intros`

isn't a logical step unless you know what that inequality really means.

#### Reid Barton (Sep 02 2020 at 20:27):

presumably the argument you want is that whatever set we're taking the probability of, it's contained in `univ`

, which has measure 1, so the original probability is at most 1

#### Reid Barton (Sep 02 2020 at 20:27):

really, it should be a lemma that already exists

#### Iocta (Sep 02 2020 at 21:35):

Is that lemma `measure_lt_top`

?

Last updated: May 08 2021 at 03:17 UTC