Confusion about MeasureSpace type inference

Stream: new members

[Matthew Ho]

Hi, apologies if the answer to this question is very obvious.

So I tried creating a MeasureSpace, and then tried to create a product of iid measures by creating (Fin n → Ω). I was confused by this, because I didn't specify a joint measure, but it seems that this is a MeasureSpace, and from the below my understanding is that Lean found MeasureSpace.pi and constructed it by taking the product measure.

import Mathlib.MeasureTheory.Measure.Map
import Mathlib.Probability.Kernel.CondDistrib

open MeasureTheory

variable {Ω : Type*}
  [MeasureSpace Ω]

variable (n : ℕ)
#synth MeasureSpace (Fin n → Ω)

How would I have determined that this would have been the default joint measure? (I suppose from a math perspective this is the only measure that makes sense to use without any more information, but I was surprised that there was even was a default.)

Thanks!

[Sébastien Gouëzel]

If you look at the output of your #synth command in the infoview, it tells you that the instance it uses is MeasureSpace.pi. So you can have a look at what this does (for instance by doing #check MeasureSpace.pi and following the symbol)

[Matthew Ho]

Ah, ok, thanks for the help! Stylistically, is it generally better to explicitly specify that I am using MeasureSpace.pi, or is it preferable to allow Lean to infer that this is the right instance to use and not state it?

[Sébastien Gouëzel]

By design, instances are things that Lean will fetch for you automatically. So you should never specify one yourself by hand.

[Matthew Ho]

Thanks very much!