diff --git a/LeanEval/Combinatorics/BalanceableBoundedPartitions.lean b/LeanEval/Combinatorics/BalanceableBoundedPartitions.lean new file mode 100644 index 0000000..677ffc1 --- /dev/null +++ b/LeanEval/Combinatorics/BalanceableBoundedPartitions.lean @@ -0,0 +1,37 @@ +import Mathlib.Combinatorics.Enumerative.Partition.Basic +import Mathlib.Algebra.GCDMonoid.Finset +import EvalTools.Markers + +namespace LeanEval +namespace Combinatorics + +/-- +A partition is `k`-bounded if all of its members are 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 ≤ k + +/-- +A partition is balanceable if it can be decoposed into two multisets of +the same size. + +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₂.sum + +/-- +For any `k`, the smallest `n` such that any `k`-bounded partition of `n` is +also balanceable is given by `2 * lcm(1, ..., k)`. +-/ +@[eval_problem] +theorem 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) := by + sorry + +end Combinatorics +end LeanEval diff --git a/manifests/problems.toml b/manifests/problems.toml index d0d66c4..7b4f2ad 100644 --- a/manifests/problems.toml +++ b/manifests/problems.toml @@ -645,3 +645,12 @@ module = "LeanEval.NumberTheory.NeukirchUchida" holes = ["neukirch_uchida"] submitter = "Junyan Xu" source = "Jürgen Neukirch, Alexander Schmidt, Kay Wingberg. *Cohomology of Number Fields*, Theorem 12.2.1." + +[[problem]] +id = "balanceable_bounded_partitions" +title = "Balanceable k-bounded partitions" +test = false +module = "LeanEval.Combinatorics.BalanceableBoundedPartitions" +holes = ["minimal_balanceable_of_bounded"] +submitter = "Julia M. Himmel" +source = "https://projecteuler.net/problem=772" \ No newline at end of file