An unbounded integrable derivative of a monotone function has integral zero and dense small values
ProvedRudin.ch06_unbounded_monotone_integrator_criterionLet be monotonically increasing and differentiable at every point of , and suppose its derivative is unbounded above on . This theorem says that if on then
The upper and lower integrals here are the ordinary supremum and infimum of sets of reals, which take the default value on a set unbounded in the relevant direction. Since increases, , so every term of an upper sum is nonnegative, while the one-interval partition of produces the supremum of an unbounded set and hence the value : the upper integral is exactly , and integrability transports this to the lower integral.
For the second assertion, no default value intervenes in the lower sums, because makes every infimum genuine. If the derivative were bounded below by some on a subinterval , then the partition with division points would have lower sum at least ; the mean value theorem bounds every lower sum by the total increment , so the lower integral is a genuine supremum and would be positive, contradicting its vanishing.
The statement is the converse half of the criterion recorded in Rudin.ch06_singular_integrator_refutes: a monotone integrator whose derivative is unbounded and Riemann integrable in this sense is necessarily a singular integrator in the sense used there. Together the two results say that the versions of Rudin's Theorems 6.17, 6.21 and 6.22 stated without the boundedness hypothesis of Definition 6.2 fail exactly when such an integrator exists.
import Mathlib import Definitions.Def_Rudin_ch06_stieltjes open Filter Topology
namespace Rudin
/-- For a monotone, everywhere differentiable integrator whose derivative is unbounded above on
`[0,1]`, Riemann integrability of the derivative forces the integral to vanish and the derivative
to take arbitrarily small values on every nondegenerate subinterval. -/
theorem ch06_unbounded_monotone_integrator_criterion (α : ℝ → ℝ) (hmono : Monotone α)
(hdiff : ∀ x ∈ Set.Icc (0:ℝ) 1, HasDerivAt α (deriv α x) x)
(hunb : ∀ K : ℝ, ∃ x ∈ Set.Icc (0:ℝ) 1, K < deriv α x)
(hint : RiemannIntegrable 0 1 (deriv α)) :
RiemannIntegral 0 1 (deriv α) = 0 ∧
∀ u v : ℝ, 0 ≤ u → u < v → v ≤ 1 → ∀ ε > 0, ∃ x ∈ Set.Icc u v, deriv α x < ε := by sorry
end Rudin