Provedalphamulti-device-learningrepartitioning

Repartitioned shares differ by at most one sample

For all $\htmlData{mx=1}{\alpha \in \htmlData{mx=0}{\operatorname{Type}}}$ , $\htmlData{mx=3}{\mathit{xs} \in \htmlData{mx=2}{\htmlData{mx=0}{\operatorname{List}}\,\htmlData{mx=1}{\alpha}}}$ and $\htmlData{mx=1}{\mathit{owners} \in \htmlData{mx=0}{\mathbb{N}}}$ , if $0 \mathrel{\htmlData{mx=1}{<}} \htmlData{mx=0}{\mathit{owners}}$ , then

\begin{aligned} & \htmlData{mx=9}{\operatorname{length}\left(\htmlData{mx=8}{\htmlData{mx=5}{\operatorname{repartition}}(\htmlData{mx=6}{\mathit{xs}}, \htmlData{mx=7}{\mathit{owners}})}\right)} \mathrel{\htmlData{mx=11}{=}} \htmlData{mx=10}{\mathit{owners}} \\ & \htmlData{mx=0}{\land} \htmlData{mx=12}{\forall} s, \\ & \quad \htmlData{mx=14}{s} \mathrel{\htmlData{mx=16}{<}} \htmlData{mx=15}{\mathit{owners}} \\ & \quad \htmlData{mx=13}{\implies} \htmlData{mx=28}{\operatorname{length}\left(\htmlData{mx=27}{\htmlData{mx=23}{\operatorname{repartitionShare}}(\htmlData{mx=24}{\mathit{xs}}, \htmlData{mx=25}{\mathit{owners}}, \htmlData{mx=26}{s})}\right)} \\ & \quad \quad \htmlData{mx=17}{=} \htmlData{mx=42}{\htmlData{mx=33}{\frac{\htmlData{mx=31}{\operatorname{length}\left(\htmlData{mx=30}{\mathit{xs}}\right)}}{\htmlData{mx=32}{\mathit{owners}}}} + \left(\htmlData{mx=41}{\begin{cases} 1 & \text{if } \htmlData{mx=34}{s} \mathrel{\htmlData{mx=40}{<}} \htmlData{mx=39}{\htmlData{mx=37}{\operatorname{length}\left(\htmlData{mx=36}{\mathit{xs}}\right)} \bmod \htmlData{mx=38}{\mathit{owners}}} \\ 0 & \text{otherwise} \end{cases}}\right)} \end{aligned}

What the notation means · or point at any symbol

Type: Type: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Type)
List: List: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (List)
f(x)Function application: List applied to α. Lean writes f x; papers write f(x). (List α)
NNatural numbers: The natural numbers 0, 1, 2, …. In Lean they start at 0. (Nat)
<Less than: 0 is strictly smaller than owners. (0 < owners)
e.flength: length of repartition(xs, owners): Lean's dot notation e.length means length applied to e. ((repartition xs owners).length)
=Equality: length(repartition(xs, owners)) and owners are the same. ((repartition xs owners).length = owners)
∧And: Both hold: length(repartition(xs, owners)) = owners, and ∀ s, s < owners → length(repartitionShare(xs, owners, s)) …. ((repartition xs owners).length = owners…)
repartition: repartition: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (repartition)
∀For all: The statement after the comma holds for every s. (∀ s, s < owners → (repartitionShare xs …)
⟹Implies: If s < owners, then length(repartitionShare(xs, owners, s)) = xs.length/owners…. (Between types, A → B is the type of functions from A to B.) (s < owners → (repartitionShare xs owner…)
repartitionShare: repartitionShare: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (repartitionShare)
a/bDivision: xs.length divided by owners. In Lean, dividing by 0 gives 0. (xs.length / owners)
+Addition: xs.length/owners plus 1 if s < xs.length % owners, else 0. (xs.length / owners + (if s < xs.length …)
{ a if c; b otherwiseCases (if … then … else): 1 when s < xs.length % owners, and 0 otherwise. (if s < xs.length % owners then 1 else 0)
modRemainder: The remainder when xs.length is divided by owners. (xs.length % owners)

theorem alpha-repartition-balanced-shares {α : Type} (xs : List α) (owners : Nat) (hn : 0 < owners) :
    (repartition xs owners).length = owners ∧ ∀ s, s < owners → (repartitionShare xs owners s).length = xs.length / owners + (if s < xs.length % owners then 1 else 0)

There are owners shares; share s holds floor(n / owners) samples plus one for the first n mod owners shares. Model: definition alpha-multi-device-learning (revision 01a1255c-84f1-7e7f-a994-fc8c2d274bee).

How it was proved

Proved: 10 October 2026
By: Ajax
Checked by: Lean's kernel (Lean 4.33.1, with Mathlib); the proof is signed and replays offline
Axioms: Quot.sound, propext
Proof: 28 lines of Lean

Repartitioned shares differ by at most one sample

How it was proved

More proved statements