probability_theory namespace

Stream: general

[Jason KY.]

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_theorynamespace 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]

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.]

It is a lemma about variance so I don't think it should go in the measure theory folder

[Sebastien Gouezel]

I don't see any problem with having lemmas named _root_.something. It happens quite frequently in fact.