theorem intervalPartition_three_points {a b c : ℝ} (hab : a < b) (hbc : b < c) : ∃ (P : IntervalPartition a c), b ∈ Set.range P.points

A three-point partition of [a, c] with an interior point b.

theorem intervalPartition_refine_with_point {a b c : ℝ} (hab : a < b) (hbc : b < c) (P : IntervalPartition a c) : ∃ (Q : IntervalPartition a c), P.IsRefinement Q ∧ b ∈ Set.range Q.points

Any partition of [a, c] admits a refinement that includes b.

theorem intervalPartition_small_delta {a b δ : ℝ} (hab : a < b) (hδ : 0 < δ) : ∃ (P : IntervalPartition a b), ∀ (i : Fin P.n), P.delta i < δ

A uniform partition of [a, b] with mesh smaller than δ.

theorem darbouxIntegral_restrict_to_partitions_with_point {a b c : ℝ} {f : ℝ → ℝ} (hab : a < b) (hbc : b < c) (hbound : ∃ (M : ℝ), ∀ x ∈ Set.Icc a c, |f x| ≤ M) : lowerDarbouxIntegral f a c = sSup (Set.range fun (P : { P : IntervalPartition a c // b ∈ Set.range P.points }) => lowerDarbouxSum f ↑P) ∧ upperDarbouxIntegral f a c = sInf (Set.range fun (P : { P : IntervalPartition a c // b ∈ Set.range P.points }) => upperDarbouxSum f ↑P)

Restrict lower/upper Darboux integrals to partitions containing a point.

theorem intervalPartition_split_at_point {a b c : ℝ} {f : ℝ → ℝ} (P : IntervalPartition a c) (hb : b ∈ Set.range P.points) : ∃ (P1 : IntervalPartition a b) (P2 : IntervalPartition b c), lowerDarbouxSum f P = lowerDarbouxSum f P1 + lowerDarbouxSum f P2 ∧ upperDarbouxSum f P = upperDarbouxSum f P1 + upperDarbouxSum f P2

Split a partition that contains b into left/right partitions.

theorem intervalPartition_append {a b c : ℝ} {f : ℝ → ℝ} (P1 : IntervalPartition a b) (P2 : IntervalPartition b c) : ∃ (P : IntervalPartition a c), b ∈ Set.range P.points ∧ lowerDarbouxSum f P = lowerDarbouxSum f P1 + lowerDarbouxSum f P2 ∧ upperDarbouxSum f P = upperDarbouxSum f P1 + upperDarbouxSum f P2

Append a left/right partition into a partition of [a, c].