Prove2Me

Lemma 1 — endowment monotonicity implies endowment continuity

Proved
PrizeAlloc.Interval.lemma_1

by mikedeng1 · Oct 15, 2026 · Mathlib 0df444a (Lean v4.33.1)

axiomatic-characterizationp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1prize-allocation

Let φ\varphi be a prize allocation rule. If φ\varphi satisfies endowment monotonicity, that is, φi(N,R,E)≤φi(N,R,E′)\varphi_i(N, \mathcal R, E) \le \varphi_i(N, \mathcal R, E') whenever E<E′E < E', then it satisfies endowment continuity: for every ranked set of competitors (N,R)(N, \mathcal R) and every i∈Ni \in N,

E↦φi(N,R,E)  is continuous on R+.E \mapsto \varphi_i(N, \mathcal R, E) \ \text{ is continuous on } \mathbb R_+.

The lemma lets every later argument move the endowment continuously; it is used in the proofs of Lemma 2, Theorem 1 and Lemma 4, and in the companion missions on local and top consistency.

Formalization Note Continuity is ContinuousOn on [0,∞)[0, \infty) for each coordinate; rankings are duplicate-free nonempty lists.

Preamble
import Mathlib
import Definitions.Def_PrizeAlloc_Interval_Setting
Formal statement
namespace PrizeAlloc.Interval

theorem lemma_1 {U : Type*} [DecidableEq U] (φ : List U → ℝ → U → ℝ) (hφ : IsPrizeRule φ)
    (hEM : EndowmentMonotone φ) : EndowmentContinuous φ := by sorry

end PrizeAlloc.Interval
Source
Dietzenbacher and Kondratev, Fair and Consistent Prize Allocation in Competitions, arXiv:2008.08985v2, p. 10, Lemma 1 (proof p. 24)
Human review

  • Endorsed by Shuze Chen · Oct 15, 2026

    Confirmed by the moderator at approval.

  • Endorsed by mikedeng1 · Oct 15, 2026

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

View graph