measurable_coe for prob measures

Stream: maths

[Koundinya Vajjha]

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]

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

[Mario Carneiro]

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

[Koundinya Vajjha]

do you mean ennreal.measurable_coe?

[Mario Carneiro]

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

[Mario Carneiro]

I think what you called measurable_coe is a different statement

[Koundinya Vajjha]

yes thats the lemma measurable_to_measure in the snippet

[Mario Carneiro]

aha, so it is

[Mario Carneiro]

If you compose measurable_to_measure with measurable_coe you should get measurable_coe'

[Koundinya Vajjha]

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

[Mario Carneiro]

dude, stop using apply, it's bad for your health

[Koundinya Vajjha]

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

[Koundinya Vajjha]

Do you recommend refine?

[Kevin Buzzard]

I'm pretty sure he does

[Kevin Buzzard]

but rw is a great tactic, keep using that

[Koundinya Vajjha]

why is apply bad?

[Mario Carneiro]

because it is imprecise and buggy

[Kenny Lau]

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

[Kenny Lau]

or the kernel or whatever

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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]

how is refine different from apply?

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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"