type vs set for finite measure

Stream: new members

[Iocta]

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]

e.g. unfold doesn't seem to work on structures so idk how to expand the set.univ = 1

[Kevin Buzzard]

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

[Iocta]

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

[Kevin Buzzard]

You want a type

[Kevin Buzzard]

They're a more primitive notion

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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]

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?

[Scott Morrison]

#mwe (sorry)

[Iocta]

see above

[Iocta]

(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]

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

[Scott Morrison]

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]

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

[Sebastien Gouezel]

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]

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]

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]

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

[Iocta]

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]

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]

example : p univ = 1 := measure_univ

[Sebastien Gouezel]

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]

Oh oops, not sure how I missed that.

[Iocta]

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]

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

[Reid Barton]

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

[Iocta]

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

[Reid Barton]

I would unsuggest it

[Iocta]

ok

[Reid Barton]

Your goal is to prove an inequality--intros isn't a logical step unless you know what that inequality really means.

[Reid Barton]

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]

really, it should be a lemma that already exists

[Iocta]

Is that lemma measure_lt_top?