Commit 2024-05-22 06:25 4ae950b7

chore: fix variables declarations in probability theory files (#13084) When we have a measure around, it's better to declare {_ : MeasurableSpace Ω} than [MeasurableSpace Ω] because, when there are several measurable space structures around (as is often the case with conditional expectations), this ensures that the right one will be picked automatically. This PR enforces this design in several probability theory files, and uses this occasion to cleanup variable declaration in these files. This makes it possible to remove a bunch of lines set_option backward.synthInstance.canonInstances false in. No statement added or removed or changed, only variable management.