Timeline for How do we express measurable spaces using type theory?
Current License: CC BY-SA 3.0
15 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| May 10, 2017 at 15:14 | history | edited | Jason Rute | CC BY-SA 3.0 |
fixed math typo
|
| May 10, 2017 at 10:43 | comment | added | Jules | Do you mean X -> Bool instead of Bool -> X? | |
| Jul 14, 2013 at 11:50 | comment | added | Jason Rute | @TomLaGatta, I added a update at the bottom of my answer based on your comment. (Sorry it took me a month. I have been quite busy lately.) | |
| Jul 14, 2013 at 11:49 | history | edited | Jason Rute | CC BY-SA 3.0 |
Added an new section on
|
| Jun 20, 2013 at 21:24 | comment | added | Tom LaGatta | My hope is to eventually compute with arbitrary hierarchies of probability spaces (e.g., measures on spaces of measures on spaces of measures, etc.). This is of importance in epistemic game theory, where topological assumptions seem quite contrived. I do not have a specific, concrete application in mind at the moment, but as I move down the path of agent-based modeling in practice something will surely come up. Thank you very much for the nice answer & comments, and the offer of assistance. Cheers! | |
| Jun 20, 2013 at 21:22 | comment | added | Tom LaGatta | Thanks very much, @Jason. I'm dubious about the necessity of topological for meaningful computations. Statements like, "Everything else ... has little practical value" raise red flags. Maybe there's no application yet, but it's hard for me to believe that there never would be one. | |
| Jun 19, 2013 at 7:17 | comment | added | Jason Rute | @Tom, I added an update after that paragraph you were interested in more. However, having said this, I really still have no idea what you are trying to do, so I can't give too much help. If you are able to get your project to work, I would be really curious how it goes. (You could contact me personally.) | |
| Jun 19, 2013 at 7:13 | history | edited | Jason Rute | CC BY-SA 3.0 |
Added update
|
| Jun 19, 2013 at 6:51 | comment | added | Jason Rute | Moreover, I specialize in the computability of probability theory (at the most high level: what is and is not computable). Anything practical in probability seems to be doable on the Borel probability measure on a complete separable metric space. Everything else is just mathematical generalization that has little practical value. | |
| Jun 19, 2013 at 6:48 | comment | added | Jason Rute | @Tom, while it is true that there are weird sigma-algebras and weird sets, I don't think they have any value in computation. Computation is actually a very topological thing. A computation in some sense has to be continuous. I admit, I still don't know what applications you are looking for. What could you reasonably compute about a sigma-algebra on ${0,1}^\mathbb{R}$? From a computational perspective, ${0,1}^\mathbb{R}$ is much too big, unless I am misunderstanding your applications. | |
| Jun 19, 2013 at 4:59 | comment | added | Tom LaGatta | Can you expand on this statement? "Given a type X, you can make a new type 𝚂𝚒𝚐𝚖𝚊𝙰𝚕𝚐𝚎𝚋𝚛𝚊(X) that depends on X, and can be understood as the sigma-algebras of X. Rather than going into the details, it is important to note that this is all a formalism. If I know nothing about X then I only know the most basic properties about 𝚂𝚒𝚐𝚖𝚊𝙰𝚕𝚐𝚎𝚋𝚛𝚊(X)." | |
| Jun 19, 2013 at 4:56 | comment | added | Tom LaGatta | @Jason: thank you so much for the comprehensive answer. I want to be able to compute things in terms of probabilities. Obviously I won't be evaluating a measure on every possible measurable set, but I want to have a guarantee that I can at least measure a wide class of sets. Incidentally, neither approach you propose works in general, since both are rooted in topological measurable spaces. But there are plenty of reasonable spaces which do not admit topologically generated $\sigma$-algebras. e.g., $\{0,1\}^{\mathbb R}$, see this question: mathoverflow.net/questions/87838 | |
| Jun 19, 2013 at 4:52 | vote | accept | Tom LaGatta | ||
| Jun 18, 2013 at 23:23 | history | edited | Jason Rute | CC BY-SA 3.0 |
added 3 characters in body; added 15 characters in body
|
| Jun 18, 2013 at 23:16 | history | answered | Jason Rute | CC BY-SA 3.0 |