Balanceable partitions
Definition\(k\)-bounded partition#✓fully proved
A partition of \(n\) is \(k\)-bounded if each of its parts is at most \(k\).
For example, \(12 = 3 + 2 + 2 + 2 + 2 + 1\) is a \(3\)-bounded partition of \(12\).
def Bounded {n : ℕ} (k : ℕ) (p : n.Partition) : Prop :=
∀ i ∈ p.parts, i ≤ kUsed by 1
DefinitionBalanceable partition#✓fully proved
A partition of \(n\) is balanceable if its multiset of parts can be split as \(s_1 + s_2\) into two multisets \(s_1\) and \(s_2\) whose elements have equal sums.
For example, \(12 = (3 + 2 + 1) + (2 + 2 + 2)\) is a balanceable partition of \(12\).
def Balanceable {n : ℕ} (p : n.Partition) : Prop :=
∃ s₁ s₂, s₁ + s₂ = p.parts ∧ s₁.sum = s₂.sumUsed by 1
TheoremSmallest size forcing bounded partitions to be balanceable#●ready to prove
For every integer \(k \ge 1\), the smallest positive integer \(n\) such that every \(k\)-bounded partition of \(n\) is balanceable is \(2 \operatorname{lcm}(1, 2, \ldots, k)\).
public theorem_wanted minimal_balanceable_of_bounded (k : ℕ) (hk : 0 < k) :
Minimal (fun n => 0 < n ∧ ∀ p : n.Partition, Bounded k p → Balanceable p) (2 * (Finset.Icc 1 k).lcm id)def Bounded {n : ℕ} (k : ℕ) (p : n.Partition) : Prop :=
∀ i ∈ p.parts, i ≤ kWantedExt/Combinatorics/BalanceableBoundedPartitionsWanted.lean:52
def Balanceable {n : ℕ} (p : n.Partition) : Prop :=
∃ s₁ s₂, s₁ + s₂ = p.parts ∧ s₁.sum = s₂.sumWantedExt/Combinatorics/BalanceableBoundedPartitionsWanted.lean:62
Sources
- https://projecteuler.net/problem=772. Problem
balanceable_bounded_partitionsof the lean-eval benchmark.
Uses 2
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.