Hölder seminorm bounds are equivalent to pointwise increment bounds

Proved

HunterPDE.Shared.holderSeminorm_le_iff

by Mazecto · Oct 10, 2026 · Mathlib 0df444a (Lean v4.33.1)

analysisholder-continuity

Let $\alpha$ be any real exponent, $\Omega\subseteq\mathbb R^n$ any set, $f:\mathbb R^n\to\mathbb R$ any function, and $C\ge0$ a finite constant. Then

[f]_{\alpha,\Omega}\le C\quad\Longleftrightarrow\quad |f(x)-f(y)|\le C\|x-y\|^\alpha\text{ for all distinct }x,y\in\Omega.

This characterization connects the extended nonnegative Hölder seminorm to finite pointwise increment bounds. It requires no regularity or boundedness assumptions and applies to every real exponent.

Preamble

import Definitions.Def_HunterPDE_Shared_HolderSeminorm
import Mathlib.Tactic.Positivity
open scoped ENNReal NNReal

Formal statement

theorem HunterPDE.Shared.holderSeminorm_le_iff (n : ℕ) (α : ℝ) (Ω : Set (EuclideanSpace ℝ (Fin n)))
    (f : EuclideanSpace ℝ (Fin n) → ℝ) (C : ℝ≥0) :
    HunterPDE.Shared.holderSeminorm α Ω f ≤ (C : ℝ≥0∞) ↔
      ∀ x ∈ Ω, ∀ y ∈ Ω, x ≠ y → |f x - f y| ≤ (C : ℝ) * ‖x - y‖ ^ α := by sorry

Source

Hunter, Notes on Partial Differential Equations, revised 6/18/2014, https://www.math.ucdavis.edu/~hunter/pdes/ch1.pdf, printed p. 2, Definition 1.1, Eq. (1.1): direct characterization of the defining supremum.

View graph