Hi, in my project I have introduced a lot of locales, which are generalizations of oneanother. Specifically i have the hierarchy:
stochastic_process adapted_process progressive_process predictable_process
For each of these locales, I have two additional "instantiations":
nat_stochastic_process = stochastic_process ........
nat_adapted_process = adapted_process ........
real_stochastic_process = stochastic_process ........
real_adapted_process = adapted_process ........
Furthermore, I have two other conditions, one: the underlying filtrations can be sigma finite, two: the codomain of the processes can be ordered banach spaces. Therefore currently I have introduced all possible combinations of locales, ranging from "stochastic_process_order" to "real_sigma_finite_predictable_process_order".
In total, I have around 40-50 locales and 10-20 sublocale relations covering all possible combinations.
Today, I noticed that I also need to consider the case where the measure space is finite, so I need to add at least 40 other locales to cover all possible combinations and also prove all sublocale relations (something like nat_adapted_process nat_stochastic_process is not generated automatically).
From a style perspective, would it make more sense to include all possibilities, or should I only introduce the locales that I will actually use, and leave the rest to others (or me in the future) who will (hopefully) use my formalization for their purposes. I only really need sigma_finite_adapted_process, nat_sigma_finite_predictable_process and a couple more for example.
TLDR; Should I introduce locales for all combinations of type classes, or should I only introduce the locales that I will actually use?
I have decided to take the second path and introduce only those locales that I will directly need. I have deleted all other locale statements to avoid clutter. But please provide me with suggestions if you have any experience with (or opinion on) an issue similar to this.
I think that it mostly depend on your usage.:
I would say that: don't add too many locales as long as you might still be changing them (aka when you follow a math book, this is not too important) and then, add the ones that feel important, but not everything you can
Last updated: Feb 27 2024 at 08:17 UTC