Integration by parts for Stieltjes functions

Stream: Is there code for X?

[Lorenzo Luccioli]

In our project @Rémy Degenne and I would need a version of the integration by parts theorem for Stieltjes functions, the statement would be something like this (see also the file in the project):

import Mathlib.MeasureTheory.Integral.IntervalIntegral

lemma integral_stieltjes_meas_by_parts (f g : StieltjesFunction) (a b : ℝ) :
    ∫ x in a..b, f x ∂g.measure = (f b) * (g b) - (f a) * (g a) - ∫ x in a..b, g x ∂f.measure := by
  sorry

I think this is not in mathlib yet, but I was wondering if anyone has a version of this in a separate repo or is looking for ideas for a project.

In case anyone is interested in trying to prove it, here are some possible references:

• This link.
• Mathematical Analysis, Tom M. Apostol, 5th edition, Theorem 7.6, page 144.
• The Integrals of Lebesgue, Denjoy, Perron, and Henstock, Theorem 12.14.