bundle sigma-algebra with a type

Stream: Is there code for X?

[Lua Viana Reis]

Is there a better way to do this? It feels like a common pattern?

import Mathlib

/-- A type tag for `α` with `MeasurableSet`. -/
@[nolint unusedArguments]
def MeasurableType (α : Type*) (m : MeasurableSpace α) : Type _ := α

instance : MeasurableSpace (MeasurableType α m) := m

The context is, if I don't do that, I run into the "synthesized type class instance is not definitionally equal to expression inferred by typing rules" error when using the condKernel API... even if I try to be very explicit in the type annotations

import Mathlib.Probability.Kernel.Disintegration.StandardBorel
namespace MeasureTheory.Measure

variable {α : Type*} {m m₀ : MeasurableSpace α}

variable (m) in
noncomputable def condProd (μ : Measure[m₀] α) : Measure[m.prod m₀] (α × α) :=
  @μ.map _ _ _ (m.prod m₀) fun x => (x, x)

def condMeas (μ : Measure[m₀] α) (m : MeasurableSpace α) (x : α) : Measure[m₀] α :=
  -- does not work
  let s := (μ.condProd m).condKernel (mα := m)
  sorry

[Aaron Liu]

this isn't just a problem with measurable spaces

[Kenny Lau]

Lua Viana Reis said:

even if I try to be very explicit in the type annotations

in general that's not the way to solve it

[Aaron Liu]

@Kenny Lau it sounds like you have a solution?

[Aaron Liu]

("don't have diamonds" is not good enough for me)

[Lua Viana Reis]

Kenny Lau said:

in general that's not the way to solve it

Is it a fault in the existing condMeas API then? In this case, I expected (mα := m) to make it work, but it still does not. Is there some flag to help me find where the conflict is?

[Lua Viana Reis]

if I made it work with type annotations first, I would be happy to at least find where is the problem

[Kenny Lau]

@Lua Viana Reis could you be more clear on which synthesized instance is conflicting with which inferred instance?

[Kenny Lau]

without that information, I would say, turn the default instance off using attribute [-instance] xxx

[Lua Viana Reis]

sorry, I think I found the problem in this case!

[Lua Viana Reis]

but perhaps condKernel should make the other one of the MeasurableSpace parameters named, so it's easier to specify

[Aaron Liu]

Kenny Lau said:

without that information, I would say, turn the default instance off using attribute [-instance] xxx

what if it's a local variable

[Kenny Lau]

I don't know without more context

[Lua Viana Reis]

In what I sent above, the context is m0 is the "base" sigma-algebra and m is a sub-sigma-algebra, I want to disintegrate a Measure[m0] over m. To do that, I push the measure to $\alpha \times \alpha$, but with the m.prod m0 algebra. Now, I want to disintegrate into a the conditional kernel $\alpha \to \mathsf{Measure}\;\alpha$, which is measurable with respect to m, and they are called the conditional measures.

[Lua Viana Reis]

Basically: I certainly have to deal with at least two different sub-sigma-algebras in code related to that, and it would be better if Lean didn't try to be smart about using typeclass instances but failed

[Etienne Marion]

It's not trying to be smart actually, it's just that if the argument is to be synthesized by typeclass inference it will use the last one introduced, so in your case m. But specifying things explicitely works.

import Mathlib.Probability.Kernel.Disintegration.StandardBorel
namespace MeasureTheory.Measure

variable {α : Type*} {m m₀ : MeasurableSpace α} [@StandardBorelSpace α m₀] [Nonempty α]

variable (m) in
noncomputable def condProd (μ : Measure[m₀] α) : Measure[m.prod m₀] (α × α) :=
  @μ.map _ _ _ (m.prod m₀) fun x => (x, x)
#check condProd
def condMeas (μ : Measure[m₀] α) (m : MeasurableSpace α) (x : α) : Measure[m₀] α := by
  -- does not work
  let s := @Measure.condKernel α α m m₀ inferInstance inferInstance (μ.condProd m)
  sorry

[Lua Viana Reis]

But this is the problem, I think. If the argument was implicit instead of a typeclass argument, it would find the right algebra and not complain.

[Etienne Marion]

It is a typeclass argument here because as the space is required to be standard Borel, there can only be one sigma-algebra on it, ie the Borel one. But of course this breaks if alpha = Omega. You might open a pull request to change that, it is quite frequent that we turn typeclass MeasurableSpace arguments into implicit arguments precisely because of this issue.

[Lua Viana Reis]

Etienne Marion said:

there can only be one sigma-algebra on it, ie the Borel one

This is not exactly true, right? The StandardBorelSpace does not require the topology beforehand, and instead says there exist one. And often, subalgebras are Borel too

[Etienne Marion]

You're right I mixed it up with the case where the hypothesis is BorelSpace.

[Lua Viana Reis]

I can confirm that changing [MeasurableSpace Ω] to {mΩ : MeasurableSpace Ω} in Mathlib.Probability.Kernel.Disintegration.StandardBorel makes the code above work, and Mathlib still compiles.

[Etienne Marion]

Yes that's expected because the measurable space structure can be inferred from the measure. As I said this kind of change is quite frequent as we often bump into this issue (although it gets rarer as time passes).

[Etienne Marion]

Probably nobody tried to use condKernel with the two spaces being the same before you so the issue went unnoticed.

[Rémy Degenne]

Please open a PR for the change! Whenever a MeasurableSpace can be inferred from a Measure, the argument should be implicit and not an instance. Precisely because of the issues you encountered.

[Lua Viana Reis]

#31071