A singular integrator refutes the unbounded forms of Theorems 6.17, 6.21 and 6.22
ProvedRudin.ch06_singular_integrator_refutesIn this formalization the upper and lower integrals are the ordinary sSup/sInf of sets of reals, which return the default value on a set that is unbounded in the relevant direction. Rudin's Chapter 6 assumes throughout that the integrand is bounded, and the three statements of the chapter that omit that clause — Theorem 6.17 (reduction of a Stieltjes integral to a Riemann integral with a density), Theorem 6.21 (the fundamental theorem of calculus) and Theorem 6.22 (integration by parts) — are all refuted at once by a single object.
Call a function a singular integrator if it is monotonically increasing, differentiable at every point of , satisfies , has derivative unbounded above on , and has
This theorem asserts that the existence of such an makes all three unbounded statements false.
The mechanism is the default value of the suprema and infima. Since is increasing, , so every infimum occurring in a lower sum is a genuine infimum and every term of an upper sum is nonnegative. The one-interval partition of has a single supremum, which is the supremum of an unbounded set and therefore evaluates to , so the upper integral of is ; the dense small values force every lower sum to vanish, so the lower integral is as well. Hence with
even though grows. Taking (which is bounded, and whose upper and lower sums telescope to ) contradicts the conclusion of Theorem 6.17; taking contradicts Theorem 6.21; and taking , , contradicts Theorem 6.22, whose right-hand side is then while its left-hand side is .
import Mathlib import Definitions.Def_Rudin_ch06_stieltjes open Filter Topology
namespace Rudin
/-- If there is a monotone, everywhere differentiable integrator `α` on `[0,1]` whose derivative
is unbounded above and takes arbitrarily small values on every nondegenerate subinterval, then the
unbounded forms of Rudin's Theorems 6.17, 6.21 and 6.22 all fail. -/
theorem ch06_singular_integrator_refutes (α : ℝ → ℝ) (hmono : Monotone α)
(hdiff : ∀ x ∈ Set.Icc (0:ℝ) 1, HasDerivAt α (deriv α x) x)
(hgrow : α 0 < α 1)
(hunb : ∀ K : ℝ, ∃ x ∈ Set.Icc (0:ℝ) 1, K < deriv α x)
(hsmall : ∀ u v : ℝ, 0 ≤ u → u < v → v ≤ 1 → ∀ ε > 0, ∃ x ∈ Set.Icc u v, deriv α x < ε) :
(¬ ∀ (a b : ℝ), a ≤ b → ∀ (f β : ℝ → ℝ), MonotoneOn β (Set.Icc a b) →
(∀ x ∈ Set.Icc a b, HasDerivAt β (deriv β x) x) →
RiemannIntegrable a b (deriv β) →
(∃ M, ∀ x ∈ Set.Icc a b, |f x| ≤ M) →
(RSIntegrable a b f β ↔ RiemannIntegrable a b (fun x => f x * deriv β x)) ∧
(RSIntegrable a b f β →
RSIntegral a b f β = RiemannIntegral a b (fun x => f x * deriv β x)))
∧ (¬ ∀ (a b : ℝ), a ≤ b → ∀ (f F : ℝ → ℝ), RiemannIntegrable a b f →
(∀ x ∈ Set.Icc a b, HasDerivAt F (f x) x) → RiemannIntegral a b f = F b - F a)
∧ (¬ ∀ (a b : ℝ), a ≤ b → ∀ (F G f g : ℝ → ℝ),
(∀ x ∈ Set.Icc a b, HasDerivAt F (f x) x) →
(∀ x ∈ Set.Icc a b, HasDerivAt G (g x) x) →
RiemannIntegrable a b f → RiemannIntegrable a b g →
RiemannIntegral a b (fun x => F x * g x) =
F b * G b - F a * G a - RiemannIntegral a b (fun x => f x * G x)) := by sorry
end Rudin