## 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 structures 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"?

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 structures?

#mwe (sorry)

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

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