Rearrangements with distinct partial sums
TheoremValid orderings of finite sets of nonzero integers#●ready to prove
Every finite set \(A\) of nonzero integers has a valid ordering: its elements can be listed as \(a_1, \dots, a_m\), each exactly once, so that the partial sums \(a_1, a_1 + a_2, \dots, a_1 + \cdots + a_m\) are pairwise distinct. The empty sum \(0\) is not counted among the partial sums.
theorem_wanted exists_distinct_partial_sums_ordering
(A : Finset ℤ) (h0 : 0 ∉ A) :
∃ l : List ℤ, List.Perm l A.toList ∧
((l.scanl (· + ·) 0).tail).NodupSources
- Noah Kravitz, "Rearranging Small Sets for Distinct Partial Sums", Theorem 2.
TheoremLev's rectification principle#●ready to prove
Let \(\ell \ge 2\) be a natural number, \(p\) a prime and \(A\) a subset of \(\mathbb{Z}/p\mathbb{Z}\) with \(|A| \le \lceil \log p / \log \ell \rceil\). Then there are a finite set \(B\) of integers and a map \(f \colon \mathbb{Z}/p\mathbb{Z} \to \mathbb{Z}\) that is a Freiman isomorphism of order \(\ell\) from \(A\) to \(B\): \(f\) maps \(A\) bijectively onto \(B\), and for all \(a_1, \dots, a_\ell, b_1, \dots, b_\ell \in A\) we have \(f(a_1) + \cdots + f(a_\ell) = f(b_1) + \cdots + f(b_\ell)\) if and only if \(a_1 + \cdots + a_\ell = b_1 + \cdots + b_\ell\).
theorem_wanted exists_freimanIso_to_int (ℓ p : ℕ)
(hℓ : 2 ≤ ℓ) (hp : p.Prime) (A : Finset (ZMod p))
(hA : A.card ≤ ⌈Real.log p / Real.log ℓ⌉₊) :
∃ (B : Finset ℤ) (f : ZMod p → ℤ),
IsAddFreimanIso ℓ (A : Set (ZMod p)) (B : Set ℤ) fSources
- Noah Kravitz, "Rearranging Small Sets for Distinct Partial Sums", Theorem 3.
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.