Erdős problem 319 · problems.science

What is the size of the largest $A\subseteq\{1, \dots, N\}$ such that there is a function $\delta : A \to \{-1, 1\}$ such that $\sum_{n\in A} \frac{\delta n}{n} = 0$ and $\sum_{n\in A'}\frac{\delta n}{n} \neq 0$ for all non-empty $A'\subsetneq A$ .

Sources

Browse retained paths and inspect the exact material available for this Problem.

5 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

319.lean

Retained formal statement3 of 5

Let c(N) be the size of the largest $A\subseteq\{1, \dots, N\}$ such that there is a function $\delta$ : $A \to$ \{-1, 1\} such that $\sum_{n\in A} \frac{\delta n}{n} = 0$ and $\sum_{n\in A'}\frac{\delta n}{n} \neq 0$ for all non-empty $A'\subsetneq A$ . Find the simplest g(N) such that c(N) = o(g(N)).

FormalConjectures/ErdosProblems/319.leanErdos319.erdos_319.variants.isLittleO9 linesExact file

1∀ (N : ℕ) (c : ℕ → ℝ),2  (∀ (N : ℕ),3      IsGreatest4        {x |5          ∃ A,6            ∃ (_ : A ⊆ Finset.Icc 1 N) (_ :7              ∃ δ, ∑ n ∈ A, ↑↑(δ n) / ↑n = 0 ∧ ∀ A' ⊂ A, A'.Nonempty → ∑ n ∈ A', ↑↑(δ n) / ↑n ≠ 0), ↑A.card = x}8        (c N)) →9    c =o[Filter.atTop] sorry

OpenStatement only, no proof

Sources

Search problems.science