Zulip Chat Archive

Stream: maths

Topic: measurable_coe for prob measures


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

view this post on Zulip Mario Carneiro (Jul 08 2019 at 21:03):

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

view this post on Zulip Mario Carneiro (Jul 08 2019 at 21:04):

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

view this post on Zulip Koundinya Vajjha (Jul 08 2019 at 21:06):

do you mean ennreal.measurable_coe?

view this post on Zulip Mario Carneiro (Jul 08 2019 at 21:07):

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

view this post on Zulip Mario Carneiro (Jul 08 2019 at 21:07):

I think what you called measurable_coe is a different statement

view this post on Zulip Koundinya Vajjha (Jul 08 2019 at 21:08):

yes thats the lemma measurable_to_measure in the snippet

view this post on Zulip Mario Carneiro (Jul 08 2019 at 21:08):

aha, so it is

view this post on Zulip Mario Carneiro (Jul 08 2019 at 21:08):

If you compose measurable_to_measure with measurable_coe you should get measurable_coe'

view this post on Zulip Koundinya Vajjha (Jul 08 2019 at 21:15):

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

view this post on Zulip Mario Carneiro (Jul 08 2019 at 21:22):

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

view this post on Zulip Koundinya Vajjha (Jul 08 2019 at 21:29):

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

view this post on Zulip Koundinya Vajjha (Jul 08 2019 at 21:29):

Do you recommend refine?

view this post on Zulip Kevin Buzzard (Jul 08 2019 at 21:30):

I'm pretty sure he does

view this post on Zulip Kevin Buzzard (Jul 08 2019 at 21:30):

but rw is a great tactic, keep using that

view this post on Zulip Koundinya Vajjha (Jul 08 2019 at 21:33):

why is apply bad?

view this post on Zulip Mario Carneiro (Jul 08 2019 at 21:33):

because it is imprecise and buggy

view this post on Zulip Kenny Lau (Jul 08 2019 at 21:34):

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

view this post on Zulip Kenny Lau (Jul 08 2019 at 21:34):

or the kernel or whatever

view this post on Zulip Mario Carneiro (Jul 08 2019 at 21:34):

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

view this post on Zulip Kevin Buzzard (Jul 08 2019 at 21:35):

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

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

view this post on Zulip Mario Carneiro (Jul 08 2019 at 21:36):

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

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

view this post on Zulip Koundinya Vajjha (Jul 08 2019 at 21:36):

how is refine different from apply?

view this post on Zulip Mario Carneiro (Jul 08 2019 at 21:36):

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

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

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

view this post on Zulip Kevin Buzzard (Jul 08 2019 at 21:37):

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

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