2.3: I claim that the definition "m is the infimum of S := ∀x:x≤m⇔x≤S" is better: It should make for prettier proofs, and expresses "m eliminates ∀s∈S for purposes of testing ≤".
Have this marvelously pretty proof of 3b:
Theorem: {monotone, 1-Lipschitz, 0-increasing, concave}
Proof:
is monotone iff . is 1-Lipschitz iff . is 0-increasing iff . is concave iff convex combination:. It thus suffices to show that for enough .
We'd like to say . The first needs precisely that be monotone, which all of the above are. The second is being monotone at the premise. The third is equality when is (which all of the above are), characterizing the very definition of on functions.
Open: Does 3a characterize affine? Can the full set of p for which this goes through be succinctly described?
5c:
I had rejected this answer as unfair. This sort of trolling should be overseen personally.
pg 6 "there exist" -> "there exists"
pg 13 maybe specify that you mean a linear functional that cannot be written as an integral (I quickly jumped ahead after thinking of one where you don't need to take any integrals to evaluate it)
In section 1: When the 'affine' word is commonly used, the mixture coeffecient (denoted there by ) can be any real number. When , then it's still an affine combination, but a more precise tern could be 'convex combination'.
However, as you work with function spaces, convexity in a function space is different then being a convex function, so maybe some new notation should be introduced.
Nitpicks: Def 2.4 builds on the obvious generalisation of Def 2.3, not Def 2.3 itself. Also, Def. 2.3 is a little poorly worded, and should make clear that "not all sets [1]all sets of reals which are bounded below have an infimum". I think it would be helpful for those with no background in proofs if you had an exercise to justify the use of "the" when talking about the supremum of a set. Or even link it to the idea of a lower bound at all.
More to come as I read through this.
EDIT: I think you probably want to point people to guides on how to prove things so that people without maths backgrounds know what task they're meant to be accomplishing. Otherwise they might go through this text and be hopelessly stuck or think they've proven something when they really haven't. Plus, having the ability to notice the difference between a proof and the intuition behind a proof is quite important for doing mathsy stuff, and Vanessa's agenda is amongst the more mathy alignment agendas.
Ignore the struck through text.
I have two questions that may be slightly off-topic and a minor remark:
There have been a few remarks about how my and Vanessa’s posts on Infra-Bayesianism seem interesting, but that it's quite a formidable body of work to chew through.
So anyone interested in learning Inframeasure theory to the level of proficiency where they are actually able to develop their own proofs about it and casually deploy it as a tool on other problems is probably not best served by the existing posts. You can only go so far by reading about something without ever applying it.
And so, to help people get a taste for the underlying math, I have constructed a sheet of exercises analogous to Scott's exercise sheets about fixpoints, to guide the reader through inventing most of the basic theory for themselves.
Said problem sheet was dramatically improved by Jack Parker, Connall Garrod, and Thomas Larsen as part of a SERI project, by including proof sketches, relevant definitions, and commentary, and generally making the whole exercise sheet dramatically more polished than it would otherwise be. Several others also contributed to testing out the exercises and providing solutions and feedback, most prominently, Viktoria Malyasova.
This first sheet focuses on introducing Inframeasures, and working through the Fundamental Theorem of Inframeasures. Admittedly, this is a bit distant from much of the later work (further problem sheets are upcoming), but it is a very important result to have a solid understanding of.
There is more information on how to approach the problems in the introduction of the document. We may potentially release more problem sheets in the future, depending on what the feedback to this one looks like. And if the polished versions are not created, I will publish the unpolished ones.
The link to the problems is right here.