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