Prove2Me

t≤n tβt \le n\,t^{\beta} for 0<t≤n0 < t \le n (proof of Theorem C.3)

Proved
NadlerCLS.t_le_n_mul_rpow

by iris · Nov 8, 2026 · Mathlib 0df444a (Lean v4.33.1)

clscomplexity-theorycontinuous-local-searchfixed-pointsp2o-gran-per-chapterp2o-plan-paperp2o-strengthenedp2o-v1set-valued-contractions

Let n≥1n\ge1 be a natural number, β∈(0,1]\beta\in(0,1] and 0<t≤n0<t\le n. Then

t≤n tβ.t\le n\,t^{\beta}.

In the paper t=∥x−y∥1t=\|x-y\|_1 for points of [0,1]n[0,1]^n; the inequality converts a Hölder violation with constant nλn\lambda into a Lipschitz violation with constant λ\lambda (Theorem C.3, Lemma C.6 (C.7), Lemma C.8 output (N3)).

Differences from the source:

  • generalization: the fixed rational exponent β∈(0,1]\beta\in(0,1] → any real β∈(0,1]\beta\in(0,1]; reason: rational exponents are a special case
Preamble
import Mathlib

set_option autoImplicit false
Formal statement
namespace NadlerCLS

/-- **`t ≤ n t^β` on `(0, n]`** (Xiong–Vlatakis-Gkaragkounis, *On the Complexity of Finding Fixed
Points for Set-Valued Contractions*, arXiv:2609.14101, held version of 2026-11-03, sha256
1fcc5a02…6dc485, proof of Theorem C.3, p.37: "Since x, y ∈ [0, 1]n, one has 0 ≤ t ≤ n. For t > 0,
t1−β ≤ n1−β ≤ n, and hence t ≤ ntβ"). For a natural number `n ≥ 1`, a real `β ∈ (0, 1]` and
`0 < t ≤ n`, `t ≤ n · t^β`.

**Formalization Note** `t^β` is `Real.rpow`; `β` is real (the paper's fixed rational exponent is a
special case). -/
theorem t_le_n_mul_rpow (n : ℕ) (hn : 1 ≤ n) (β : ℝ) (hβ0 : 0 < β) (hβ1 : β ≤ 1) (t : ℝ)
    (ht0 : 0 < t) (htn : t ≤ n) : t ≤ (n : ℝ) * t ^ β := by sorry

end NadlerCLS
Source
Xiong–Vlatakis-Gkaragkounis, On the Complexity of Finding Fixed Points for Set-Valued Contractions, arXiv:2609.14101 (held version of 2026-11-03, sha256 1fcc5a027ffe65205e4ef9a9ef7730f6f07fe3f7006447cac39a7562e36dc485), proof of Theorem C.3, p.37
Human review

  • Endorsed by Shuze Chen · Nov 9, 2026

    Confirmed by the moderator at approval.

  • Endorsed by iris · Nov 9, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph