## Stream: maths

### Topic: measurable_coe for prob measures

#### Koundinya Vajjha (Jul 08 2019 at 20:30):

I've been trying to port some of the results in giry_monad.lean over to probability measures, and i'm struggling with the first one.
Can someone help?

import measure_theory.giry_monad
universe u
open measure_theory measure_theory.measure set lattice

section
variables (α : Type*) (β : Type*) [measurable_space α] [measurable_space β]

structure probability_measure extends measure_theory.measure α :=
(measure_univ : to_measure univ = 1)

instance : measurable_space (probability_measure α) :=
measure.measurable_space.comap probability_measure.to_measure

lemma measurable_to_measure :
measurable (@probability_measure.to_measure α _) :=
measurable_space.le_map_comap

instance prob_measure_coe : has_coe (probability_measure α) (measure α) :=
⟨probability_measure.to_measure⟩

instance : has_coe_to_fun (probability_measure α) :=
⟨λ_, set α → nnreal, λp s, ennreal.to_nnreal (p.to_measure s)⟩

lemma measurable_coe {s : set α} (hs : is_measurable s) : measurable (λμ : measure α, μ s) :=
measurable_space.comap_le_iff_le_map.1 $le_supr_of_le s$ le_supr_of_le hs $le_refl _ lemma measurable_coe' {s : set α} (hs : is_measurable s) : measurable (λμ : probability_measure α, μ s) := measurable_space.comap_le_iff_le_map.1$
begin
rw probability_measure.measurable_space,
rw measurable_space.comap_le_iff_le_map,
intros s hs, sorry,
end

end


#### Mario Carneiro (Jul 08 2019 at 21:03):

I guess the first thing you want to show is that coe is a measurable function

#### Mario Carneiro (Jul 08 2019 at 21:04):

which should follow from the definition of the measurable space as the comap of coe

#### Koundinya Vajjha (Jul 08 2019 at 21:06):

do you mean ennreal.measurable_coe?

#### Mario Carneiro (Jul 08 2019 at 21:07):

I mean the coe from probability_measure to measure that you just defined

#### Mario Carneiro (Jul 08 2019 at 21:07):

I think what you called measurable_coe is a different statement

#### Koundinya Vajjha (Jul 08 2019 at 21:08):

yes thats the lemma measurable_to_measure in the snippet

aha, so it is

#### Mario Carneiro (Jul 08 2019 at 21:08):

If you compose measurable_to_measure with measurable_coe you should get measurable_coe'

#### Koundinya Vajjha (Jul 08 2019 at 21:15):

apply measurable.comp is picking up a different composition..

#### Koundinya Vajjha (Jul 08 2019 at 21:29):

Someone told me to stop using rw because that was bad for my health

#### Koundinya Vajjha (Jul 08 2019 at 21:29):

Do you recommend refine?

#### Kevin Buzzard (Jul 08 2019 at 21:30):

I'm pretty sure he does

#### Kevin Buzzard (Jul 08 2019 at 21:30):

but rw is a great tactic, keep using that

#### Koundinya Vajjha (Jul 08 2019 at 21:33):

why is apply bad?

#### Mario Carneiro (Jul 08 2019 at 21:33):

because it is imprecise and buggy

#### Kenny Lau (Jul 08 2019 at 21:34):

because the elaborator needs to figure out how many spaces you are leaving

#### Kenny Lau (Jul 08 2019 at 21:34):

or the kernel or whatever

#### Mario Carneiro (Jul 08 2019 at 21:34):

especially measurable.comp is a bad thing to apply because matching the composition is wildly ambiguous

#### Kevin Buzzard (Jul 08 2019 at 21:35):

We seem to have used apply well over 200 times in the perfectoid project.

#### Mario Carneiro (Jul 08 2019 at 21:35):

you will have much better luck if you actually specify at least one of the two functions in the composition

#### Mario Carneiro (Jul 08 2019 at 21:36):

apply is fine when it works, but you should be pleasantly surprised when it does work

#### Kevin Buzzard (Jul 08 2019 at 21:36):

but one thing I've learnt about apply is that in general you shouldn't get too cocky with it, or you'll end up with 10 goals some of which are metavariables and some of which are instances which are already in your context and some of which will randomly disappear later on for no obvious reason

#### Koundinya Vajjha (Jul 08 2019 at 21:36):

how is refine different from apply?

#### Mario Carneiro (Jul 08 2019 at 21:36):

I think writing an entire proof using apply, apply, apply is bad style

#### Mario Carneiro (Jul 08 2019 at 21:37):

You get control over what you want to specify now and what to leave to the next step

#### Mario Carneiro (Jul 08 2019 at 21:37):

for example instead of apply foo, apply bar you can write refine foo bar _ or refine foo _ bar

#### Kevin Buzzard (Jul 08 2019 at 21:37):

With apply you should usually fill in as many of the gaps as you can.

#### Kevin Buzzard (Jul 08 2019 at 21:39):

My thought process is usually: "aah, random_lemma has conclusion equal to my goal, let's try applying that with apply random_lemma, oh crap I now have a gazillion goals not all of which are solvable, maybe I should have used refine random_lemma _ _, oh wait, what am I even doing, I may as well just fill in those _s, oh look, now it's working great again"

Last updated: May 18 2021 at 06:15 UTC