theorem RiemannStieltjes.stieltjesSum_linear_integrand {a b : ℝ} {𝕜 : Type u_1} [NormedField 𝕜] (PT : TaggedPartition a b) (c₁ c₂ : 𝕜) (f₁ f₂ h : ℝ → 𝕜) : stieltjesSum PT (fun (x : ℝ) => c₁ * f₁ x + c₂ * f₂ x) h = c₁ * stieltjesSum PT f₁ h + c₂ * stieltjesSum PT f₂ h

theorem RiemannStieltjes.stieltjesSum_linear_integrator {a b : ℝ} {𝕜 : Type u_1} [NormedField 𝕜] (PT : TaggedPartition a b) (c₁ c₂ : 𝕜) (f g₁ g₂ : ℝ → 𝕜) : (stieltjesSum PT f fun (x : ℝ) => c₁ * g₁ x + c₂ * g₂ x) = c₁ * stieltjesSum PT f g₁ + c₂ * stieltjesSum PT f g₂

theorem RiemannStieltjes.norm_linear_combo_sub {𝕜 : Type u_1} [NormedField 𝕜] (c₁ c₂ A B S₁ S₂ : 𝕜) : ‖c₁ * A + c₂ * B - (c₁ * S₁ + c₂ * S₂)‖ ≤ ‖c₁‖ * ‖A - S₁‖ + ‖c₂‖ * ‖B - S₂‖

theorem RiemannStieltjes.eps_bound {𝕜 : Type u_1} [NormedField 𝕜] (c₁ c₂ : 𝕜) (ε : ℝ) (hε : 0 < ε) : (‖c₁‖ + ‖c₂‖) * (ε / (2 * (‖c₁‖ + ‖c₂‖ + 1))) < ε

theorem RiemannStieltjes.refinement_trans {a b : ℝ} {PT : TaggedPartition a b} {R P : IntervalPartition a b} (hPT : PT.IsRefinementOf R) (hR : R.IsRefinementOf P) : PT.IsRefinementOf P

theorem RiemannStieltjes.abel_summation_tagged_partitions {a b : ℝ} {𝕜 : Type u_1} [NormedField 𝕜] (P : IntervalPartition a b) (f g : ℝ → 𝕜) : ∃ (PT_L : TaggedPartition a b) (PT_R : TaggedPartition a b), PT_L.IsRefinementOf P ∧ PT_R.IsRefinementOf P ∧ stieltjesSum PT_L f g + stieltjesSum PT_R g f = f b * g b - f a * g a

theorem RiemannStieltjes.stieltjesIntegrable_of_parts {a b : ℝ} {𝕜 : Type u_1} [NormedField 𝕜] {f g : ℝ → 𝕜} (hfg : StieltjesIntegrable f g a b) : StieltjesIntegrable g f a b

theorem RiemannStieltjes.integration_by_parts {a b : ℝ} {𝕜 : Type u_1} [NormedField 𝕜] {f g : ℝ → 𝕜} (hfg : StieltjesIntegrable f g a b) : stieltjesIntegral f g a b + stieltjesIntegral g f a b = f b * g b - f a * g a