Erdős problem 498
Let with for . Let be an arbitrary disc of radius . Is it true that the number of sums of the shape which lie in is at most ?
No current result
No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.
Retained declaration
FormalConjectures/ErdosProblems/498.leanTrue ↔ ∀ (n : ℕ) (z : Fin n → ℂ), (∀ (i : Fin n), 1 ≤ ‖z i‖) → ∀ (c : ℂ), {ε | (∀ (i : Fin n), ε i = -1 ∨ ε i = 1) ∧ ∑ i, ↑(ε i) * z i ∈ Metric.ball c 1}.ncard ≤ n.choose (n / 2)SolvedStatement only, no proof
Proof manifests naming this Problem
- Jayyhk Erdős Lean
jayyhk:erdos:498 - PLBY Lean proofs
ErdosProblems.Erdos498
Reported activity
Work these sources record against this Problem. Source-reported attribution, not reviewed here.
Formalization
- Machine