## 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.

Is it true?

#### 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?

I don't know

#### 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):

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: May 11 2021 at 21:10 UTC