Zulip Chat Archive

Stream: new members

Topic: type vs set for finite measure


view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Sep 02 2020 at 06:35):

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

view this post on Zulip Iocta (Sep 02 2020 at 06:36):

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

view this post on Zulip Kevin Buzzard (Sep 02 2020 at 06:37):

You want a type

view this post on Zulip Kevin Buzzard (Sep 02 2020 at 06:37):

They're a more primitive notion

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip Scott Morrison (Sep 02 2020 at 07:01):

#mwe (sorry)

view this post on Zulip Iocta (Sep 02 2020 at 07:02):

see above

view this post on Zulip 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

view this post on Zulip Scott Morrison (Sep 02 2020 at 07:09):

The API for probability_measure seems to be basically nonexistent. Someone should fix this!

view this post on Zulip 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.

view this post on Zulip Scott Morrison (Sep 02 2020 at 07:10):

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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Sebastien Gouezel (Sep 02 2020 at 20:11):

example : p univ = 1 := measure_univ

view this post on Zulip 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).

view this post on Zulip Iocta (Sep 02 2020 at 20:17):

Oh oops, not sure how I missed that.

view this post on Zulip 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...

view this post on Zulip Reid Barton (Sep 02 2020 at 20:23):

What made you think intros x pr h was a good idea?

view this post on Zulip Reid Barton (Sep 02 2020 at 20:23):

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

view this post on Zulip Iocta (Sep 02 2020 at 20:24):

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

view this post on Zulip Reid Barton (Sep 02 2020 at 20:24):

I would unsuggest it

view this post on Zulip Iocta (Sep 02 2020 at 20:25):

ok

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Reid Barton (Sep 02 2020 at 20:27):

really, it should be a lemma that already exists

view this post on Zulip Iocta (Sep 02 2020 at 21:35):

Is that lemma measure_lt_top?


Last updated: May 08 2021 at 03:17 UTC