Implementation of bind for ProbabilityMeasure?

Stream: Is there code for X?

[Harry Goldstein]

The GiryMonad docs talk about how the presentation has been generalized to arbitrary Measures, despite the standard presentation focusing specifically on probability measures. This seems like a reasonable choice, but I was surprised that I couldn't find a version of bind that comes with an appropriate IsProbabilityMeasure proof. I'm relatively new to Mathlib, so there's a chance that I'm just missing something. Or maybe there's a technical reason that this is hard / not possible? Any help would be appreciated.

[Kenny Lau]

@Harry Goldstein Loogle (which everyone should learn) reveals MeasureTheory.Measure.bind. Is this what you're looking for? (Disclaimer, I don't work with this part of the library)

[Harry Goldstein]

I did check Loogle, it's a great tool! Measure.bind implements the functionality I'm after, but if I have a ProbabilityMeasure (which is a Measure satisfying IsProbabilityMeasure) then I don't have a version of bind that maintains the IsProbabilityMeasure proof. At least, not as far as I can tell.

[Bhavik Mehta]

It looks to me that docs#MeasureTheory.Measure.instIsProbabilityMeasureBindCoeKernelOfIsMarkovKernel might be the instance you want

[Harry Goldstein]

Ah that looks like it! I didn't think to search for things to do with kernels. Thank you!

[Bhavik Mehta]

This is what I searched, in case it's helpful in the future: I also didn't think to search for things about kernels!

[Harry Goldstein]

I don't know why I didn't think to search that way! That makes sense. Thanks

[Harry Goldstein]

Hmm. On further inspection this might not quite be what I want? Or if it is, the proof that shows it does what I want is a bit tricky.

import Mathlib.Data.Real.Basic
import Mathlib.MeasureTheory.Measure.GiryMonad
import Mathlib.MeasureTheory.Measure.DiracProba
import Mathlib.Probability.Kernel.Composition.MeasureComp

open MeasureTheory

noncomputable def ProbabilityMeasure.bind
    [MeasurableSpace α]
    [MeasurableSpace β]
    (x : ProbabilityMeasure α)
    (f : α → ProbabilityMeasure β) :
    ProbabilityMeasure β := by
  refine ⟨x.val.bind ((·.val) ∘ f), ?pf⟩
  have x_prop := x.property
  have f_prop a := (f a).property
  let κ := ProbabilityTheory.Kernel.mk (fun a : α => (f a).val) sorry
  have : ProbabilityTheory.IsMarkovKernel κ := ⟨f_prop⟩
  have : IsProbabilityMeasure ((x.val).bind ↑κ) := inferInstance
  assumption

That last inferInstance uses the instance mentioned above, but it requires me to make f a Kernel, and I don't see an easy route there. Anyone have ideas here? Or should I ask elsewhere?

[Aaron Liu]

You need f to be measurable

[David Ledvinka]

Also you should use Measure with IsProbabilityMeasure instances instead of ProbabilityMeasure.

[David Ledvinka]

Perhaps for some more clarity the reason there is no bind for ProbabilityMeasure is that ProbabilityMeasure is only supposed to be used when you are using the topology of weak convergence on the space of probability measures (convergence in distribution). Otherwise you should just use Measure with IsProbabilityMeasure. This way we don't have to duplicate the entire API for probability measures (or finite measures etc...) and all the API for measures also works for them.

[David Ledvinka]

Also you can think of a Kernel as just a function f : α → Measure β with a measurability condition, and that measurability condition is needed to make statements like this true. So whatever your application is there is a good chance you want to be using the language of kernels anyway (and this is the reason there is more API for Kernels then bind directly).