help with measurability proof

Stream: general

[Koundinya Vajjha]

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]

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]

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

[Chris Hughes]

Is it true?

[Koundinya Vajjha]

i'm about 70% sure

[Jason Rute]

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]

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

[Kenny Lau]

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]

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

[Kenny Lau]

is this even true

[Kenny Lau]

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

[Kenny Lau]

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

[Kenny Lau]

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

[Kenny Lau]

this looks neater

[Kenny Lau]

surely all neat propositions are true

[Kenny Lau]

this looks like some sort of fubini theorem

[Kenny Lau]

let's extract a proof from Billingsley Ch.18

[Kenny Lau]

which assumes sigma-finiteness of alpha and beta

[Johannes Hölzl]

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]

does every measurable space have a sigma-finite measure?

[Kenny Lau]

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

[Johannes Hölzl]

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]

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]

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]

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]

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

[Johannes Hölzl]

But there is ν

[Kenny Lau]

but that's just a measure on beta

[Kenny Lau]

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

[Kenny Lau]

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

[Kenny Lau]

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

[Kenny Lau]

maybe you need a non-zero measure

[Kenny Lau]

how is this not trivial

[Johannes Hölzl]

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]

well there are only 4 measurable sets

[Kenny Lau]

and I'm sure none of them works

[Kenny Lau]

since in A everything is measurable

[Kenny Lau]

every function from A is automatically measurable

[Kenny Lau]

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

[Kenny Lau]

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]

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]

(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]

Doesn't aux follow from bind_dirac?

[Kenny Lau]

I don't know

[Mario Carneiro]

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

[Mario Carneiro]

I thought it got PRd but maybe not

[Kenny Lau]

that's like 10 times shorter than my proof lol

[Koundinya Vajjha]

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

[Koundinya Vajjha]

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]

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]

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]

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]

aka your to_mathlib collection

[Koundinya Vajjha]

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]

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

[Koundinya Vajjha]

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]

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

[Koundinya Vajjha]

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