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