Provedalphamulti-device-learningrepartitioning
Alpha's repartitioning laws
What the notation means · or point at any symbol
- e.fmap
- map of repartition(range(6), 3): Lean's dot notation e.map means map applied to e. (
(repartition (List.range 6) 3).map) - =Equality
- map(repartition(range(6), 3))(length) and [2, 2, 2] are the same. (
(repartition (List.range 6) 3).map List…) - ∧And
- Both hold: map(repartition(range(6), 3))(length) = [2, 2, 2], and map(repartition(range(6), 5))(length) = [2, 1, 1, 1, 1]. (
(repartition (List.range 6) 3).map List…) - 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) - range
- List.range: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (
List.range) - f(x)Function application
- List.range applied to 6. Lean writes f x; papers write f(x). (
List.range 6) - length
- List.length: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (
List.length) - [a, b]List
- The list of 2, 2, 2, in order. (
[2, 2, 2])
theorem alpha-repartition-six-samples :
(repartition (List.range 6) 3).map List.length = [2, 2, 2] ∧ (repartition (List.range 6) 5).map List.length = [2, 1, 1, 1, 1]Six samples on three owners are shares of 2, 2, 2, and on five owners of 2, 1, 1, 1, 1 (the gates resume four-owner checkpoints on three and five owners). 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
- None
- Proof
- 19 lines of Lean
Sign in to see the proofThe proof, its signed report and its history.