comment

TestingLowerBounds/Divergences/StatInfo.lean

@@ -1134,4 +1134,8 @@ is needed basically for 2 things:
 For 1. it may be possible to directly generalize the lemma to the case of convexity on an interval (or at least on `Ici 0`), by first generalizing it to a function that is convex on the interval and has right and left derivatives finite at the endpoints, then it should be possibe to generalize this without the finite derivatives, by using the monotone convergence theorem, taking a slightly smaller interval and then taking the limit, however this would require some acrobatics about the integrability condition.
 
 For 2. it is more complicated, it should be possible to generalize the definition of stieltjes measure to the case where the function is convex on some interval (this would deped also on the interval), but then there is the whole API to be generalized, it may be a lot of work. Moreover, it is not clear to me what would be the best way to generalize it, the way I would do it now is by defining a structure (or class?) `IsStieltjesOn` that takes a function `f : ℝ → ℝ` and a set `s` (or should it be the proof that s is convex?) and says that f is monotone and right continuous on `s`, then the curvature measure should be a measure on `univ` that gives zero mass outside of `s` (or should it be a measure on `s` as a separate measurable space?), but how should it behave at the endpoints? (at the right endpoint the function may be discontinuous, is it a problem? at the left endpoint f is continuous, is there any way to make it so the curvature measure at that point is not zero? if there isn't, is this restrictive somehow?)
+What if instead we only generalize it to intervals that are infinite on the right? this would at least avoid the problem of the right endpoint.
+Probably such a measure actually only makes sense on the interval open on the left, that would also take care of the left endpoint.
+Actually the discontinuity at the right is not really a problem, we can probably allow it and go for Ioc or Ioi intervals
+Then should we ask as a hypothesis directly the endpoints of the interval and make two versions, one with the finite interval and the other with the infinite interval? or is there a more clever way to do it?
 -/