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_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 (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