noncomputable def Integration.modulusOfContinuity (f : ℝ → ℝ) (a b η : ℝ) : ℝ

The modulus of continuity of a function f on [a, b] at scale η: w_f(η) = sup {|f(x) - f(y)| : x, y ∈ [a,b], |x - y| ≤ η}.

theorem Integration.modulusOfContinuity_tendsto_zero (f : ℝ → ℝ) (a b : ℝ) (hab : a ≤ b) (hf : ContinuousOn f (Set.Icc a b)) : Filter.Tendsto (modulusOfContinuity f a b) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

Theorem I (Modulus of continuity vanishes). For f ∈ C([a,b]), lim_{η → 0⁺} w_f(η) = 0. That is, ∀ ε > 0, ∃ δ > 0, ∀ η < δ : w_f(η) < ε.

theorem Integration.modulusOfContinuity_bddAbove (f : ℝ → ℝ) (a b η : ℝ) (hf : ContinuousOn f (Set.Icc a b)) : BddAbove {x : ℝ | ∃ x_1 ∈ Set.Icc a b, ∃ y ∈ Set.Icc a b, ∃ (_ : |x_1 - y| ≤ η), |f x_1 - f y| = x}

The set of values |f x - f y| for x, y ∈ [a,b] with |x - y| ≤ η is bounded above when f is continuous on [a,b].

theorem Integration.le_modulusOfContinuity (f : ℝ → ℝ) {a b : ℝ} (η : ℝ) (hf : ContinuousOn f (Set.Icc a b)) {x : ℝ} (hx : x ∈ Set.Icc a b) {y : ℝ} (hy : y ∈ Set.Icc a b) (hxy : |x - y| ≤ η) : |f x - f y| ≤ modulusOfContinuity f a b η

For x, y ∈ [a,b] with |x - y| ≤ η, the absolute difference |f x - f y| is bounded by the modulus of continuity w_f(η).

theorem Integration.Partition.succ_sub_castSucc_nonneg {a b : ℝ} (P : Partition a b) (i : Fin P.n) : 0 ≤ P.points i.succ - P.points i.castSucc

Each subinterval [x_i, x_{i+1}] of a partition has nonnegative length.

theorem Integration.Partition.le_mesh {a b : ℝ} (P : Partition a b) (i : Fin P.n) : P.points i.succ - P.points i.castSucc ≤ P.mesh

Each subinterval length x_{i+1} - x_i of a partition is bounded above by the partition's mesh (i.e., the maximum subinterval length).

theorem Integration.Partition.sum_sub_eq {a b : ℝ} (P : Partition a b) : ∑ i : Fin P.n, (P.points i.succ - P.points i.castSucc) = b - a

The subinterval lengths of a partition of [a,b] telescope to b - a: ∑ᵢ (x_{i+1} - x_i) = b - a.

theorem Integration.TaggedPartition.tag_mem_Icc {a b : ℝ} (T : TaggedPartition a b) (hab : a ≤ b) (i : Fin T.n) : T.tags i ∈ Set.Icc a b

Every tag ξ_i of a tagged partition of [a,b] lies in [a,b].

structure Integration.TaggedPartition.IsTaggedRefinement {a b : ℝ} (T T' : TaggedPartition a b) : Type

T' is a tagged refinement of T when every subinterval of T' is contained in some subinterval of T (witnessed by assign), and the subintervals of T' assigned to each T-subinterval telescope to its length. This captures the condition x ⊂ x' in Theorem II.

• assign : Fin T'.n → Fin T.n
• contained_left (j : Fin T'.n) : T.points (self.assign j).castSucc ≤ T'.points j.castSucc
• contained_right (j : Fin T'.n) : T'.points j.succ ≤ T.points (self.assign j).succ
• telescope (k : Fin T.n) : ∑ j : Fin T'.n with self.assign j = k, (T'.points j.succ - T'.points j.castSucc) = T.points k.succ - T.points k.castSucc

theorem Integration.riemannSum_eq_fiber {a b : ℝ} (f : ℝ → ℝ) (T T' : TaggedPartition a b) (href : T.IsTaggedRefinement T') : riemannSum f T = ∑ j : Fin T'.n, f (T.tags (href.assign j)) * (T'.points j.succ - T'.points j.castSucc)

The Riemann sum S_f(T) can be rewritten by summing over the refinement T': each summand uses the tag of T at the parent subinterval and the length of the finer T'-subinterval.

theorem Integration.riemannSum_sub_le_modulusOfContinuity_mul {a b : ℝ} (f : ℝ → ℝ) (T T' : TaggedPartition a b) (hab : a ≤ b) (hf : ContinuousOn f (Set.Icc a b)) (href : T.IsTaggedRefinement T') : |riemannSum f T - riemannSum f T'| ≤ modulusOfContinuity f a b T.mesh * (b - a)

Theorem II. If T' is a tagged refinement of T (i.e. x ⊂ x'), then for f ∈ C([a,b]), |S_f(T) - S_f(T')| ≤ w_f(‖T‖) · (b - a).

theorem Integration.riemannSum_sub_le_modulusOfContinuity_add_mul_of_commonRefinement {a b : ℝ} (f : ℝ → ℝ) (T₁ T₂ : TaggedPartition a b) (hab : a ≤ b) (hf : ContinuousOn f (Set.Icc a b)) (T'' : TaggedPartition a b) (href₁ : T₁.IsTaggedRefinement T'') (href₂ : T₂.IsTaggedRefinement T'') : |riemannSum f T₁ - riemannSum f T₂| ≤ (modulusOfContinuity f a b T₁.mesh + modulusOfContinuity f a b T₂.mesh) * (b - a)

Theorem III (given a common refinement). For tagged partitions T₁, T₂ that share a common tagged refinement T'', and f ∈ C([a,b]), |S_f(T₁) - S_f(T₂)| ≤ (w_f(‖T₁‖) + w_f(‖T₂‖)) · (b - a).

theorem Integration.telescope_sum_of_embedding {n'' m : ℕ} (pts : Fin (n'' + 1) → ℝ) (φ : Fin (m + 1) → Fin (n'' + 1)) (hφ_strict : StrictMono φ) (assign : Fin n'' → Fin m) (hassign_spec : ∀ (j : Fin n''), ↑(φ (assign j).castSucc) ≤ ↑j ∧ ↑j < ↑(φ (assign j).succ)) (k : Fin m) : ∑ j : Fin n'' with assign j = k, (pts j.succ - pts j.castSucc) = pts (φ k.succ) - pts (φ k.castSucc)

Telescoping identity: given a strictly monotone embedding φ of a coarse index set into a fine index set, the lengths of the fine subintervals whose indices are assigned to a coarse index k sum to the length of the k-th coarse subinterval.

theorem Integration.TaggedPartition.exists_commonRefinement {a b : ℝ} (T₁ T₂ : TaggedPartition a b) (hab : a ≤ b) : ∃ (T'' : TaggedPartition a b), Nonempty (T₁.IsTaggedRefinement T'') ∧ Nonempty (T₂.IsTaggedRefinement T'')

Any two tagged partitions of [a,b] admit a common tagged refinement: the partition whose points are the union of both partitions' points.

theorem Integration.riemannSum_sub_le_modulusOfContinuity_add_mul {a b : ℝ} (f : ℝ → ℝ) (T₁ T₂ : TaggedPartition a b) (hab : a ≤ b) (hf : ContinuousOn f (Set.Icc a b)) : |riemannSum f T₁ - riemannSum f T₂| ≤ (modulusOfContinuity f a b T₁.mesh + modulusOfContinuity f a b T₂.mesh) * (b - a)

Theorem III. For any two tagged partitions T₁, T₂ of [a,b] and f ∈ C([a,b]), |S_f(T₁) - S_f(T₂)| ≤ (w_f(‖T₁‖) + w_f(‖T₂‖)) · (b - a).

theorem Integration.riemannSum_cauchySeq_of_mesh_tendsto (f : ℝ → ℝ) (a b : ℝ) (hab_lt : a < b) (hf : ContinuousOn f (Set.Icc a b)) (T : ℕ → TaggedPartition a b) (hmesh : Filter.Tendsto (fun (r : ℕ) => (T r).mesh) Filter.atTop (nhds 0)) : CauchySeq fun (r : ℕ) => riemannSum f (T r)

For f ∈ C([a,b]) with a < b, if a sequence of tagged partitions has mesh tending to 0, then the corresponding sequence of Riemann sums is Cauchy.

theorem Integration.riemannSum_sub_tendsto_zero (f : ℝ → ℝ) (a b : ℝ) (hab_lt : a < b) (hf : ContinuousOn f (Set.Icc a b)) (T₁ T₂ : ℕ → TaggedPartition a b) (hmesh₁ : Filter.Tendsto (fun (r : ℕ) => (T₁ r).mesh) Filter.atTop (nhds 0)) (hmesh₂ : Filter.Tendsto (fun (r : ℕ) => (T₂ r).mesh) Filter.atTop (nhds 0)) : Filter.Tendsto (fun (r : ℕ) => riemannSum f (T₁ r) - riemannSum f (T₂ r)) Filter.atTop (nhds 0)

For f ∈ C([a,b]) with a < b, if two sequences of tagged partitions both have meshes tending to 0, then the difference of their Riemann sums tends to 0.

theorem Integration.riemann_integral_convergence (f : ℝ → ℝ) (a b : ℝ) (hab : a ≤ b) (hf : ContinuousOn f (Set.Icc a b)) : ∃ (I : ℝ), ∀ (T : ℕ → TaggedPartition a b), Filter.Tendsto (fun (r : ℕ) => (T r).mesh) Filter.atTop (nhds 0) → Filter.Tendsto (fun (r : ℕ) => riemannSum f (T r)) Filter.atTop (nhds I)

Convergence of the Riemann integral. For f ∈ C([a,b]), there exists a real number I such that for every sequence of tagged partitions whose mesh tends to 0, the Riemann sums converge to I.