Zulip Chat Archive

Stream: general

Topic: help with measurability proof


Koundinya Vajjha (Jun 26 2019 at 18:02):

Can anyone help me prove this lemma?

import measure_theory.giry_monad
universe u

variables {α : Type u} {β : Type u}

open measure_theory measure_theory.measure

lemma inl_measurable_bind_ret [measurable_space α] [measurable_space β] (ν : measure β) :
  measurable (λ (x : α), bind ν (λ y, dirac (x,y))) :=
begin
  apply measurable_of_measurable_coe,
  intros s hs,
  sorry,
end

I have proven that λ y, dirac (x,y) is measurable for all x and also have that bind followed by dirac is map. But at this point, I am stuck...any suggestions?

Chris Hughes (Jun 26 2019 at 19:22):

I had a go. No idea if the sorry if even true or not, but I look like I made progress.

lemma inl_measurable_bind_ret' [measurable_space α] [measurable_space β] (w : measure β) :
  measurable (λ (x : α), bind w (λ y, dirac (x, y))) :=
have  x : α, measurable (@prod.mk α β x),
  from λ x, measurable_prod_mk measurable_const measurable_id,
begin
  dsimp [measure.bind],
  conv in (map _ _) { rw [ measure.map_map measurable_dirac (this x)] },
  refine measurable_join.comp _,
  refine measurable.comp _ _,
  { refine measurable_map _ measurable_dirac },
  { sorry }

end

Koundinya Vajjha (Jun 26 2019 at 20:15):

this is progress, but I'm not able to fill in the sorry either.

Chris Hughes (Jun 26 2019 at 20:16):

Is it true?

Koundinya Vajjha (Jun 26 2019 at 20:32):

i'm about 70% sure

Jason Rute (Jun 26 2019 at 21:35):

Dumb question: as far as whether or not this is true, what is the implicit sigma algebra on the codomain of the map you are trying to prove is measurable?

Koundinya Vajjha (Jun 26 2019 at 21:41):

For Chris' sorry, the codomain is ennreal. So it is the Borel sigma algebra

Kenny Lau (Jun 26 2019 at 21:52):

after a long while I've reduced the statement to proving this:

α β : Type u,
_inst_1 : measurable_space α,
_inst_2 : measurable_space β,
ν : measure β,
s : set (α × β),
hs : is_measurable s
 measurable (λ (b : α), ν {y : β | (b, y)  s})

Koundinya Vajjha (Jun 26 2019 at 21:57):

Yeah this is where I am stuck as well. :(

Kenny Lau (Jun 26 2019 at 21:57):

is this even true

Kenny Lau (Jun 26 2019 at 21:58):

this is demonstrably false if one uses Lebesgue measurable sets for R and R^2

Kenny Lau (Jun 26 2019 at 21:59):

but the Lebesgue sigma-algebra for R^2 isn't the product of the Lebesgue sigma algebra for R right

Kenny Lau (Jun 26 2019 at 22:31):

α β : Type u,
_inst_1 : measurable_space α,
_inst_2 : measurable_space β,
ν : measure β
 measurable (λ (x : α), map (prod.mk x) ν)

Kenny Lau (Jun 26 2019 at 22:31):

this looks neater

Kenny Lau (Jun 26 2019 at 22:31):

surely all neat propositions are true

Kenny Lau (Jun 26 2019 at 22:45):

this looks like some sort of fubini theorem

Kenny Lau (Jun 26 2019 at 22:54):

let's extract a proof from Billingsley Ch.18

Kenny Lau (Jun 26 2019 at 23:05):

which assumes sigma-finiteness of alpha and beta

Johannes Hölzl (Jun 26 2019 at 23:05):

Yep, this only works for sigma-finite measures. In Isabelle, we first prove that the product measure is measurable: (λx. f x ⨂⇩M g x) ∈ measurable M (subprob_algebra (N ⨂⇩M L)) http://isabelle.in.tum.de/dist/library/HOL/HOL-Probability/Giry_Monad.html (lemma measurable_pair_measure). The proof can be generalized from subprobabilities to sigma-finite measures, it is even enough if one factor of the product is sigma-finite.

Kenny Lau (Jun 26 2019 at 23:06):

does every measurable space have a sigma-finite measure?

Kenny Lau (Jun 26 2019 at 23:06):

and is there a counter-example to the claim measurable (λ (x : α), map (prod.mk x) ν)?

Johannes Hölzl (Jun 26 2019 at 23:13):

it should boil down to the fact that P s := measurable (fun x. (f x <*> g x) s) (where <*> is the product of measures) is closed under complement, i.e. P s --> P (set.univ - s). Now, when the product is finite it translates to measurable (fun x. (f x) univ * (g x) univ - (f x <*> g x) s)

Johannes Hölzl (Jun 26 2019 at 23:15):

We can cover a sigma-finite measure with finite measures, so this works out if both sides of the product are sigma-finite.

Johannes Hölzl (Jun 26 2019 at 23:16):

I thought there was a trick where it is enough that one side is sigma-finite, but I don't remember it.

Johannes Hölzl (Jun 26 2019 at 23:19):

every measurable space has a trivial sigma-finite measure (the null-measure). but we don't talk about measurable spaces, but measurable functions A -> measure B (I guess one can call them Kleisli arrows in the Giry Monad?!)

Kenny Lau (Jun 26 2019 at 23:20):

but in the claim above, alpha doesn't have a measure yet

Johannes Hölzl (Jun 26 2019 at 23:21):

But there is ν

Kenny Lau (Jun 26 2019 at 23:21):

but that's just a measure on beta

Kenny Lau (Jun 26 2019 at 23:22):

if every measurable space has a sigma-finite measure then you can use the trick you forgot

Kenny Lau (Jun 26 2019 at 23:22):

by cooking up a sigma-finite measure on alpha, then let that "one side" be alpha

Kenny Lau (Jun 26 2019 at 23:22):

but since every set has measure zero I dont see how your trick works

Kenny Lau (Jun 26 2019 at 23:22):

maybe you need a non-zero measure

Kenny Lau (Jun 26 2019 at 23:25):

how is this not trivial

Johannes Hölzl (Jun 26 2019 at 23:28):

Maybe a finite counterexample works: Let's assume in A is everything measurable (top) and B is bottom (only univ and empty). And both are isomorphic to bool. Now ν maps each non-empty map to infinity. I'm too tired to figure out what the measurable set is, but I something like this might result in a counter example.

Kenny Lau (Jun 26 2019 at 23:31):

well there are only 4 measurable sets

Kenny Lau (Jun 26 2019 at 23:31):

and I'm sure none of them works

Kenny Lau (Jun 26 2019 at 23:31):

since in A everything is measurable

Kenny Lau (Jun 26 2019 at 23:32):

every function from A is automatically measurable

Kenny Lau (Jun 26 2019 at 23:32):

(and if you swap A and B, still there are only 4 measurable sets and none of them works)

Kenny Lau (Jun 26 2019 at 23:32):

also I'm quite sure there is no finite counter-example, since you can decompose each finite sigma algebra into a disjoint union of tops

Kenny Lau (Jun 26 2019 at 23:38):

tactic failed, there are unsolved goals
state:
α β : Type u,
_inst_1 : measurable_space α,
_inst_2 : measurable_space β,
ν : measure β,
s : set (α × β),
hs : is_measurable s,
t : set ennreal,
ht : t  {s : set ennreal | is_open s}
 is_measurable {x : α | (map (prod.mk x) ν) s  t}

Kenny Lau (Jun 27 2019 at 14:39):

(clearing my sandbox) here's my current status:

import measure_theory.giry_monad
universe u

variables {α : Type u} {β : Type u}

open measure_theory measure_theory.measure

lemma aux [measurable_space α] [measurable_space β] (ν : measure β) (x : α) :
  bind ν (λ (y : β), dirac (x, y)) = ν.map (prod.mk x) :=
ext $ λ s hs,
have h1 : measurable (λ y:β, dirac (x,y)),
from measurable.comp (measurable_prod_mk measurable_const measurable_id) measurable_dirac,
have h2 : (λ (y : β), (dirac (x, y) : measure (α × β)) s) ⁻¹' {0} = set.compl (prod.mk x ⁻¹' s), begin
  ext y, classical,
  rw [set.mem_preimage_eq, dirac_apply _ hs, set.mem_singleton_iff, lattice.supr_eq_if, ennreal.bot_eq_zero],
  split_ifs with h h,
  { exact iff_of_false one_ne_zero (not_not_intro h) },
  { exact iff_of_true rfl h }
end,
have h3 : (λ (y : β), (dirac (x, y) : measure (α × β)) s) ⁻¹' {1} = prod.mk x ⁻¹' s, begin
  ext y, classical,
  rw [set.mem_preimage_eq, dirac_apply _ hs, set.mem_singleton_iff, lattice.supr_eq_if, ennreal.bot_eq_zero],
  split_ifs with h h,
  { exact iff_of_true rfl h },
  { exact iff_of_false zero_ne_one h }
end,
have h4 :  r:ennreal, r  0  r  1  (λ (y : β), (dirac (x, y) : measure (α × β)) s) ⁻¹' {r} = , begin
  intros r hr0 hr1, ext y, classical,
  rw [set.mem_preimage_eq, dirac_apply _ hs, set.mem_singleton_iff, lattice.supr_eq_if, ennreal.bot_eq_zero, set.mem_empty_eq, iff_false],
  split_ifs with h h, exact hr1.symm, exact hr0.symm
end,
have h5 : is_measurable { y:β | (x,y)  s },
from measurable_prod_mk measurable_const measurable_id _ hs,
let sf : simple_func β ennreal :=
{ to_fun := λ y:β, (dirac (x,y) : measure (α × β)) s,
  measurable_sn := λ r, begin
    classical, by_cases hr0 : r = 0,
    { subst hr0, rw h2,
      exact is_measurable.compl h5 },
    by_cases hr1 : r = 1,
    { subst hr1, rw h3, exact h5 },
    rw h4 r hr0 hr1, exact is_measurable.empty
  end,
  finite := set.finite_subset (set.finite_insert _ (set.finite_insert _ set.finite_empty)  : set.finite ({0,1} : set ennreal)) $ begin
    rintros r y, rfl, classical, dsimp only,
    rw [dirac_apply _ hs, lattice.supr_eq_if], split_ifs,
    exacts [set.mem_insert _ _, set.mem_insert_of_mem _ (set.mem_singleton _)]
  end } in
have h6 : sf = simple_func.restrict (simple_func.const β 1) { y | (x,y)  s },
from simple_func.ext $ λ y, show (dirac (x,y) : measure (α × β)) s = _,
by classical; rw [simple_func.restrict_apply _ h5, simple_func.const_apply, dirac_apply _ hs, lattice.supr_eq_if];
dsimp only [set.mem_set_of_eq, ennreal.bot_eq_zero]; split_ifs; refl,
begin
  simp only [bind_apply hs h1],
  rw map_apply (measurable_prod_mk measurable_const measurable_id : measurable (prod.mk x)) hs,
  change integral ν sf = ν { y | (x,y)  s },
  rw [integral, simple_func.lintegral_eq_integral, h6, simple_func.restrict_const_integral, one_mul], refl, exact h5
end

-- set_option pp.implicit true
-- set_option pp.notation false
lemma inl_measurable_bind_ret [measurable_space α] [measurable_space β] (ν : measure β) :
  measurable (λ (x : α), bind ν (λ y, dirac (x,y))) :=
-- measurable_of_measurable_coe _ $ λ s hs,
by simp only [aux]; refine measurable_of_measurable_coe _ (λ s hs, measurable_generate_from $ λ t ht, _);
dsimp only [set.preimage]
-- λ s hs, by dsimp only [measure.measurable_space, lattice.supr, lattice.Sup, lattice.has_Sup.Sup, lattice.conditionally_complete_lattice.Sup,
-- lattice.complete_lattice.Sup, measurable_space.lattice.complete_lattice, galois_insertion.lift_complete_lattice] at hs
-- begin
--   -- apply measurable_of_measurable_coe,
--   -- intros s hs,
--   -- dsimp only [measure_theory.measure.bind, join, of_measurable]
--   -- intros s hs, dsimp only [measurable_space.map, measure_theory.measure.bind, join, of_measurable, dirac]
-- end
set_option pp.implicit false

#print measure_theory.measure.bind
#print outer_measure.dirac
#print measure.measurable_space
#print prod.measurable_space
#print measurable_space.gi_generate_from
#print bind_apply
#check @integral
#check measurable_integral
#check integral_dirac
#check simple_func.lintegral_eq_integral
#print simple_func
#check measurable_dirac
#check measurable_prod_mk
#check simple_func.restrict_const_integral
#check measurable
#check measure.map

#check measurable_generate_from

Mario Carneiro (Jun 27 2019 at 14:44):

Doesn't aux follow from bind_dirac?

Kenny Lau (Jun 27 2019 at 14:44):

I don't know

Mario Carneiro (Jun 27 2019 at 14:48):

Er, I mean this one https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Integral.20of.20a.20constant/near/165952054

Mario Carneiro (Jun 27 2019 at 14:49):

I thought it got PRd but maybe not

Kenny Lau (Jun 27 2019 at 14:53):

that's like 10 times shorter than my proof lol

Koundinya Vajjha (Jun 27 2019 at 14:55):

sorry i missed this discussion last night. @Kenny Lau , are you assuming sigma-finiteness?

Koundinya Vajjha (Jun 27 2019 at 14:55):

Er, I mean this one https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Integral.20of.20a.20constant/near/165952054

yes this was never PR'd

Kenny Lau (Jun 27 2019 at 14:57):

sorry i missed this discussion last night. Kenny Lau , are you assuming sigma-finiteness?

I only know that I need to prove or disprove this:

α β : Type u,
_inst_1 : measurable_space α,
_inst_2 : measurable_space β,
ν : measure β,
s : set (α × β),
hs : is_measurable s
 measurable (λ (b : α), ν {y : β | (b, y)  s})

Mario Carneiro (Jun 27 2019 at 14:58):

What's the status on PRing your stuff @Koundinya Vajjha ? Remember not to build up too much stuff and PR some giant thing. A good strategy is to PR all the stuff that's not actually part of your main work but is missing from other parts of the library

Koundinya Vajjha (Jun 27 2019 at 14:59):

yes I've been putting it off to make it mathlib-ready. i'll get to it soon and yes, will make small PR chunks.

Mario Carneiro (Jun 27 2019 at 15:00):

aka your to_mathlib collection

Koundinya Vajjha (Jun 27 2019 at 15:00):

actually the stuff I need is a little specialized so its not general enough. but i'll PR it anyway so the maintainers can decide

Mario Carneiro (Jun 27 2019 at 15:02):

You can also make a [WIP] PR if you want to expose your current design decisions without making everything ready for merge

Koundinya Vajjha (Jun 27 2019 at 15:28):

Probably putting this question in context will help: I ran into this when I was trying to finish proving that the product measure as returned by the Giry monad has it's expected property: (⇑doₐ (x : α) ←ₐ μ ; doₐ (y : β) ←ₐ ν ; ret (x, y)) (set.prod A B) = ⇑μ A * ⇑ν B
I start off this proof by using a bind_apply.
Which reduces the goal to

α β : Type u,
_inst_1 : measurable_space α,
_inst_2 : measurable_space β,
_inst_3 : nonempty α,
_inst_4 : nonempty β,
μ : measure α,
ν : measure β,
A : set α,
B : set β,
hA : is_measurable A,
hB : is_measurable B
 ((λ (a : α), (doₐ (y : β) ←ₐ ν ; ret (a, y)) (set.prod A B))ðμ) = μ A * ν B

But with the additional goal that ⊢ measurable (λ (x : α), doₐ (y : β) ←ₐ ν ; ret (x, y))

Koundinya Vajjha (Jun 27 2019 at 15:29):

I was able to finish everything except for this final goal.

Koundinya Vajjha (Jun 27 2019 at 15:30):

I guess in hindsight sigma-finiteness is needed to prove this, but I'm not sure how exactly.


Last updated: Dec 20 2023 at 11:08 UTC