# Zulip Chat Archive

## Stream: general

### Topic: probability_theory namespace

#### Jason KY. (Sep 30 2022 at 11:07):

Currently, files in the probability folder are either in the `measure_theory`

(files on martingales) or the `probability_theory`

(independence and SLLN files) namespace. There were some discussions in #16517 which said we should change to the `probability_theory`

namespace for the entire folder.

I am currently rewriting the definition of variance (as discussed here) which lives in the `probability_theory`

namespace and I would like to make a lemma using dot notation in the form of `mem_ℒp.foo`

. But since everything in that namespace is in `probability_theory`

, I have to name the lemma `_root_.measure_theory.mem_ℒp.foo`

in order for the dot notation to work. I feel like this situation will come up quite often so I think we should have everything in the probability folder to live in the `measure_theory`

namespace in contrast to what was said in #16517. Is this a reasonable argument?

#### Vincent Beffara (Sep 30 2022 at 11:22):

I guess the alternative is to say that `mem_ℒp.foo`

belongs in the measure theory folder and not in the probability one. Do you want to put it there because the proof uses some probability?

#### Jason KY. (Sep 30 2022 at 11:29):

It is a lemma about `variance`

so I don't think it should go in the measure theory folder

#### Sebastien Gouezel (Sep 30 2022 at 11:48):

I don't see any problem with having lemmas named `_root_.something`

. It happens quite frequently in fact.

Last updated: Dec 20 2023 at 11:08 UTC