Riemann integrability

Stream: Is there code for X?

[Harald Helfgott]

I’m working on a barebones Riemann-Stieltjes integration theory (Montgomery–Vaughan Appendix A), and I want it to interface cleanly with Mathlib’s existing integration framework.

The natural way to do so is through Riemann integrability; for instance, one can show (as in Theorem A.3 of Montgomery-Vaughan) that, if $f$ is Riemann integrable and $g$ is $C^1$, then the Riemann-Stieltjes integral $\int_a^b f(x) dg(x)$ equals $\int_a^b f(x) g'(x) dx$, where this last integral is to be understood as a Riemann integral (which is the same as a Riemann-Stieltjes integral when it comes to $dx$).

Then one can use existing results on when a function is Riemann integrable to show when Riemann-Stieltjes integration theory is applicable.

In Mathlib, Riemann integration appears to be accessible as a special case of BoxIntegral, via IntegrationParams with bRiemann = true. In particular, results such as
BoxIntegral.integrable_of_bounded_and_ae_continuousWithinAt
seem to encode the classical fact that a bounded function which is continuous a.e. on an interval is Riemann integrable, and then of course the Riemann integral equals the Lebesgue integral.

What I am missing is a clear bridge between this BoxIntegral notion of Riemann integrability and a completely elementary, mesh-based definition of Riemann integrability. Concretely, suppose one defines tagged partitions, mesh, and Riemann sums in the usual way - say, keeping things simple:

structure RPartition (a b : ℝ) where
  n : ℕ
  x : Fin (n + 1) → ℝ
  monotone : Monotone x
  left : x 0 = a
  right : x (Fin.last n) = b

def RPartition.mesh {a b : ℝ} (P : RPartition a b) : ℝ :=
  ((Finset.univ : Finset (Fin P.n)).image (fun i => P.x i.succ - P.x i.castSucc)).max.getD 0

/-- A tagged Riemann partition includes points `xi` in each subinterval `[x_i, x_{i+1}]`. -/
structure TaggedRPartition (a b : ℝ) extends RPartition a b where
  xi : Fin n → ℝ
  h_xi : ∀ i : Fin n, x i.castSucc ≤ xi i ∧ xi i ≤ x i.succ

def RiemannSumR {a b : ℝ} (f : ℝ → ℝ) (P : TaggedRPartition a b) : ℝ :=
  ∑ i : Fin P.n, f (P.xi i) * (P.x i.succ - P.x i.castSucc)

def HasRIntegral (f : ℝ → ℝ) (a b I : ℝ) : Prop :=
  ∀ ε > 0, ∃ δ > 0, ∀ P : TaggedRPartition a b,
    P.mesh ≤ δ → |RiemannSumR f P - I| < ε

Question: is there already a lemma proving that HasRIntegral f a b I (or something very close to it; people must have worked with simple implementations such as this) is equivalent to BoxIntegral’s Riemann integrability? If not, can anybody more experienced with BoxIntegral show us how to do it?

I would like, at the very least, have a lemma showing that HasRIntegral f a b I holds if f is bounded and continuous a.e. on [a,b], and also a lemma showing that the Riemann integral I then equals the Lebesgue integral. Again, the proof should simply use the theory developed in BoxIntegral, rather than do anything from scratch.

[Notification Bot]

A message was moved here from #Is there code for X? > Riemann integral by Harald Helfgott.

[Yury G. Kudryashov]

You need to build an equivalence between your partitions and partitions used for box integrals.

[Harald Helfgott]

Right - how do we do that?

[Yury G. Kudryashov]

I see that we've already started this discussion in #PrimeNumberTheorem+ > Formalizing Riemann-Stieltjes theory . For one side of the equivalence, you can define boxes as [![x i.castSucc], ![x i.succ]). For the other side, you need to take all the endpoints and sort them. Then you need to show that these maps are inverse of each other.

[Yury G. Kudryashov]

Note that box integrals in Mathlib use nonempty boxes (I don't remember the exact reasons; AFAIR, I wanted coercion to set to be injective), while your construction allows empty intervals.

[Yury G. Kudryashov]

This will complicate things a bit.