Upper and Lower Darboux Sums of a Bounded Function on a Partition

In the setting of The Real Line: Standing Notation and Background for Calculus on Intervals, let $a,b\in\mathbb{R}$ with $a<b$, and let $f:[a,b]\to\mathbb{R}$ be bounded: there is $B\in\mathbb{R}$ with $|f(t)|\le B$ for every $t\in[a,b]$. Let $P$ be a partition of $[a,b]$, and let $n\in\mathbb{N}$ and the increasing listing $a=x_{1}<x_{2}<\dots<x_{n+1}=b$ of $P$ be as in The Increasing Listing of a Partition: Endpoints, Lengths, Covering, Unions, Inserting a Point, Concatenation and Uniform Partitions (i), which states that they are unique; $[n]=\{1,\dots,n\}$ is as in Intervals of Natural Numbers (ii). For $i\in[n]$, $x_{i}$ and $x_{i+1}$ are defined by The Increasing Listing of a Partition: Endpoints, Lengths, Covering, Unions, Inserting a Point, Concatenation and Uniform Partitions (ii), they lie in $P\subseteq[a,b]$, and $x_{i}<x_{i+1}$ by The Increasing Listing of a Partition: Endpoints, Lengths, Covering, Unions, Inserting a Point, Concatenation and Uniform Partitions (iii); so $[x_{i},x_{i+1}]\subseteq[a,b]$ by Basic Facts about Intervals of the Real Line (v) and Basic Facts about Intervals of the Real Line (ii). The sums $\sum_{i=1}^{n}$ below are finite sums of maps from $[n]$ to $\mathbb{R}$ as in Iterated Operations: Finite Sums and Finite Products (i) and Iterated Operations: Finite Sums and Finite Products (iii), equal to the sums over the finite set $[n]$ by Natural Numbers as Indices: ℕ ⊆ ℕ₀, 1 ∈ ℕ₀, and the Two Readings of an Operation from 1 to n (v).

(i) For $i\in[n]$, let

$$S_{i}=\{f(t):t\in[x_{i},x_{i+1}]\}$$

be the image $f([x_{i},x_{i+1}])$ of $[x_{i},x_{i+1}]$ under $f$, a set by Sets and Maps: Ordinary Notation (vii); by The Image and the Preimage of a Class under a Class (i), its elements are the values $f(t)$ with $t\in[x_{i},x_{i+1}]$, so it is a subset of $\mathbb{R}$, it is nonempty, as $f(x_{i})\in S_{i}$, and $-B\le s\le B$ for every $s\in S_{i}$. Hence it has a supremum and an infimum by The Real Line: Standing Notation and Background for Calculus on Intervals (iii), each unique by Bounds, Least and Greatest Elements, Suprema and Infima for a Partial Order (iv). The upper bound map $M:[n]\to\mathbb{R}$ and the lower bound map $m:[n]\to\mathbb{R}$ of $f$ on $P$ are the maps with

$$M(i)=\sup S_{i},\qquad m(i)=\inf S_{i}\qquad(i\in[n]),$$

which exist and are unique by Predicative Formulas for Suprema and Infima, and Maps Defined by Suprema and Infima (iii), applied with $p=\mathbb{R}$ and $a=[n]$, the set $S_{i}$ being given by a typed term in $i$ by Images of Typed Terms: the Set of Values $\{t:u\in D\}$ Is a Set, Finite when $D$ Is Finite, and a Typed Term (v). For every $i\in[n]$ and every set $s$: $s\in S_{i}$ if and only if $s=f(t)$ for some $t\in[x_{i},x_{i+1}]$; $M(i)$ is the supremum and $m(i)$ the infimum of $S_{i}$ in $\mathbb{R}$; and $M(i)\,(x_{i+1}-x_{i})$ and $m(i)\,(x_{i+1}-x_{i})$ lie in $\mathbb{R}$.

(ii) The upper sum of $f$ with respect to $P$ is the real number

$$U(f,P)=\sum_{i=1}^{n}M(i)\,(x_{i+1}-x_{i}),$$

the finite sum of the map $i\mapsto M(i)\,(x_{i+1}-x_{i})$ from $[n]$ to $\mathbb{R}$, the pointwise product of $M$ and the map $i\mapsto x_{i+1}-x_{i}$ of The Increasing Listing of a Partition: Endpoints, Lengths, Covering, Unions, Inserting a Point, Concatenation and Uniform Partitions (iii); it lies in $\mathbb{R}$ by Iterated Operations and Operations over Finite Sets Take Values in the Underlying Set.

(iii) The lower sum of $f$ with respect to $P$ is the real number

$$L(f,P)=\sum_{i=1}^{n}m(i)\,(x_{i+1}-x_{i}),$$

the finite sum of the map $i\mapsto m(i)\,(x_{i+1}-x_{i})$ from $[n]$ to $\mathbb{R}$, the pointwise product of $m$ and the map $i\mapsto x_{i+1}-x_{i}$ of The Increasing Listing of a Partition: Endpoints, Lengths, Covering, Unions, Inserting a Point, Concatenation and Uniform Partitions (iii); it lies in $\mathbb{R}$ by Iterated Operations and Operations over Finite Sets Take Values in the Underlying Set.