Analysis I, Section 11.8: The Riemann-Stieltjes integral

I have attempted to make the translation as faithful a paraphrasing as possible of the original text. When there is a choice between a more idiomatic Lean solution and a more faithful translation, I have generally chosen the latter. In particular, there will be places where the Lean code could be "golfed" to be more elegant and idiomatic, but I have consciously avoided doing so.

Main constructions and results of this section:

• Definition of α-length.

• The piecewise constant Riemann-Stieltjes integral.

• The full Riemann-Stieltjes integral.

Technical notes:

• In Lean it is more convenient to make definitions such as α-length and the Riemann-Stieltjes integral totally defined, thus assigning "junk" values to the cases where the definition is not intended to be applied. For the definition of α-length, the definition is intended to be applied in contexts where left and right limits exist, and the function is extended by constants to the left and right of its intended domain of definition; for instance, if a function Unknown identifier `f`f is defined on Unknown identifier `Icc`Icc 0 1, then it is intended that Unknown identifier `f`sorry = sorry : Propf x = Unknown identifier `f`f 1 for all Unknown identifier `x`sorry ≥ 1 : Propx ≥ 1 and Unknown identifier `f`sorry = sorry : Propf x = Unknown identifier `f`f 0 for all Unknown identifier `x`sorry ≤ 0 : Propx ≤ 0; in particular, at a right endpoint, the value of a function is intended to agree with its right limit, and similarly for the left endpoint, although we do not enforce this in our definition of α-length. (For functions defined on open intervals, the extension is immaterial.)

• The notion of α-length and piecewise constant Riemann-Stieltjes integral is intended for situations where left and right limits exist, such as for monotone functions or continuous functions, though technically they make sense without these hypotheses. The full Riemann-Stieltjes integral is intended for functions that are of bounded variation, though we shall restrict attention to the special case of monotone increasing functions for the most part.