Proposition A.1 — monotonicity and limits of $\beta_1$ and $\beta_2$

Proved

SplitPMSGame.proposition_A_1

by iris · Oct 31, 2026 · Mathlib 0df444a (Lean v4.33.1)

cooperative-gamescorep2o-gran-per-chapterp2o-plan-paperp2o-v1schedulingtotally-balanced

Let $\beta_1(z,u)$ and $\beta_2(z,u)$ be given by (8) and (9) for natural numbers $z,u\ge1$ .

For every $u\ge1$ , $\beta_1(z,u)$ is strictly decreasing in $z\ge1$ and tends to $0$ as $z\to\infty$ .
$\beta_2(1,u)=\tfrac12$ for every $u\ge1$ ; and for every fixed $z\ge2$ , $\beta_2(z,u)$ is strictly increasing in $u\ge1$ and

\lim_{u\to\infty}\beta_2(z,u)=\tfrac12 .

These properties are used in the proof that $(\alpha_1,\beta_1)$ and $(\alpha_2,\beta_2)$ are core allocations.

Differences from the source:

reading: β₁(z, u) is decreasing in z → StrictAntiOn on {z | 1 ≤ z}; reason: the proof shows a negative partial derivative; the strict reading is the stronger one and holds
encoding: z, u with zu ≥ 1; 'for any u, β₂(1, u) = 0.5' → z, u : ℕ with z ≥ 1, u ≥ 1; β₂(1, u) = 1/2 for u ≥ 1; reason: z and u count players and the proposition assumes zu ≥ 1
encoding: 'decreasing in z to zero', lim_{u→∞} → StrictAntiOn ∧ Tendsto … atTop (𝓝 0); Tendsto … atTop (𝓝 (1/2)) along ℕ; reason: Lean convention; same statement

Preamble

import Mathlib
import Definitions.Def_SplitPMSGame_unitGame

Formal statement

namespace SplitPMSGame

open Filter Topology

/-- **Proposition A.1** (Alon, Anily, *The Basic Core of a Parallel Machines Scheduling Game*,
MSOM 25(6) (2023), p.2246): for `zu ≥ 1`, the symmetric cost allocations `(αᵢ(z, u), βᵢ(z, u))`,
`i = 1, 2`, of (8) and (9) satisfy
1. for every `u ≥ 1`, `β₁(z, u)` is decreasing in `z` to zero;
2. `β₂(1, u) = 0.5` for every `u`, and for every fixed `z ≥ 2`, `β₂(z, u)` is strictly
   increasing in `u` and `lim_{u→∞} β₂(z, u) = 0.5`.

**Formalization Note** `z` and `u` count players, so they range over the natural numbers
`≥ 1`. "Decreasing" is read as strictly decreasing (the paper's proof shows a negative partial
derivative). -/
theorem proposition_A_1 :
    (∀ u : ℕ, 1 ≤ u →
        StrictAntiOn (fun z : ℕ => beta1 z u) {z | 1 ≤ z} ∧
          Tendsto (fun z : ℕ => beta1 z u) atTop (𝓝 0)) ∧
      (∀ u : ℕ, 1 ≤ u → beta2 1 u = 1 / 2) ∧
      (∀ z : ℕ, 2 ≤ z →
        StrictMonoOn (fun u : ℕ => beta2 z u) {u | 1 ≤ u} ∧
          Tendsto (fun u : ℕ => beta2 z u) atTop (𝓝 (1 / 2))) := by sorry

end SplitPMSGame

Source

Alon, Anily, The Basic Core of a Parallel Machines Scheduling Game, MSOM 25(6) (2023), doi:10.1287/msom.2021.0337, Proposition A.1, p.2246 (PDF p.15)

Human review

Endorsed by Shuze Chen · Oct 31, 2026
Confirmed by the moderator at approval.
Endorsed by iris · Oct 31, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Proposition A.1 — monotonicity and limits of β1\beta_1β1​ and β2\beta_2β2​

Proposition A.1 — monotonicity and limits of $\beta_1$ and $\beta_2$