structure RiemannStieltjes.IntervalPartition (a b : ℝ) : Type

• n : ℕ
• hn : 0 < self.n
• pts : Fin (self.n + 1) → ℝ
• first : self.pts ⟨0, ⋯⟩ = a
• last : self.pts ⟨self.n, ⋯⟩ = b
• strict_mono : StrictMono self.pts

def RiemannStieltjes.IntervalPartition.IsRefinementOf {a b : ℝ} (P Q : IntervalPartition a b) : Prop

structure RiemannStieltjes.TaggedPartition (a b : ℝ) extends RiemannStieltjes.IntervalPartition a b : Type

• n : ℕ
• hn : 0 < self.n
• pts : Fin (self.n + 1) → ℝ
• first : self.pts ⟨0, ⋯⟩ = a
• last : self.pts ⟨self.n, ⋯⟩ = b
• strict_mono : StrictMono self.pts
• tags : Fin self.n → ℝ
• tag_mem (k : Fin self.n) : self.pts ⟨↑k, ⋯⟩ ≤ self.tags k ∧ self.tags k ≤ self.pts ⟨↑k + 1, ⋯⟩

noncomputable def RiemannStieltjes.stieltjesSum {a b : ℝ} {𝕜 : Type u_1} [NormedField 𝕜] (PT : TaggedPartition a b) (f g : ℝ → 𝕜) : 𝕜

def RiemannStieltjes.HasStieltjesIntegral {𝕜 : Type u_1} [NormedField 𝕜] (f g : ℝ → 𝕜) (a b : ℝ) (S : 𝕜) : Prop

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

theorem RiemannStieltjes.taggedPartitionOfPartition {a b : ℝ} (P : IntervalPartition a b) : ∃ (PT : TaggedPartition a b), PT.toIntervalPartition = P

noncomputable def RiemannStieltjes.IntervalPartition.pointSet {a b : ℝ} (P : IntervalPartition a b) : Finset ℝ

theorem RiemannStieltjes.IntervalPartition.pts_mem_Icc {a b : ℝ} (P : IntervalPartition a b) (i : Fin (P.n + 1)) : P.pts i ∈ Set.Icc a b

theorem RiemannStieltjes.commonRefinement {a b : ℝ} (P Q : IntervalPartition a b) : ∃ (R : IntervalPartition a b), R.IsRefinementOf P ∧ R.IsRefinementOf Q

theorem RiemannStieltjes.hasStieltjesIntegral_unique {a b : ℝ} {𝕜 : Type u_1} [NormedField 𝕜] {f g : ℝ → 𝕜} {S₁ S₂ : 𝕜} (h₁ : HasStieltjesIntegral f g a b S₁) (h₂ : HasStieltjesIntegral f g a b S₂) : S₁ = S₂

noncomputable def RiemannStieltjes.stieltjesIntegral {𝕜 : Type u_1} [NormedField 𝕜] (f g : ℝ → 𝕜) (a b : ℝ) : 𝕜

theorem RiemannStieltjes.stieltjesIntegral_spec {a b : ℝ} {𝕜 : Type u_1} [NormedField 𝕜] {f g : ℝ → 𝕜} (h : StieltjesIntegrable f g a b) : HasStieltjesIntegral f g a b (stieltjesIntegral f g a b)

def RiemannStieltjes.IsBoundedVariation {𝕜 : Type u_1} [NormedField 𝕜] (f : ℝ → 𝕜) (a b : ℝ) : Prop

theorem RiemannStieltjes.stieltjes_eq_riemann (f g g' : ℝ → ℝ) (a b : ℝ) (hg : ∀ x ∈ Set.Icc a b, HasDerivAt g (g' x) x) (hg' : ContinuousOn g' (Set.Icc a b)) (hint : StieltjesIntegrable f g a b) : stieltjesIntegral f g a b = ∫ (x : ℝ) in a..b, f x * g' x

theorem RiemannStieltjes.IsRefinementOf.trans {a b : ℝ} {P Q R : IntervalPartition a b} (hPQ : P.IsRefinementOf Q) (hQR : Q.IsRefinementOf R) : P.IsRefinementOf R

theorem RiemannStieltjes.IsRefinementOf.refl {a b : ℝ} (P : IntervalPartition a b) : P.IsRefinementOf P

noncomputable def RiemannStieltjes.cumRefine {a b : ℝ} (P : ℕ → IntervalPartition a b) (cr : ∀ (Q R : IntervalPartition a b), ∃ (S : IntervalPartition a b), S.IsRefinementOf Q ∧ S.IsRefinementOf R) : ℕ → IntervalPartition a b

theorem RiemannStieltjes.cumRefine_refines_prev {a b : ℝ} (P : ℕ → IntervalPartition a b) (cr : ∀ (Q R : IntervalPartition a b), ∃ (S : IntervalPartition a b), S.IsRefinementOf Q ∧ S.IsRefinementOf R) (n : ℕ) : (cumRefine P cr (n + 1)).IsRefinementOf (cumRefine P cr n)

theorem RiemannStieltjes.cumRefine_refines_P {a b : ℝ} (P : ℕ → IntervalPartition a b) (cr : ∀ (Q R : IntervalPartition a b), ∃ (S : IntervalPartition a b), S.IsRefinementOf Q ∧ S.IsRefinementOf R) (n : ℕ) : (cumRefine P cr (n + 1)).IsRefinementOf (P (n + 1))

theorem RiemannStieltjes.cumRefine_refines_P_le {a b : ℝ} (P : ℕ → IntervalPartition a b) (cr : ∀ (Q R : IntervalPartition a b), ∃ (S : IntervalPartition a b), S.IsRefinementOf Q ∧ S.IsRefinementOf R) (n k : ℕ) (hk : k ≤ n) : (cumRefine P cr n).IsRefinementOf (P k)

theorem RiemannStieltjes.integrable_of_cauchy (f g : ℝ → ℝ) (a b : ℝ) (hcauchy : ∀ ε > 0, ∃ (P : IntervalPartition a b), ∀ (PT₁ PT₂ : TaggedPartition a b), PT₁.IsRefinementOf P → PT₂.IsRefinementOf P → ‖stieltjesSum PT₁ f g - stieltjesSum PT₂ f g‖ < ε) : StieltjesIntegrable f g a b

theorem RiemannStieltjes.cauchyStieltjes (f g : ℝ → ℝ) (a b : ℝ) (hf_bv : IsBoundedVariation f a b) (hg_bv : IsBoundedVariation g a b) (hf_left : ∀ c ∈ Set.Icc a b, Filter.Tendsto f (nhdsWithin c (Set.Iio c)) (nhds (f c))) (hg_right : ∀ c ∈ Set.Icc a b, Filter.Tendsto g (nhdsWithin c (Set.Ioi c)) (nhds (g c))) (ε : ℝ) : ε > 0 → ∃ (P : IntervalPartition a b), ∀ (PT₁ PT₂ : TaggedPartition a b), PT₁.IsRefinementOf P → PT₂.IsRefinementOf P → ‖stieltjesSum PT₁ f g - stieltjesSum PT₂ f g‖ < ε

theorem RiemannStieltjes.stieltjesIntegrable_of_boundedVariation (f g : ℝ → ℝ) (a b : ℝ) (hf_bv : IsBoundedVariation f a b) (hg_bv : IsBoundedVariation g a b) (hf_left : ∀ c ∈ Set.Icc a b, Filter.Tendsto f (nhdsWithin c (Set.Iio c)) (nhds (f c))) (hg_right : ∀ c ∈ Set.Icc a b, Filter.Tendsto g (nhdsWithin c (Set.Ioi c)) (nhds (g c))) : StieltjesIntegrable f g a b

theorem RiemannStieltjes.fin_sum_telescope {n : ℕ} (g : Fin (n + 1) → ℝ) : ∑ i : Fin n, (g ⟨↑i + 1, ⋯⟩ - g ⟨↑i, ⋯⟩) = g ⟨n, ⋯⟩ - g ⟨0, ⋯⟩