Maps of the line whose increments are dominated by a density

A map g defined on a set s ⊆ ℝ is said here to have its increments dominated by a density φ : ℝ → ℝ≥0∞ when

edist (g x) (g y) ≤ ∫⁻ t in Ioc x y, φ t for all x ≤ y in s.

This is the conclusion the fundamental theorem of calculus delivers for a C¹ map, with φ = ‖deriv g‖ₑ; it is also the conclusion the chord bound of the length–area method delivers for a holomorphic map restricted to a circular arc, with φ the angular length density (TauCeti.ofReal_dist_le_mul_lintegral_Ioc in Analysis/Complex/Conformal/LengthArea.lean). This file records three consequences of the domination on an order-connected s:

• With no finiteness assumption, Metric.ediam (g '' s) ≤ ∫⁻ t in s, φ t.
• If the total integral is finite and the target is a pseudo-metric space, g '' s is bounded.
• If the total integral is finite, g is uniformly continuous on s, even for a pseudo-emetric target.

Uniform continuity does not follow from bounded variation: domination by a finite integral is an absolute-continuity statement. The set s need only be order-connected, so a half-line and the whole line are covered along with Ioo a b, and φ need not be measurable, the integrals being lower integrals throughout.

Uniform continuity is what a boundary-limit argument spends: on a complete target it turns the Cauchy criterion at an endpoint of s into an honest limit there, so a map dominated by a density of finite integral over Ioo a b, where a < b, extends continuously to Icc a b. The results are therefore stated in the packaged UniformContinuousOn / Metric.ediam vocabulary rather than in ε–δ form; EMetric.uniformContinuousOn_iff_le (or Metric.uniformContinuousOn_iff_le) unpacks the first for a consumer that wants an explicit modulus, and Metric.isBounded_iff_ediam_ne_top the second.

The diameter and boundedness bounds are stated for any measure on a linear order. The diameter bound allows a weak pseudo-emetric target, and boundedness a pseudo-metric target. Uniform continuity uses Lebesgue measure on ℝ and a pseudo-emetric target.

Main results

• Set.OrdConnected.ediam_image_le_of_edist_le_setLIntegral: the image of an order-connected s under a map whose increments are dominated by φ has diameter at most ∫⁻ t in s, φ t.
• Set.OrdConnected.uniformContinuousOn_of_edist_le_setLIntegral: such a map is uniformly continuous on s as soon as the total integral is finite.
• Set.OrdConnected.isBounded_image_of_edist_le_setLIntegral: for a pseudo-metric target, the image is bounded as soon as the total integral is finite.

theorem Set.OrdConnected.ediam_image_le_of_edist_le_setLIntegral {α : Type u_1} {X : Type u_2} [LinearOrder α] [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace X] [WeakPseudoEMetricSpace X] {g : α → X} {φ : α → ENNReal} {s : Set α} (hs : s.OrdConnected) (hdom : ∀ x ∈ s, ∀ y ∈ s, x ≤ y → edist (g x) (g y) ≤ ∫⁻ (t : α) in Ioc x y, φ t ∂μ) : Metric.ediam (g '' s) ≤ ∫⁻ (t : α) in s, φ t ∂μ

A map whose increments are dominated by φ on an order-connected set has image diameter at most the total integral of φ. This holds for any measure on a linear order and a weak pseudo-emetric target; neither measurability of φ nor finiteness of the integral is required.

theorem Set.OrdConnected.uniformContinuousOn_of_edist_le_setLIntegral {X : Type u_1} [PseudoEMetricSpace X] {g : ℝ → X} {φ : ℝ → ENNReal} {s : Set ℝ} (hs : s.OrdConnected) (hdom : ∀ x ∈ s, ∀ y ∈ s, x ≤ y → edist (g x) (g y) ≤ ∫⁻ (t : ℝ) in Ioc x y, φ t) (hfin : ∫⁻ (t : ℝ) in s, φ t ≠ ⊤) : UniformContinuousOn g s

A map whose increments are dominated by a density of finite integral is uniformly continuous. For an order-connected s ⊆ ℝ and a map g with edist (g x) (g y) ≤ ∫⁻ t in Ioc x y, φ t for every increasing pair in s, finiteness of ∫⁻ t in s, φ t makes g uniformly continuous on s.

The modulus is uniform over s; in particular it does not degrade as an endpoint of s is approached. Finiteness of the total integral cannot be weakened to local integrability, which gives continuity but no uniform modulus, nor to bounded variation, which gives neither: a monotone jump function has bounded variation and is not uniformly continuous.

theorem Set.OrdConnected.isBounded_image_of_edist_le_setLIntegral {α : Type u_1} {X : Type u_2} [LinearOrder α] [MeasurableSpace α] {μ : MeasureTheory.Measure α} [PseudoMetricSpace X] {g : α → X} {φ : α → ENNReal} {s : Set α} (hs : s.OrdConnected) (hdom : ∀ x ∈ s, ∀ y ∈ s, x ≤ y → edist (g x) (g y) ≤ ∫⁻ (t : α) in Ioc x y, φ t ∂μ) (hfin : ∫⁻ (t : α) in s, φ t ∂μ ≠ ⊤) : Bornology.IsBounded (g '' s)

A map whose increments are dominated by a density of finite integral has bounded image. The finiteness form of Set.OrdConnected.ediam_image_le_of_edist_le_setLIntegral, for a pseudo-metric target.