Alphabeta Math
DefinitionDefinition: AI-adaptedProof: Not applicablejudge pass (deepseek-v4-pro + gpt-5.6-terra)verified 2026-08-03 (gpt-5.6-sol-codex-subscription)
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.

Lipschitz map, α-Hölder map for rational 0<α≤1, and contraction

Definition

Let (X,dX) and (Y,dY) be metric spaces (Metric space: d(x,y)=0 iff x=y, symmetry, and the triangle inequality; pseudometric and ultrametric) and let f:X→Y be a function. Recall that a metric takes nonnegative real values (Nonnegativity of a metric is a consequence of the other axioms, not an axiom).

  • f is Lipschitz with constant L, where L∈R and L≥0, if dY(f(x),f(x′))  ≤  L dX(x,x′)for all x,x′∈X. f is Lipschitz if it is Lipschitz with some such constant.
  • Let α∈Q with 0<α≤1 (Order on the rationals). f is α-Hölder with constant C, where C∈R and C≥0, if dY(f(x),f(x′))  ≤  C dX(x,x′)αfor all x,x′∈X, the power being the rational power of a nonnegative base (Rational powers ar of a positive base). f is α-Hölder if it is so with some such constant, and Hölder if it is α-Hölder for some rational α∈(0,1].
  • f is a contraction with constant q if it is Lipschitz with constant q and 0≤q<1. The number q is then called a contraction constant for f.

The power dX(x,x′)α is defined at every pair, including x=x′. The base dX(x,x′) is a nonnegative real, and Rational powers ar of a positive base defines aα for every a>0 and, by its supplementary clause, sets 0α=0 for every rational α>0. Since α>0 is required here, the displayed inequality at x=x′ reads 0≤C⋅0, which holds; so no separate clause and no restriction to x≠x′ is needed. Note that this does not by itself explain the strict inequality α>0: if one extended the formula to α=0 using the convention 00=1 of Integer powers am, the equal-point inequality would still be the automatic 0≤C. Globally, however, that extension would reduce to the bounded-diameter condition dY(f(x),f(x′))≤C, outside the standard Hölder range adopted here.

Why the exponent is rational on this page and why it is at most 1. At this point in the reading order only rational powers are available (Rational powers ar of a positive base), so α ranges over the rationals. The upper bound α≤1 is the standard convention, and it is where the notion is useful: the classical theory reserves the name for α∈(0,1], and nothing in this library uses an exponent outside that range. No claim is made here about what an exponent α>1 would do.

Constants are not unique and are not part of the data. If f is Lipschitz with constant L it is Lipschitz with every constant L′≥L, and likewise for Hölder constants; the adjectives above are existential statements. A contraction, by contrast, requires a constant strictly below 1, and that is a real restriction: exhibiting the constant is part of exhibiting a contraction, and a map that shrinks every distance without admitting one uniform constant is not a contraction here.

Remarks

Depends on

Used by

…and 15 more results.

Dependency tree · two levels

33 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