Riemann–Stieltjes and Riemann integrals

In this file we give some API for intervals (using the type BoxIntegral.Box (Fin 1)), and use this to define the (one-dimensional) Riemann–Stieltjes integral ∫ˢ x in a..b, f x ∂[B; g] from a to b of a function f : ℝ → E against an integrator g : ℝ → F, paired by a continuous bilinear map B : E →L[ℝ] F →L[ℝ] G. It is not required that a < b.

The notation here is deliberately chosen to mimic the notation ∫ x in a..b, f x ∂μ for IntervalIntegral, as well as the notation ∫ᵛ x, f x ∂[B; μ] for MeasureTheory.VectorMeasure.Integral.

The bilinear pairing B covers the three main variants of Stieltjes integration that appear in practice:

• f scalar, g vector-valued (B = .lsmul ℝ ℝ): notation ∫ˢ x in a..b, f x ∂•g.
• f vector-valued, g scalar (B = (.lsmul ℝ ℝ).flip): notation ∫ˢ x in a..b, f x ∂<•g.
• f and g both real or both complex (B = .mul ℝ E): no dedicated shorthand; use the general ∫ˢ x in a..b, f x ∂[B; g].

The . here can be removed if ContinuousLinearMap is open.

The Riemann integral is the special case F = ℝ, B = (.lsmul ℝ ℝ).flip and g = id, and is denoted ∫ʳ x in a..b, f x.

Key definitions

• interval hab: the one-dimensional interval (a, b] as a Box (Fin 1), given a proof of hab : a < b.
• BoxAdditiveMap.increment g: the box-additive map on Box (Fin 1) defined by J ↦ g J.upper₁ - g J.lower₁, where g : ℝ → M is a function to an additive commutative group M.
• BoxIntegral.StieltjesIntegrable a b B f g: the predicate that the integral ∫ˢ x in a..b, f x ∂[B; g] exists.
• BoxIntegral.HasStieltjesIntegral a b B f g L: the predicate that the integral ∫ˢ x in a..b, f x ∂[B; g] exists and equals L.
• BoxIntegral.stieltjesIntegral a b B f g: the value of ∫ˢ x in a..b, f x ∂[B; g] if it exists, or the junk value of 0 otherwise.
• BoxIntegral.RiemannIntegrable a b f: the predicate that the Riemann integral ∫ʳ x in a..b, f x exists.
• BoxIntegral.HasRiemannIntegral a b f L: the predicate that the Riemann integral ∫ʳ x in a..b, f x exists and equals L.
• BoxIntegral.riemannIntegral a b f: the value of ∫ʳ x in a..b, f x if it exists, or the junk value of 0 otherwise.

These notions are named in analogy with BoxIntegral.Integrable, BoxIntegral.HasIntegral, and BoxIntegral.integral.

Thanks to ICERM for hosting the workshop "Formalization of Analysis" where most of this work was conducted.

Usage

Some very basic API is provided in this file. More extensive API may be found at https://github.com/leanprover-community/mathlib-at-ICERM26/tree/stieltjes . However, unless one is specifically interested in the Riemann aspect of integration theory, it is recommended that one instead use the more general integration API already in Mathlib, specifically MeasureTheory.Integral.Bochner (for integration against non-negative measures) or MeasureTheory.VectorMeasure (to handle Lebesgue--Stieltjes) type integrals.

Tags

Stieltjes integral, Riemann–Stieltjes, Riemann integral

One-dimensional intervals

Ioc intervals can be represented within the BoxIntegral API as objects of type Box (Fin 1). We provide some minimal API for manipulating such intervals.

Note: one could use Equiv.funUnique (Fin 1) ℝ instead of using the maps x ↦ x 0 and x ↦ ![x] to identify Fin 1 → ℝ and ℝ, but this does not seem to gain very much.

def BoxIntegral.Box.lower₁ (J : Box (Fin 1)) : ℝ

The left endpoint of a one-dimensional box.

Equations

• J.lower₁ = J.lower 0

def BoxIntegral.Box.upper₁ (J : Box (Fin 1)) : ℝ

The right endpoint of a one-dimensional box.

Equations

• J.upper₁ = J.upper 0

theorem BoxIntegral.Box.lower_lt_upper₁ (J : Box (Fin 1)) : J.lower₁ < J.upper₁

@[simp]

theorem BoxIntegral.Box.le_iff₁ (J J' : Box (Fin 1)) : J ≤ J' ↔ J'.lower₁ ≤ J.lower₁ ∧ J.upper₁ ≤ J'.upper₁

noncomputable def BoxIntegral.interval {a b : ℝ} (hab : a < b) : Box (Fin 1)

One-dimensional Ioc interval as a Box (Fin 1)

Equations

• BoxIntegral.interval hab = { lower := ![a], upper := ![b], lower_lt_upper := ⋯ }

@[simp]

theorem BoxIntegral.interval_lower {a b : ℝ} (hab : a < b) : (interval hab).lower₁ = a

@[simp]

theorem BoxIntegral.interval_upper {a b : ℝ} (hab : a < b) : (interval hab).upper₁ = b

@[simp]

theorem BoxIntegral.Icc_interval {a b : ℝ} (hab : a < b) : Box.Icc (interval hab) = {x : Fin 1 → ℝ | x 0 ∈ Set.Icc a b}

The increment of a function on ℝ as a box-additive map

def BoxIntegral.BoxAdditiveMap.incrementAux {M : Type u_1} [AddCommGroup M] (g : ℝ → M) : BoxAdditiveMap (Fin 1) M ⊤

Underlying construction for increment: sends g : ℝ → M to the box-additive map on Box (Fin 1) defined by J ↦ g J.upper₁ - g J.lower₁.

Equations

• BoxIntegral.BoxAdditiveMap.incrementAux g = BoxIntegral.BoxAdditiveMap.ofMapSplitAdd (fun (J : BoxIntegral.Box (Fin 1)) => g J.upper₁ - g J.lower₁) ⊤ ⋯

def BoxIntegral.BoxAdditiveMap.increment {M : Type u_1} [AddCommGroup M] : (ℝ → M) →+ BoxAdditiveMap (Fin 1) M ⊤

The box-additive increment sending a function g : ℝ → M to the box-additive map on Box (Fin 1) defined by J ↦ g J.upper₁ - g J.lower₁, bundled as an AddMonoidHom.

Equations

• BoxIntegral.BoxAdditiveMap.increment = { toFun := BoxIntegral.BoxAdditiveMap.incrementAux, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem BoxIntegral.BoxAdditiveMap.increment_apply {M : Type u_1} [AddCommGroup M] (g : ℝ → M) (J : Box (Fin 1)) : (increment g) J = g J.upper₁ - g J.lower₁

@[simp]

theorem BoxIntegral.BoxAdditiveMap.increment_smul {M : Type u_1} [AddCommGroup M] {R : Type u_2} [Monoid R] [DistribMulAction R M] (c : R) (g : ℝ → M) : increment (c • g) = c • increment g

theorem BoxIntegral.BoxAdditiveMap.increment_lsmul_eq_volume {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] : (increment fun (x : ℝ) => (ContinuousLinearMap.lsmul ℝ ℝ) x) = BoxAdditiveMap.volume

The increment of ContinuousLinearMap.lsmul ℝ ℝ : ℝ → (E →L[ℝ] E) equals the Lebesgue volume box-additive map on Box (Fin 1).

Definition of the Riemann--Stieltjes integral

def RiemannStieltjes.HasStieltjesIntegralOrdered {E : Type u_1} {F : Type u_2} {G : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] (a b : ℝ) (B : E →L[ℝ] F →L[ℝ] G) (f : ℝ → E) (g : ℝ → F) (L : G) (hab : a < b) : Prop

The (Riemann--)Stieltjes integral predicate of a function f : ℝ → E and g : ℝ → F having its Riemann--Stieltjes sums converge to a limit L : G, given a bilinear map B : E → F → G and endpoints a, b takes values in G. Initially defined under the implicit assumption that a < b.

Equations

• One or more equations did not get rendered due to their size.

def RiemannStieltjes.HasStieltjesIntegral {E : Type u_1} {F : Type u_2} {G : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] (a b : ℝ) (B : E →L[ℝ] F →L[ℝ] G) (f : ℝ → E) (g : ℝ → F) (L : G) : Prop

Extension of HasStieltjesIntegralOrdered to cover the cases a = b and a > b.

Equations

• One or more equations did not get rendered due to their size.

def RiemannStieltjes.StieltjesIntegrable {E : Type u_1} {F : Type u_2} {G : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] (a b : ℝ) (B : E →L[ℝ] F →L[ℝ] G) (f : ℝ → E) (g : ℝ → F) : Prop

StieltjesIntegrable a b B f g asserts that the Riemann–Stieltjes integral of f against g paired by B from a to b exists, i.e. some L satisfies HasStieltjesIntegral a b B f g L.

Equations

• RiemannStieltjes.StieltjesIntegrable a b B f g = ∃ (L : G), RiemannStieltjes.HasStieltjesIntegral a b B f g L

noncomputable def RiemannStieltjes.stieltjesIntegral {E : Type u_1} {F : Type u_2} {G : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] (a b : ℝ) (B : E →L[ℝ] F →L[ℝ] G) (f : ℝ → E) (g : ℝ → F) : G

The Riemann–Stieltjes integral of f against g paired by B from a to b. Returns the junk value 0 if no such integral exists. The integral remains meaningful outside of the case a < b.

Equations

• RiemannStieltjes.stieltjesIntegral a b B f g = if h : RiemannStieltjes.StieltjesIntegrable a b B f g then Exists.choose h else 0

def RiemannStieltjes.«term∫ˢ_In_.._,_∂[_;_]» : Lean.ParserDescr

Notation ∫ˢ x in a..b, f x ∂[B; g] for the Riemann–Stieltjes integral of f against the integrator g, paired by the bilinear map B. Mirrors the vector-measure integral notation ∫ᵛ x, f x ∂[B; μ], and parallels ∫ x in a..b, f x ∂μ for intervalIntegral.

Equations

• One or more equations did not get rendered due to their size.

def RiemannStieltjes.«term∫ˢ_In_.._,_∂•_» : Lean.ParserDescr

The special case of ∫ˢ x in a..b, f x ∂[B; g] with f real-valued, g vector-valued, and B = ContinuousLinearMap.lsmul ℝ ℝ.

Equations

• One or more equations did not get rendered due to their size.

def RiemannStieltjes.«term∫ˢ_In_.._,_∂<•_» : Lean.ParserDescr

The special case of ∫ˢ x in a..b, f x ∂[B; g] with f vector-valued, g real-valued, and B = (ContinuousLinearMap.lsmul ℝ ℝ).flip.

Equations

• One or more equations did not get rendered due to their size.

The Riemann integral

def RiemannStieltjes.HasRiemannIntegral {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (a b : ℝ) (f : ℝ → E) (L : E) : Prop

HasRiemannIntegral a b f L is defined to equal HasStieltjesIntegral a b (lsmul ℝ ℝ).flip f id L. Use unfold HasRiemannIntegral or similar to access the Stieltjes integral API.

Equations

• RiemannStieltjes.HasRiemannIntegral a b f L = RiemannStieltjes.HasStieltjesIntegral a b (ContinuousLinearMap.lsmul ℝ ℝ).flip f id L

def RiemannStieltjes.RiemannIntegrable {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (a b : ℝ) (f : ℝ → E) : Prop

RiemannIntegrable a b f is defined to equal StieltjesIntegrable a b (lsmul ℝ ℝ).flip f id. Use unfold RiemannIntegrable or similar to access the Stieltjes integral API.

Equations

• RiemannStieltjes.RiemannIntegrable a b f = RiemannStieltjes.StieltjesIntegrable a b (ContinuousLinearMap.lsmul ℝ ℝ).flip f id

noncomputable def RiemannStieltjes.riemannIntegral {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (a b : ℝ) (f : ℝ → E) : E

riemannIntegral a b f, with notation ∫ʳ x in a..b, f x, is defined to equal ∫ˢ x in a..b, f x ∂<•id. Use unfold riemannIntegral or similar to access the Stieltjes integral API. One could relate riemannIntegral to intervalIntegral under suitable hypotheses on f; see https://github.com/leanprover-community/mathlib-at-ICERM26/blob/stieltjes/Mathlib/Analysis/BoxIntegral/Stieltjes/Measure.lean

Equations

• RiemannStieltjes.riemannIntegral a b f = RiemannStieltjes.stieltjesIntegral a b (ContinuousLinearMap.lsmul ℝ ℝ).flip (fun (x : ℝ) => f x) id

def RiemannStieltjes.«term∫ʳ_In_.._,_» : Lean.ParserDescr

riemannIntegral a b f, with notation ∫ʳ x in a..b, f x, is defined to equal ∫ˢ x in a..b, f x ∂<•id. Use unfold riemannIntegral or similar to access the Stieltjes integral API. One could relate riemannIntegral to intervalIntegral under suitable hypotheses on f; see https://github.com/leanprover-community/mathlib-at-ICERM26/blob/stieltjes/Mathlib/Analysis/BoxIntegral/Stieltjes/Measure.lean

Equations

• One or more equations did not get rendered due to their size.

Simple properties

@[simp]

theorem RiemannStieltjes.HasStieltjesIntegral.of_eq_iff_zero {E : Type u_1} {F : Type u_2} {G : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {a : ℝ} {B : E →L[ℝ] F →L[ℝ] G} {f : ℝ → E} {g : ℝ → F} {L : G} : HasStieltjesIntegral a a B f g L ↔ L = 0

theorem RiemannStieltjes.HasStieltjesIntegral.of_lt {E : Type u_1} {F : Type u_2} {G : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {a b : ℝ} {B : E →L[ℝ] F →L[ℝ] G} {f : ℝ → E} {g : ℝ → F} {L : G} (hab : a < b) : HasStieltjesIntegral a b B f g L ↔ HasStieltjesIntegralOrdered a b B f g L hab

@[simp]

theorem RiemannStieltjes.HasStieltjesIntegral.of_gt {E : Type u_1} {F : Type u_2} {G : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {a b : ℝ} {B : E →L[ℝ] F →L[ℝ] G} {f : ℝ → E} {g : ℝ → F} {L : G} (hba : b < a) : HasStieltjesIntegral a b B f g L ↔ HasStieltjesIntegralOrdered b a B f g (-L) hba

theorem RiemannStieltjes.HasStieltjesIntegral.symm_iff {E : Type u_1} {F : Type u_2} {G : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {a b : ℝ} {B : E →L[ℝ] F →L[ℝ] G} {f : ℝ → E} {g : ℝ → F} {L : G} : HasStieltjesIntegral a b B f g L ↔ HasStieltjesIntegral b a B f g (-L)

theorem RiemannStieltjes.HasStieltjesIntegral.symm {E : Type u_1} {F : Type u_2} {G : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {a b : ℝ} {B : E →L[ℝ] F →L[ℝ] G} {f : ℝ → E} {g : ℝ → F} {L : G} (h : HasStieltjesIntegral a b B f g L) : HasStieltjesIntegral b a B f g (-L)

theorem RiemannStieltjes.stieltjesIntegrable_iff_integrable_of_lt {E : Type u_1} {F : Type u_2} {G : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {a b : ℝ} {B : E →L[ℝ] F →L[ℝ] G} {f : ℝ → E} {g : ℝ → F} (hab : a < b) : StieltjesIntegrable a b B f g ↔ BoxIntegral.Integrable (BoxIntegral.interval hab) BoxIntegral.IntegrationParams.Riemann (fun (x : Fin 1 → ℝ) => f (x 0)) (BoxIntegral.BoxAdditiveMap.increment fun (x : ℝ) => B.flip (g x))

@[simp]

theorem RiemannStieltjes.StieltjesIntegrable.of_eq {E : Type u_1} {F : Type u_2} {G : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {a : ℝ} {B : E →L[ℝ] F →L[ℝ] G} {f : ℝ → E} {g : ℝ → F} : StieltjesIntegrable a a B f g

theorem RiemannStieltjes.StieltjesIntegrable.symm_iff {E : Type u_1} {F : Type u_2} {G : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {a b : ℝ} {B : E →L[ℝ] F →L[ℝ] G} {f : ℝ → E} {g : ℝ → F} : StieltjesIntegrable a b B f g ↔ StieltjesIntegrable b a B f g

theorem RiemannStieltjes.StieltjesIntegrable.symm {E : Type u_1} {F : Type u_2} {G : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {a b : ℝ} {B : E →L[ℝ] F →L[ℝ] G} {f : ℝ → E} {g : ℝ → F} (h : StieltjesIntegrable a b B f g) : StieltjesIntegrable b a B f g

theorem RiemannStieltjes.stieltjesIntegrable_iff_integrable_of_gt {E : Type u_1} {F : Type u_2} {G : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {a b : ℝ} {B : E →L[ℝ] F →L[ℝ] G} {f : ℝ → E} {g : ℝ → F} (hab : b < a) : StieltjesIntegrable a b B f g ↔ BoxIntegral.Integrable (BoxIntegral.interval hab) BoxIntegral.IntegrationParams.Riemann (fun (x : Fin 1 → ℝ) => f (x 0)) (BoxIntegral.BoxAdditiveMap.increment fun (x : ℝ) => B.flip (g x))

theorem RiemannStieltjes.StieltjesIntegrable.iff_min_max {E : Type u_1} {F : Type u_2} {G : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {a b : ℝ} {B : E →L[ℝ] F →L[ℝ] G} {f : ℝ → E} {g : ℝ → F} : StieltjesIntegrable a b B f g ↔ StieltjesIntegrable (min a b) (max a b) B f g

theorem RiemannStieltjes.HasStieltjesIntegral.unique {E : Type u_1} {F : Type u_2} {G : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {a b : ℝ} {B : E →L[ℝ] F →L[ℝ] G} {f : ℝ → E} {g : ℝ → F} {L₁ L₂ : G} (h₁ : HasStieltjesIntegral a b B f g L₁) (h₂ : HasStieltjesIntegral a b B f g L₂) : L₁ = L₂

Uniqueness: the Riemann–Stieltjes integral, when it exists, is unique.

theorem RiemannStieltjes.HasStieltjesIntegral.stieltjesIntegrable {E : Type u_1} {F : Type u_2} {G : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {a b : ℝ} {B : E →L[ℝ] F →L[ℝ] G} {f : ℝ → E} {g : ℝ → F} {L : G} (h : HasStieltjesIntegral a b B f g L) : StieltjesIntegrable a b B f g

The existence of a Riemann–Stieltjes integral implies StieltjesIntegrable.

theorem RiemannStieltjes.StieltjesIntegrable.hasStieltjesIntegral {E : Type u_1} {F : Type u_2} {G : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {a b : ℝ} {B : E →L[ℝ] F →L[ℝ] G} {f : ℝ → E} {g : ℝ → F} (h : StieltjesIntegrable a b B f g) : HasStieltjesIntegral a b B f g (stieltjesIntegral a b B (fun (x : ℝ) => f x) g)

theorem RiemannStieltjes.HasStieltjesIntegral.stieltjesIntegral_eq {E : Type u_1} {F : Type u_2} {G : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {a b : ℝ} {B : E →L[ℝ] F →L[ℝ] G} {f : ℝ → E} {g : ℝ → F} {L : G} (h : HasStieltjesIntegral a b B f g L) : stieltjesIntegral a b B (fun (x : ℝ) => f x) g = L

If HasStieltjesIntegral a b B f g L, then ∫ˢ x in a..b, f x ∂[B; g] = L.

theorem RiemannStieltjes.StieltjesIntegrable.hasStieltjesIntegral_iff {E : Type u_1} {F : Type u_2} {G : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {a b : ℝ} {B : E →L[ℝ] F →L[ℝ] G} {f : ℝ → E} {g : ℝ → F} (h : StieltjesIntegrable a b B f g) (L : G) : HasStieltjesIntegral a b B f g L ↔ stieltjesIntegral a b B (fun (x : ℝ) => f x) g = L

@[simp]

theorem RiemannStieltjes.stieltjesIntegral.integral_same {E : Type u_1} {F : Type u_2} {G : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {a : ℝ} {B : E →L[ℝ] F →L[ℝ] G} {f : ℝ → E} {g : ℝ → F} : stieltjesIntegral a a B (fun (x : ℝ) => f x) g = 0

@[simp]

theorem RiemannStieltjes.stieltjesIntegral.integral_undef {E : Type u_1} {F : Type u_2} {G : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {a b : ℝ} {B : E →L[ℝ] F →L[ℝ] G} {f : ℝ → E} {g : ℝ → F} (h : ¬StieltjesIntegrable a b B f g) : stieltjesIntegral a b B (fun (x : ℝ) => f x) g = 0

theorem RiemannStieltjes.stieltjesIntegral.integral_symm {E : Type u_1} {F : Type u_2} {G : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {a b : ℝ} {B : E →L[ℝ] F →L[ℝ] G} {f : ℝ → E} {g : ℝ → F} : stieltjesIntegral b a B (fun (x : ℝ) => f x) g = -stieltjesIntegral a b B (fun (x : ℝ) => f x) g

theorem RiemannStieltjes.hasStieltjesIntegral'_congr {E : Type u_1} {F : Type u_2} {G : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {a b : ℝ} {B B' : E →L[ℝ] F →L[ℝ] G} {f₁ f₂ : ℝ → E} {g₁ g₂ : ℝ → F} {L : G} (hab : a < b) (hBB' : B = B') (hf : Set.EqOn f₁ f₂ (Set.Icc a b)) (hg : Set.EqOn g₁ g₂ (Set.Icc a b)) : HasStieltjesIntegralOrdered a b B f₁ g₁ L hab ↔ HasStieltjesIntegralOrdered a b B' f₂ g₂ L hab

theorem RiemannStieltjes.hasStieltjesIntegral_congr {E : Type u_1} {F : Type u_2} {G : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {a b : ℝ} {B B' : E →L[ℝ] F →L[ℝ] G} {f₁ f₂ : ℝ → E} {g₁ g₂ : ℝ → F} {L : G} (hBB' : B = B') (hf : Set.EqOn f₁ f₂ (Set.uIcc a b)) (hg : Set.EqOn g₁ g₂ (Set.uIcc a b)) : HasStieltjesIntegral a b B f₁ g₁ L ↔ HasStieltjesIntegral a b B' f₂ g₂ L

theorem RiemannStieltjes.stieltjesIntegrable_congr {E : Type u_1} {F : Type u_2} {G : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {a b : ℝ} {B B' : E →L[ℝ] F →L[ℝ] G} {f₁ f₂ : ℝ → E} {g₁ g₂ : ℝ → F} (hBB' : B = B') (hf : Set.EqOn f₁ f₂ (Set.uIcc a b)) (hg : Set.EqOn g₁ g₂ (Set.uIcc a b)) : StieltjesIntegrable a b B f₁ g₁ ↔ StieltjesIntegrable a b B' f₂ g₂

theorem RiemannStieltjes.stieltjesIntegral_congr {E : Type u_1} {F : Type u_2} {G : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {a b : ℝ} {B B' : E →L[ℝ] F →L[ℝ] G} {f₁ f₂ : ℝ → E} {g₁ g₂ : ℝ → F} (hBB' : B = B') (hf : Set.EqOn f₁ f₂ (Set.uIcc a b)) (hg : Set.EqOn g₁ g₂ (Set.uIcc a b)) : stieltjesIntegral a b B (fun (x : ℝ) => f₁ x) g₁ = stieltjesIntegral a b B' (fun (x : ℝ) => f₂ x) g₂

The Riemann integral

theorem RiemannStieltjes.HasRiemannIntegral.iff_hasIntegral {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : ℝ} {f : ℝ → E} {L : E} (hab : a < b) : HasRiemannIntegral a b f L ↔ BoxIntegral.HasIntegral (BoxIntegral.interval hab) BoxIntegral.IntegrationParams.Riemann (fun (x : Fin 1 → ℝ) => f (x 0)) BoxIntegral.BoxAdditiveMap.volume L

theorem RiemannStieltjes.RiemannIntegrable_def {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : ℝ} {f : ℝ → E} : RiemannIntegrable a b f ↔ ∃ (L : E), HasRiemannIntegral a b f L

theorem RiemannStieltjes.HasRiemannIntegral.symm_iff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : ℝ} {f : ℝ → E} {L : E} : HasRiemannIntegral a b f L ↔ HasRiemannIntegral b a f (-L)

theorem RiemannStieltjes.HasRiemannIntegral.symm {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : ℝ} {f : ℝ → E} {L : E} (h : HasRiemannIntegral a b f L) : HasRiemannIntegral b a f (-L)

theorem RiemannStieltjes.RiemannIntegrable.symm {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : ℝ} {f : ℝ → E} (h : RiemannIntegrable a b f) : RiemannIntegrable b a f

@[simp]

theorem RiemannStieltjes.HasRiemannIntegral.of_eq_iff_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {a : ℝ} {f : ℝ → E} {L : E} : HasRiemannIntegral a a f L ↔ L = 0

@[simp]

theorem RiemannStieltjes.RiemannIntegrable.of_eq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {a : ℝ} {f : ℝ → E} : RiemannIntegrable a a f

@[simp]

theorem RiemannStieltjes.riemannIntegral.integral_same {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {a : ℝ} {f : ℝ → E} : (riemannIntegral a a fun (x : ℝ) => f x) = 0

theorem RiemannStieltjes.RiemannIntegrable.iff_integrable {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : ℝ} {f : ℝ → E} (hab : a < b) : RiemannIntegrable a b f ↔ BoxIntegral.Integrable (BoxIntegral.interval hab) BoxIntegral.IntegrationParams.Riemann (fun (x : Fin 1 → ℝ) => f (x 0)) BoxIntegral.BoxAdditiveMap.volume

theorem RiemannStieltjes.HasRiemannIntegral.unique {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : ℝ} {f : ℝ → E} {L₁ L₂ : E} (h₁ : HasRiemannIntegral a b f L₁) (h₂ : HasRiemannIntegral a b f L₂) : L₁ = L₂

theorem RiemannStieltjes.HasRiemannIntegral.riemannIntegrable {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : ℝ} {f : ℝ → E} {L : E} (h : HasRiemannIntegral a b f L) : RiemannIntegrable a b f

theorem RiemannStieltjes.RiemannIntegrable.hasRiemannIntegral {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : ℝ} {f : ℝ → E} (h : RiemannIntegrable a b f) : HasRiemannIntegral a b f (riemannIntegral a b fun (x : ℝ) => f x)

theorem RiemannStieltjes.HasRiemannIntegral.riemannIntegral_eq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : ℝ} {f : ℝ → E} {L : E} (h : HasRiemannIntegral a b f L) : (riemannIntegral a b fun (x : ℝ) => f x) = L

theorem RiemannStieltjes.RiemannIntegrable.hasRiemannIntegral_iff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : ℝ} {f : ℝ → E} (h : RiemannIntegrable a b f) (L : E) : HasRiemannIntegral a b f L ↔ (riemannIntegral a b fun (x : ℝ) => f x) = L

theorem RiemannStieltjes.hasRiemannIntegral_congr {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : ℝ} {f₁ f₂ : ℝ → E} {L : E} (hf : Set.EqOn f₁ f₂ (Set.uIcc a b)) : HasRiemannIntegral a b f₁ L ↔ HasRiemannIntegral a b f₂ L

theorem RiemannStieltjes.riemannIntegrable_congr {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : ℝ} {f₁ f₂ : ℝ → E} (hf : Set.EqOn f₁ f₂ (Set.uIcc a b)) : RiemannIntegrable a b f₁ ↔ RiemannIntegrable a b f₂

@[simp]

theorem RiemannStieltjes.riemannIntegral.integral_undef {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : ℝ} {f : ℝ → E} (h : ¬RiemannIntegrable a b f) : (riemannIntegral a b fun (x : ℝ) => f x) = 0

theorem RiemannStieltjes.riemannIntegral.integral_symm {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : ℝ} {f : ℝ → E} : (riemannIntegral b a fun (x : ℝ) => f x) = -riemannIntegral a b fun (x : ℝ) => f x