theorem bounded_of_eq_off_finite {a b : ℝ} {f g : ℝ → ℝ} {S : Set ℝ} (hbound : ∃ (M : ℝ), ∀ x ∈ Set.Icc a b, |f x| ≤ M) (hfin : S.Finite) (hfg : ∀ x ∈ Set.Icc a b \ S, g x = f x) : ∃ (M : ℝ), ∀ x ∈ Set.Icc a b, |g x| ≤ M

theorem riemannIntegral_eq_zero_of_eq_zero_on_Icc {a b : ℝ} {h : ℝ → ℝ} (hab : a ≤ b) (hzero : ∀ x ∈ Set.Icc a b, h x = 0) : ∃ (hh : RiemannIntegrableOn h a b), riemannIntegral h a b hh = 0

theorem intervalPartition_subinterval_subset {a b : ℝ} (P : IntervalPartition a b) (i : Fin P.n) : Set.Icc (P.points i.castSucc) (P.points i.succ) ⊆ Set.Icc a b

Each subinterval of a partition lies in the ambient interval.

theorem upperTag_le_of_bound {a b : ℝ} {h : ℝ → ℝ} {M : ℝ} (P : IntervalPartition a b) (i : Fin P.n) (hmax : ∀ x ∈ Set.Icc a b, h x ≤ M) : upperTag h P i ≤ M

Upper tag bound on a bounded interval.

theorem lowerTag_ge_of_bound {a b : ℝ} {h : ℝ → ℝ} {M : ℝ} (P : IntervalPartition a b) (i : Fin P.n) (hmin : ∀ x ∈ Set.Icc a b, -M ≤ h x) : -M ≤ lowerTag h P i

Lower tag bound on a bounded interval.

theorem tag_gap_le_two_M {a b : ℝ} {h : ℝ → ℝ} {M : ℝ} {P : IntervalPartition a b} (hmin : ∀ x ∈ Set.Icc a b, -M ≤ h x) (hmax : ∀ x ∈ Set.Icc a b, h x ≤ M) (i : Fin P.n) : upperTag h P i - lowerTag h P i ≤ 2 * M

Tag gap bound when h is bounded by ±M on [a, b].

theorem sum_fin_two_eq {n : ℕ} (h : n = 2) (f : Fin n → ℝ) : ∑ i : Fin n, f i = f ⟨0, ⋯⟩ + f ⟨1, ⋯⟩

Sum over Fin n when n = 2.

theorem upper_lower_gap_two_steps_right_zero {a b : ℝ} {h : ℝ → ℝ} {M δ : ℝ} (P : IntervalPartition a b) (hP : P.n = 2) (hzero : upperTag h P ⟨1, ⋯⟩ = 0 ∧ lowerTag h P ⟨1, ⋯⟩ = 0) (htag0 : upperTag h P ⟨0, ⋯⟩ - lowerTag h P ⟨0, ⋯⟩ ≤ 2 * M) (hdelta0 : P.delta ⟨0, ⋯⟩ = δ) : upperDarbouxSum h P - lowerDarbouxSum h P ≤ 2 * M * δ

Two-step gap bound when the right subinterval contributes zero.

theorem upper_lower_gap_two_steps_left_zero {a b : ℝ} {h : ℝ → ℝ} {M δ : ℝ} (P : IntervalPartition a b) (hP : P.n = 2) (hzero : upperTag h P ⟨0, ⋯⟩ = 0 ∧ lowerTag h P ⟨0, ⋯⟩ = 0) (htag1 : upperTag h P ⟨1, ⋯⟩ - lowerTag h P ⟨1, ⋯⟩ ≤ 2 * M) (hdelta1 : P.delta ⟨1, ⋯⟩ = δ) : upperDarbouxSum h P - lowerDarbouxSum h P ≤ 2 * M * δ

Two-step gap bound when the left subinterval contributes zero.

theorem gap_lt_of_le_twoM_delta {α M δ ε : ℝ} (hMpos : 0 < M) (hδ_le : δ ≤ ε / (4 * M)) (hgap : α ≤ 2 * M * δ) (hε : 0 < ε) : α < ε

Convert a 2 * M * δ gap bound into an ε-bound.

theorem gap_lt_of_le_fourM_delta {α M δ ε : ℝ} (hMpos : 0 < M) (hδ_le : δ ≤ ε / (8 * M)) (hgap : α ≤ 4 * M * δ) (hε : 0 < ε) : α < ε

Convert a 4 * M * δ gap bound into an ε-bound.