TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-27

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

If $∣ f (x) - f (y) ∣ \leq C ∣ x - y ∣^{α}$ on an interval for some rational $α > 1$ then $f$ is constant

Statement

Let $I \subseteq R$ be order-convex (Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length), let $f : I \to R$ , let $C \in R$ with $C \geq 0$ , and let $α \in Q$ with $α > 1$ (Order on the rationals). Suppose

$∣ f (x) - f (y) ∣ \leq C ∣ x - y ∣^{α} for all x, y \in I,$

the power being the rational power of a nonnegative base (Rational powers $a^{r}$ of a positive base, with the convention $0^{α} = 0$ for $α > 0$ ). Then $f$ is constant on $I$ : $f (x) = f (y)$ for all $x, y \in I$ .

The hypothesis is written out, and not expressed through Lipschitz map, $α$ -Hölder map for rational $0 < α \leq 1$ , and contraction, because it cannot be. That definition introduces the $α$ -Hölder condition for rational $α$ with $0 < α \leq 1$ only, and says explicitly that no claim is made about an exponent above $1$ . The displayed inequality is the natural extension of the formula to $α > 1$ , and this theorem is what that extension is worth: for rational $0 < α \leq 1$ the same inequality is the $α$ -Hölder condition of Lipschitz map, $α$ -Hölder map for rational $0 < α \leq 1$ , and contraction instantiated at $I \subseteq R$ by Dictionary: for $A \subseteq R$ with the metric $d (x, y) = ∣ x - y ∣$ , continuity and uniform continuity of $f : A \to R$ agree with the metric-space notions, the Lipschitz and Hölder conditions are the metric ones instantiated, and a subset of $R$ is compact in the open-cover sense of $R$ exactly when it is a compact metric subspace, clause 4, and then it makes $f$ uniformly continuous, hence continuous (Contraction implies Lipschitz implies uniformly continuous implies continuous; every Hölder map is uniformly continuous, and a Lipschitz map on a bounded space is Hölder for every exponent, Continuity of $f : A \to R$ at a point of $A$ and on $A$ : the $ε$ - $δ$ condition, its agreement with $\lim_{x \to c} f (x) = f (c)$ at a limit point, and continuity at an isolated point); above $1$ it makes $f$ constant, which is why the definition stops at $1$ .

Order-convexity is essential. On a domain that is not order-convex the conclusion fails: on $I = {0} \cup {1}$ the function $f (0) = 0$ , $f (1) = 1$ satisfies the inequality with $C = 1$ and any $α$ , and is not constant. What the proof uses is that the whole segment between two points of $I$ lies in $I$ , so that the distance between them can be subdivided.

Facts & Assumptions

Given: An order-convex $I \subseteq R$ , a function $f : I \to R$ , a real $C \geq 0$ and a rational $α > 1$ with $∣ f (x) - f (y) ∣ \leq C ∣ x - y ∣^{α}$ for all $x, y \in I$ . Natural numbers are identified with their canonical images in $R$ , as elsewhere in this library.

[L1]

Order-convexity: $x, y \in I$ with $x \leq z \leq y$ gives $z \in I$ (Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length).

[L2]

Rational powers of a positive base: $a^{r}$ is defined for $a > 0$ and $r \in Q$ , with $a^{1} = a$ and $a^{q / 1} = a^{q}$ agreeing with the integer power; and $0^{r} = 0$ for rational $r > 0$ (Rational powers $a^{r}$ of a positive base, Existence and uniqueness of $n$ -th roots: a unique $a^{1 / n} \geq 0$ with $(a^{1 / n})^{n} = a$ , Integer powers $a^{m}$ ).

[L3]

Laws of rational exponents for $a, b > 0$ and $r, s \in Q$ : $a^{r} > 0$ ; $a^{r + s} = a^{r} a^{s}$ ; $(a b)^{r} = a^{r} b^{r}$ ; $a^{- r} = 1 / a^{r}$ ; $(a^{r})^{s} = a^{r s}$ (Laws of rational exponents).

[L4]

Monotonicity of rational powers: for $a > 1$ and rationals $r < s$ one has $a^{r} < a^{s}$ ; and for rational $r > 0$ and $0 < a < b$ one has $a^{r} < b^{r}$ (Monotonicity of $r \mapsto a^{r}$ and of $a \mapsto a^{r}$ ).

[L5]

Finite sums: $\sum_{k < n} (c_{k + 1} - c_{k}) = c_{n} - c_{0}$ ; $\sum_{k < n} λ = n λ$ ; and $∣ \sum_{k < n} a_{k} ∣ \leq \sum_{k < n} ∣ a_{k} ∣$ (Laws of finite sums and finite products, Finite sums and finite products, by recursion, Triangle inequality for finite sums).

[L6]

Archimedean property: for every real $t$ there is a natural $m \geq 1$ with $t < m$ ; and for every real $η > 0$ there is a natural $q \geq 1$ with $1 / q < η$ (Every complete ordered field is Archimedean, For every $ε > 0$ in a complete ordered field there is a natural $n \geq 1$ with $1 / n < ε$ ).

[L7]

Reciprocals: $0 < s \leq t$ implies $0 < 1 / t \leq 1 / s$ , and $0 < s < t$ implies $1 / t < 1 / s$ (Inverses of positives are positive, and reciprocation reverses order).

[L8]

Absolute value and ordered-field arithmetic: $∣ u ∣ \geq 0$ ; $∣ u ∣ = 0$ exactly when $u = 0$ ; $∣ u ∣ = u$ for $u \geq 0$ ; the order is total; a real that is $\geq 0$ and smaller than every positive real is $0$ (Basic properties of the absolute value, Ordered field, Complete ordered field (least-upper-bound property)).

Proof

technique · direct

1.1

Normalisations. Since $∣ x - y ∣^{α} \geq 0$ by [L2] and [L3], the hypothesis with the constant $C$ implies the same inequality with the constant $C + 1 > 0$ ; so we may and do assume $C > 0$ . Also, the hypothesis and the conclusion are symmetric in $x$ and $y$ and are trivial when $x = y$ , so it suffices to prove $f (x) = f (y)$ for $x, y \in I$ with $x < y$ ; fix such a pair and put $A : = C (y - x)^{α}$ , a real with $A > 0$ by [L3].

L2L3L8suffices: prove it for C positive and x strictly less than y

1.2

The exponent gap. Put $β : = α - 1$ , a rational with $β > 0$ . By [L6] fix a natural $q \geq 1$ with $1 / q < β$ .

L6choose

1.3

Subdividing. Let $n \in N$ with $n \geq 1$ and put $h : = (y - x) / n > 0$ and $t_{k} : = x + k h$ for $k \in N$ . For $k \leq n$ one has $x \leq t_{k} \leq y$ , so $t_{k} \in I$ by [L1]; and $∣ t_{k + 1} - t_{k} ∣ = h$ for $k < n$ . Define the sequence $c : N \to R$ by $c_{k} : = f (t_{\min {k, n}})$ , so that $c_{0} = f (x)$ , $c_{n} = f (y)$ , and $c_{k + 1} - c_{k} = f (t_{k + 1}) - f (t_{k})$ for every $k < n$ .

L1L8

2.1

The telescoped estimate. By [L5], $f (y) - f (x) = c_{n} - c_{0} = \sum_{k < n} (c_{k + 1} - c_{k})$ , hence $∣ f (y) - f (x) ∣ \leq \sum_{k < n} ∣ c_{k + 1} - c_{k} ∣ = \sum_{k < n} ∣ f (t_{k + 1}) - f (t_{k}) ∣ \leq \sum_{k < n} C h^{α} = n C h^{α}$ , the middle inequality being the hypothesis applied to the pair $t_{k}, t_{k + 1}$ of points of $I$ and the last equality being the constant-sum rule of [L5].

step 1.3L5

2.2

The bound can be made arbitrarily small. Let a real $η > 0$ be given and put $R : = A / η > 0$ . By [L6] fix a natural $N$ with $R^{q} < N$ ; then $N \geq 1$ , since $R^{q} > 0$ by [L3] and [L2]. By [L4] applied with the rational exponent $1 / q > 0$ to the bases $R^{q} < N$ , and by [L2] and [L3] which give $(R^{q})^{1 / q} = R^{q \cdot (1 / q)} = R^{1} = R$ , we get $N^{1 / q} > R$ .

step 1.1step 1.2L2L3L4L6choose

3.1

Rewriting the bound. By [L3], $h^{α} = ((y - x) \cdot n^{- 1})^{α} = (y - x)^{α} (n^{- 1})^{α} = (y - x)^{α} n^{- α}$ , and $n n^{- α} = n^{1} n^{- α} = n^{1 - α} = n^{- β} = 1 / n^{β}$ . Hence $n C h^{α} = A / n^{β}$ , and step 2.1 gives $∣ f (y) - f (x) ∣ \leq A / n^{β}$ for every natural $n \geq 1$ .

step 1.1step 1.2step 2.1L2L3

3.2

By [L4], $N^{1 / q} \leq N^{β}$ : this is an equality if $N = 1$ , since then both sides are $1$ by [L3], and it is the strict inequality of [L4] for the base $N > 1$ and the exponents $1 / q < β$ . Hence $N^{β} \geq N^{1 / q} > R > 0$ , so $1 / N^{β} < 1 / R$ by [L7] and therefore $A / N^{β} < A / R = η$ .

step 1.2step 2.2L3L4L7

4.1

Combining steps 3.1 and 3.2, $∣ f (y) - f (x) ∣ \leq A / N^{β} < η$ . The real $η > 0$ was arbitrary and $∣ f (y) - f (x) ∣ \geq 0$ , so $∣ f (y) - f (x) ∣ = 0$ by [L8], that is $f (y) = f (x)$ . Since $x < y$ in $I$ were arbitrary, and by the reduction of step 1.1, $f$ is constant on $I$ .

step 1.1step 3.1step 3.2L8∎

Remarks

The mechanism in one line. Splitting $[x, y]$ into $n$ equal pieces costs $n$ applications of the hypothesis, each of size $C (∣ x - y ∣ / n)^{α}$ , for a total of $C ∣ x - y ∣^{α} n^{1 - α}$ . For $α = 1$ the factor $n^{1 - α}$ is $1$ and the estimate says nothing new; for $α < 1$ it grows and the estimate is useless; only for $α > 1$ does it tend to $0$ , and then it forces the increment to vanish.
Why the vanishing of $n^{1 - α}$ is proved rather than asserted. Neither real exponents nor a general theorem of the form $n^{- β} \to 0$ is available at this point in the reading order, so the proof supplies the one rational instance it needs. The general real-power theory is developed later in Real powers for positive bases, with the zero-base positive-exponent convention ↗. Steps 2.2 and 3.2 supply the one instance that is needed, by reducing to the exponent $1 / q$ with $q$ a natural number, where the $q$ -th root of Existence and uniqueness of $n$ -th roots: a unique $a^{1 / n} \geq 0$ with $(a^{1 / n})^{n} = a$ and the Archimedean property do the work.
The boundary case $α = 1$ is exactly the Lipschitz condition, which does not force constancy: the identity is $1$ -Lipschitz and not constant. So the theorem is sharp at the endpoint of the range that Lipschitz map, $α$ -Hölder map for rational $0 < α \leq 1$ , and contraction admits, and the strict nesting of the classes below $1$ is witnessed on the companion page by On $[0, 1]$ the function $x^{β}$ is $β$ -Hölder and is $α$ -Hölder for no rational $α > β$ , so the Hölder classes are strictly nested ↗.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

77 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Hölder condition (Wikipedia) (standard reference, not scraped)
Lipschitz continuity (Wikipedia) (standard reference, not scraped)
J. Lebl, Basic Analysis I, §3.4 (standard reference, not scraped)
Cornell numerical methods notes: Calculus (standard reference, not scraped)

If ∣f(x)−f(y)∣≤C∣x−y∣α∣f(x)−f(y)∣≤C∣x−y∣α on an interval for some rational α>1α>1 then ff is constant