def Integration.C_ab (a b : ℝ) : Set (ℝ → ℝ)

The set C([a,b]) of continuous real-valued functions on the closed interval [a,b].

structure Integration.Partition (a b : ℝ) : Type

A partition of the closed interval [a,b]: a strictly increasing finite sequence a = x_0 < x_1 < ⋯ < x_n = b of points. The field n is the number of subintervals, and points enumerates the n + 1 endpoints.

• n : ℕ
• points : Fin (self.n + 1) → ℝ
• ordered : StrictMono self.points
• first : self.points 0 = a
• last : self.points (Fin.last self.n) = b

structure Integration.TaggedPartition (a b : ℝ) extends Integration.Partition a b : Type

A tagged partition of [a,b]: a partition together with a choice of a tag ξ_k ∈ [x_{k-1}, x_k] in each subinterval.

• n : ℕ
• points : Fin (self.n + 1) → ℝ
• ordered : StrictMono self.points
• first : self.points 0 = a
• last : self.points (Fin.last self.n) = b
• tags : Fin self.n → ℝ
• tag_mem (i : Fin self.n) : self.points i.castSucc ≤ self.tags i ∧ self.tags i ≤ self.points i.succ

noncomputable def Integration.Partition.mesh {a b : ℝ} (P : Partition a b) : ℝ

The mesh (or norm) ‖x‖ of a partition: the maximum length max_k (x_k - x_{k-1}) of its subintervals. Defined to be 0 for the trivial partition with n = 0.

def Integration.Partition.pointSet {a b : ℝ} (P : Partition a b) : Set ℝ

The underlying set {x_0, x_1, …, x_n} of points of a partition.

def Integration.Partition.IsRefinement {a b : ℝ} (Q P : Partition a b) : Prop

Q is a refinement of P if every point of P appears in Q, i.e. the underlying point set of P is contained in that of Q.

noncomputable def Integration.riemannSum {a b : ℝ} (f : ℝ → ℝ) (T : TaggedPartition a b) : ℝ

The Riemann sum S_f(x, ξ) = ∑_k f(ξ_k) (x_k - x_{k-1}) of a function f with respect to a tagged partition T.

theorem Integration.Partition.n_pos_of_lt {a b : ℝ} (hab : a < b) (P : Partition a b) : 0 < P.n

If a < b, then any partition of [a,b] has at least one subinterval, i.e. 0 < P.n.

theorem Integration.Partition.mesh_pos_of_lt {a b : ℝ} (hab : a < b) (P : Partition a b) : 0 < P.mesh

If a < b, then the mesh of any partition of [a,b] is strictly positive.

theorem Integration.riemannSum_eq_zero_of_n_eq_zero {a b : ℝ} (f : ℝ → ℝ) (T : TaggedPartition a b) (h : T.n = 0) : riemannSum f T = 0

The Riemann sum over a trivial tagged partition (with n = 0 subintervals) is 0, since it is an empty sum.