theorem upper_lower_gap_degenerate_interval {a : ℝ} {h : ℝ → ℝ} (ε : ℝ) : ε > 0 → ∃ (P : IntervalPartition a a), upperDarbouxSum h P - lowerDarbouxSum h P < ε

On a degenerate interval, the upper/lower Darboux gap is zero.

theorem upper_lower_gap_left_endpoint {a b c : ℝ} {h : ℝ → ℝ} {M : ℝ} (hc : c ∈ Set.Icc a b) (hz : ∀ x ∈ Set.Icc a b \ {c}, h x = 0) (hM : ∀ x ∈ Set.Icc a b, |h x| ≤ M) (hhc : h c ≠ 0) (hca : c = a) (hlt : a < b) (ε : ℝ) : ε > 0 → ∃ (P : IntervalPartition a b), upperDarbouxSum h P - lowerDarbouxSum h P < ε

Gap estimate when the exceptional point is the left endpoint.

theorem upper_lower_gap_right_endpoint {a b c : ℝ} {h : ℝ → ℝ} {M : ℝ} (hc : c ∈ Set.Icc a b) (hz : ∀ x ∈ Set.Icc a b \ {c}, h x = 0) (hM : ∀ x ∈ Set.Icc a b, |h x| ≤ M) (hhc : h c ≠ 0) (hcb : c = b) (hlt : a < b) (ε : ℝ) : ε > 0 → ∃ (P : IntervalPartition a b), upperDarbouxSum h P - lowerDarbouxSum h P < ε

Gap estimate when the exceptional point is the right endpoint.

theorem upper_lower_gap_tag_zero_of_eq_zero {a b : ℝ} {h : ℝ → ℝ} (P : IntervalPartition a b) (i : Fin P.n) (hzero : ∀ x ∈ Set.Icc (P.points i.castSucc) (P.points i.succ), h x = 0) : upperTag h P i = 0 ∧ lowerTag h P i = 0

If h vanishes on a subinterval, its upper/lower tags are zero.

theorem upper_lower_gap_middle_delta {a b c M ε : ℝ} (hMpos : 0 < M) (hca' : a < c) (hcb' : c < b) (hε : 0 < ε) : ∃ δ > 0, δ ≤ ε / (8 * M) ∧ a < c - δ ∧ c - δ < c ∧ c < c + δ ∧ c + δ < b

Choose a small δ for the middle-case split.

theorem upper_lower_gap_middle_zero_left {a b c δ : ℝ} {h : ℝ → ℝ} (hz : ∀ x ∈ Set.Icc a b \ {c}, h x = 0) (hright_lt : c - δ < c) (hcb' : c < b) (x : ℝ) : x ∈ Set.Icc a (c - δ) → h x = 0

h vanishes on the left subinterval in the middle-case split.

theorem upper_lower_gap_middle_zero_right {a b c δ : ℝ} {h : ℝ → ℝ} (hz : ∀ x ∈ Set.Icc a b \ {c}, h x = 0) (hca' : a < c) (hmid_lt : c < c + δ) (x : ℝ) : x ∈ Set.Icc (c + δ) b → h x = 0

h vanishes on the right subinterval in the middle-case split.

theorem upper_lower_gap_append_gap {a b c : ℝ} {h : ℝ → ℝ} {M δ : ℝ} (P1 : IntervalPartition a c) (P2 : IntervalPartition c b) (hgap1 : upperDarbouxSum h P1 - lowerDarbouxSum h P1 ≤ 2 * M * δ) (hgap2 : upperDarbouxSum h P2 - lowerDarbouxSum h P2 ≤ 2 * M * δ) : ∃ (P : IntervalPartition a b), upperDarbouxSum h P - lowerDarbouxSum h P ≤ 4 * M * δ

Append two partitions and combine 2 * M * δ gap bounds.

theorem upper_lower_gap_middle {a b c : ℝ} {h : ℝ → ℝ} {M : ℝ} (hz : ∀ x ∈ Set.Icc a b \ {c}, h x = 0) (hM : ∀ x ∈ Set.Icc a b, |h x| ≤ M) (hhc : h c ≠ 0) (hca' : a < c) (hcb' : c < b) (ε : ℝ) : ε > 0 → ∃ (P : IntervalPartition a b), upperDarbouxSum h P - lowerDarbouxSum h P < ε

Gap estimate when the exceptional point lies strictly inside (a, b).

theorem upper_lower_gap_of_eq_zero_off_singleton {a b : ℝ} {h : ℝ → ℝ} {c M : ℝ} (hc : c ∈ Set.Icc a b) (hz : ∀ x ∈ Set.Icc a b \ {c}, h x = 0) (hM : ∀ x ∈ Set.Icc a b, |h x| ≤ M) (hhc : h c ≠ 0) (ε : ℝ) : ε > 0 → ∃ (P : IntervalPartition a b), upperDarbouxSum h P - lowerDarbouxSum h P < ε

theorem lower_upper_sum_sign_of_eq_zero_off_singleton {a b : ℝ} {h : ℝ → ℝ} {c M : ℝ} (hM : ∀ x ∈ Set.Icc a b, |h x| ≤ M) (hz : ∀ x ∈ Set.Icc a b \ {c}, h x = 0) (P : IntervalPartition a b) : lowerDarbouxSum h P ≤ 0 ∧ 0 ≤ upperDarbouxSum h P

theorem riemannIntegral_eq_zero_of_eq_zero_off_singleton {a b : ℝ} {h : ℝ → ℝ} {c : ℝ} (hc : c ∈ Set.Icc a b) (hz : ∀ x ∈ Set.Icc a b \ {c}, h x = 0) : ∃ (hh : RiemannIntegrableOn h a b), riemannIntegral h a b hh = 0

Changing a single point on [a, b] does not affect the Riemann integral.

theorem riemannIntegral_eq_of_eq_off_singleton {a b : ℝ} {f g : ℝ → ℝ} {c : ℝ} (hc : c ∈ Set.Icc a b) (hf : RiemannIntegrableOn f a b) (hfg : ∀ x ∈ Set.Icc a b \ {c}, g x = f x) : ∃ (hg : RiemannIntegrableOn g a b), riemannIntegral g a b hg = riemannIntegral f a b hf

Changing a single point on [a, b] does not affect the Riemann integral.

theorem riemannIntegral_eq_of_eq_off_finite {a b : ℝ} {f g : ℝ → ℝ} {S : Set ℝ} (hf : RiemannIntegrableOn f a b) (hfin : S.Finite) (hfg : ∀ x ∈ Set.Icc a b \ S, g x = f x) : ∃ (hg : RiemannIntegrableOn g a b), riemannIntegral g a b hg = riemannIntegral f a b hf

Proposition 5.2.10: If f : [a, b] → ℝ is Riemann integrable and g agrees with f on [a, b] except on a finite set S, then g is Riemann integrable and the integrals of f and g over [a, b] coincide.

theorem monotoneOn_riemannIntegrableOn {a b : ℝ} {f : ℝ → ℝ} (hmono : MonotoneOn f (Set.Icc a b)) : RiemannIntegrableOn f a b

Proposition 5.2.11: A monotone function f : [a, b] → ℝ belongs to ℛ([a, b]), i.e., it is Riemann integrable on the closed interval [a, b].