noncomputable def RiemannStieltjes.summatoryFunction (g : ℝ → ℝ) (a x : ℝ) : ℝ

noncomputable def RiemannStieltjes.discreteSum (f g : ℝ → ℝ) (a b : ℝ) : ℝ

def RiemannStieltjes.NotBothDiscAtIntegers (f g : ℝ → ℝ) (a b : ℝ) : Prop

theorem RiemannStieltjes.corollary_18_28 (f g : ℝ → ℝ) (a b : ℝ) (hab : a < b) (hcont : NotBothDiscAtIntegers f g a b) : HasStieltjesIntegral f (summatoryFunction g a) a b (discreteSum f g a b)