structure IntervalPartition (a b : ℝ) : Type

Definition 5.1.1: A partition P of [a, b] is a finite increasing list x₀, x₁, …, xₙ with x₀ = a and xₙ = b. Write Δxᵢ = xᵢ - xᵢ₋₁. For a bounded function f : [a, b] → ℝ, set mᵢ = inf {f x | x_{i-1} ≤ x ≤ xᵢ} and Mᵢ = sup {f x | x_{i-1} ≤ x ≤ xᵢ}, and define the lower Darboux sum L(P, f) = ∑ mᵢ Δxᵢ and the upper Darboux sum U(P, f) = ∑ Mᵢ Δxᵢ.

• n : ℕ
• points : Fin (self.n + 1) → ℝ
• mono : StrictMono self.points
• left_eq : self.points 0 = a
• right_eq : self.points ⟨self.n, ⋯⟩ = b

def IntervalPartition.delta {a b : ℝ} (P : IntervalPartition a b) (i : Fin P.n) : ℝ

The mesh length Δxᵢ = xᵢ - xᵢ₋₁ for the i-th subinterval.

noncomputable def lowerTag {a b : ℝ} (f : ℝ → ℝ) (P : IntervalPartition a b) (i : Fin P.n) : ℝ

The infimum of f on the i-th closed subinterval.

noncomputable def upperTag {a b : ℝ} (f : ℝ → ℝ) (P : IntervalPartition a b) (i : Fin P.n) : ℝ

The supremum of f on the i-th closed subinterval.

noncomputable def lowerDarbouxSum {a b : ℝ} (f : ℝ → ℝ) (P : IntervalPartition a b) : ℝ

Lower Darboux sum L(P, f) = ∑ mᵢ Δxᵢ.

noncomputable def upperDarbouxSum {a b : ℝ} (f : ℝ → ℝ) (P : IntervalPartition a b) : ℝ

Upper Darboux sum U(P, f) = ∑ Mᵢ Δxᵢ.

theorem lower_upper_sum_bounds {f : ℝ → ℝ} {a b m M : ℝ} (hmin : ∀ x ∈ Set.Icc a b, m ≤ f x) (hmax : ∀ x ∈ Set.Icc a b, f x ≤ M) (P : IntervalPartition a b) : m * (b - a) ≤ lowerDarbouxSum f P ∧ lowerDarbouxSum f P ≤ upperDarbouxSum f P ∧ upperDarbouxSum f P ≤ M * (b - a)

Proposition 5.1.2: If f : [a, b] → ℝ is bounded with m ≤ f x ≤ M on [a, b], then for every partition P of [a, b] we have m * (b - a) ≤ L(P, f) ≤ U(P, f) ≤ M * (b - a).

noncomputable def lowerDarbouxIntegral (f : ℝ → ℝ) (a b : ℝ) : ℝ

Definition 5.1.3: The lower Darboux integral ∫̲_a^b f is the supremum of all lower Darboux sums over partitions of [a, b]; the upper Darboux integral ∫̅_a^b f is the infimum of all upper Darboux sums over partitions of [a, b]. We also write these without an explicit integration variable.

noncomputable def upperDarbouxIntegral (f : ℝ → ℝ) (a b : ℝ) : ℝ

See lowerDarbouxIntegral for the description of the lower and upper Darboux integrals.

def realRationals : Set ℝ

The subset of real numbers consisting of rational points.

noncomputable def dirichletFunction (x : ℝ) : ℝ

Example 5.1.4: The Dirichlet function f : [0, 1] → ℝ with f x = 1 on the rationals and f x = 0 otherwise satisfies ∫̲₀¹ f = 0 and ∫̅₀¹ f = 1.

theorem dirichletFunction_bounds (x : ℝ) : 0 ≤ dirichletFunction x ∧ dirichletFunction x ≤ 1

The Dirichlet function only takes values in [0, 1].

theorem dirichlet_subinterval_has_rat_irr (P : IntervalPartition 0 1) (i : Fin P.n) : (∃ x ∈ Set.Icc (P.points i.castSucc) (P.points i.succ), x ∈ realRationals) ∧ ∃ x ∈ Set.Icc (P.points i.castSucc) (P.points i.succ), x ∉ realRationals

theorem dirichlet_tags_eq (P : IntervalPartition 0 1) (i : Fin P.n) : lowerTag dirichletFunction P i = 0 ∧ upperTag dirichletFunction P i = 1

theorem intervalPartition_sum_delta (P : IntervalPartition 0 1) : ∑ i : Fin P.n, P.delta i = 1

theorem dirichlet_darboux_sums (P : IntervalPartition 0 1) : lowerDarbouxSum dirichletFunction P = 0 ∧ upperDarbouxSum dirichletFunction P = 1

def unitIntervalPartition : IntervalPartition 0 1

theorem dirichletFunction_lower_integral : lowerDarbouxIntegral dirichletFunction 0 1 = 0

See dirichletFunction. The lower Darboux integral over [0, 1] is zero.

theorem dirichletFunction_upper_integral : upperDarbouxIntegral dirichletFunction 0 1 = 1

See dirichletFunction. The upper Darboux integral over [0, 1] is one.

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

Definition 5.1.6: A partition P̃ of [a, b] is a refinement of a partition P if, viewed as sets of partition points, P ⊆ P̃.

theorem lower_upper_sum_refinement {f : ℝ → ℝ} {a b : ℝ} (hbound : ∃ (M : ℝ), ∀ x ∈ Set.Icc a b, |f x| ≤ M) {P Q : IntervalPartition a b} (hPQ : P.IsRefinement Q) : lowerDarbouxSum f P ≤ lowerDarbouxSum f Q ∧ upperDarbouxSum f Q ≤ upperDarbouxSum f P

Proposition 5.1.7: For a bounded function f : [a, b] → ℝ, if P̃ is a refinement of a partition P of [a, b], then L(P, f) ≤ L(P̃, f) and U(P̃, f) ≤ U(P, f).

theorem intervalPartition_nonempty {a b : ℝ} (hab : a ≤ b) : Nonempty (IntervalPartition a b)

A partition exists whenever the interval is nonempty.

theorem intervalPartition_common_refinement {a b : ℝ} (P1 P2 : IntervalPartition a b) : ∃ (Q : IntervalPartition a b), P1.IsRefinement Q ∧ P2.IsRefinement Q

Two partitions admit a common refinement given by the union of their points.

theorem bounded_of_between {f : ℝ → ℝ} {a b m M : ℝ} (hmin : ∀ x ∈ Set.Icc a b, m ≤ f x) (hmax : ∀ x ∈ Set.Icc a b, f x ≤ M) : ∃ (B : ℝ), ∀ x ∈ Set.Icc a b, |f x| ≤ B

A boundedness witness from a two-sided bound on [a, b].

theorem lower_sum_le_upper_sum_any {f : ℝ → ℝ} {a b m M : ℝ} (hmin : ∀ x ∈ Set.Icc a b, m ≤ f x) (hmax : ∀ x ∈ Set.Icc a b, f x ≤ M) (P1 P2 : IntervalPartition a b) : lowerDarbouxSum f P1 ≤ upperDarbouxSum f P2

Any lower sum is bounded above by any upper sum.

theorem lower_upper_integral_bounds {f : ℝ → ℝ} {a b m M : ℝ} (hab : a ≤ b) (hmin : ∀ x ∈ Set.Icc a b, m ≤ f x) (hmax : ∀ x ∈ Set.Icc a b, f x ≤ M) : m * (b - a) ≤ lowerDarbouxIntegral f a b ∧ lowerDarbouxIntegral f a b ≤ upperDarbouxIntegral f a b ∧ upperDarbouxIntegral f a b ≤ M * (b - a)

Proposition 5.1.8: If a bounded function f : [a, b] → ℝ satisfies m ≤ f x ≤ M on [a, b], then the lower and upper Darboux integrals obey m * (b - a) ≤ ∫̲_a^b f ≤ ∫̅_a^b f ≤ M * (b - a).

def RiemannIntegrableOn (f : ℝ → ℝ) (a b : ℝ) : Prop

Definition 5.1.9: A bounded function f : [a, b] → ℝ is Riemann integrable if the lower and upper Darboux integrals coincide. The collection of such functions on [a, b] is denoted ℛ([a, b]), and when f is Riemann integrable its integral ∫_a^b f is the common value of the lower and upper integrals.

def riemannIntegrableFunctions (a b : ℝ) : Set (ℝ → ℝ)

The set ℛ([a, b]) of Riemann integrable functions on [a, b].

noncomputable def riemannIntegral (f : ℝ → ℝ) (a b : ℝ) (hf : RiemannIntegrableOn f a b) : ℝ

The Riemann integral of an integrable function is the common value of the lower and upper Darboux integrals.

theorem riemannIntegral_bounds {f : ℝ → ℝ} {a b m M : ℝ} (hab : a ≤ b) (hf : RiemannIntegrableOn f a b) (hmin : ∀ x ∈ Set.Icc a b, m ≤ f x) (hmax : ∀ x ∈ Set.Icc a b, f x ≤ M) : m * (b - a) ≤ riemannIntegral f a b hf ∧ riemannIntegral f a b hf ≤ M * (b - a)

Proposition 5.1.10: If f : [a, b] → ℝ is Riemann integrable and bounded between m and M on [a, b], then the integral is bounded by m * (b - a) and M * (b - a).

theorem constant_function_riemannIntegral (c a b : ℝ) (hab : a ≤ b) : ∃ (hf : RiemannIntegrableOn (fun (x : ℝ) => c) a b), riemannIntegral (fun (x : ℝ) => c) a b hf = c * (b - a)

Example 5.1.11: A constant function f x = c is Riemann integrable on [a, b], and its integral is c * (b - a).

noncomputable def stepFunctionExample (x : ℝ) : ℝ

Example 5.1.12: The step function on [0, 2] given by f x = 1 for x < 1, f 1 = 1 / 2, and f x = 0 for x > 1 is Riemann integrable with integral ∫_0^2 f = 1.

theorem stepFunctionExample_bounds (x : ℝ) : 0 ≤ stepFunctionExample x ∧ stepFunctionExample x ≤ 1

The step function only takes values in [0, 1].

noncomputable def stepPartition (ε : ℝ) (hε : 0 < ε ∧ ε < 1) : IntervalPartition 0 2

A partition adapted to the step function with points 0, 1-ε, 1+ε, 2.

theorem stepPartition_sums {ε : ℝ} (hε : 0 < ε ∧ ε < 1) : lowerDarbouxSum stepFunctionExample (stepPartition ε hε) = 1 - ε ∧ upperDarbouxSum stepFunctionExample (stepPartition ε hε) = 1 + ε

theorem stepFunctionExample_riemannIntegral : ∃ (hf : RiemannIntegrableOn stepFunctionExample 0 2), riemannIntegral stepFunctionExample 0 2 hf = 1

See stepFunctionExample. The function is Riemann integrable on [0, 2] and its integral equals 1.

theorem riemannIntegrable_of_upper_lower_gap {f : ℝ → ℝ} {a b : ℝ} (hbound : ∃ (M : ℝ), ∀ x ∈ Set.Icc a b, |f x| ≤ M) (hgap : ∀ ε > 0, ∃ (P : IntervalPartition a b), upperDarbouxSum f P - lowerDarbouxSum f P < ε) : RiemannIntegrableOn f a b

Proposition 5.1.13: A bounded function f : [a, b] → ℝ is Riemann integrable if for every ε > 0 there exists a partition P of [a, b] with U(P, f) - L(P, f) < ε.

theorem reciprocal_integrable_on_interval {b : ℝ} (hb : 0 < b) : RiemannIntegrableOn (fun (x : ℝ) => 1 / (1 + x)) 0 b

Example 5.1.14: For every b > 0 the function x ↦ 1 / (1 + x) is Riemann integrable on [0, b].