Skip to content

Problems · Vela Mathematics Program

Narrowed toopen ×sidon sets ×Clear all

Problem ledger

20 problemsGraph view
declared open · formalizederdos:14
True ↔ ∀ (A : Set ℕ), ∀ ε > 0, Erdos14.almostSquareRoot ε =O[Filter.atTop] Erdos14.nonUniqueSumCount A
number theorysidon setsadditive combinatoricsA143824 · possible2 sources
declared open · formalized · $1000erdos:30
True ↔ ∀ ε > 0, (fun N => ↑(Erdos30.h N) - √↑N) =O[Filter.atTop] fun N => ↑N ^ ε
number theorysidon setsadditive combinatoricsA143824 · A227590 · A0030222 sources
declared open · formalized · $500erdos:39
True ↔ ∃ A, A.Infinite ∧ IsSidon A ∧ ∀ ε > 0, (fun x => ↑x ^ (1 / 2 - ε)) =O[Filter.atTop] fun N => ↑(Set.Icc 1 N ∩ A).ncard
number theorysidon setsadditive combinatoricsN/A2 sources
declared open · formalized · $500erdos:41
∀ (A : Set ℕ), Erdos41.NtupleCondition A 3 → A.Infinite → Filter.liminf (fun N => ↑(A ∩ Set.Icc 1 N).ncard / ↑N ^ (1 / 3)) Filter.atTop = 0
number theorysidon setsadditive combinatoricsN/A2 sources
declared open · formalizederdos:44
True ↔ ∀ N ≥ 1, ∀ A ⊆ Finset.Icc 1 N, IsSidon ↑A → ∀ ε > 0, ∃ M > N, ∃ B ⊆ Finset.Icc (N + 1) M, IsSidon (↑A ∪ ↑B) ∧ (1 - ε) * √↑M ≤ ↑(A ∪ B).card
number theorysidon setsadditive combinatoricsN/A2 sources
declared open · formalizederdos:153
True ↔ Filter.Tendsto Erdos153.f Filter.atTop Filter.atTop
sidon setsN/A2 sources
declared open · formalizederdos:155
True ↔ ∀ k ≥ 1, ∀ᶠ (N : ℕ) in Filter.atTop, Erdos155.F (N + k) ≤ Erdos155.F N + 1
additive combinatoricssidon setsA143824 · A227590 · A0030222 sources
declared open · formalizederdos:156
True ↔ (fun N => ↑(Erdos156.minMaximalSidonSet N)) =O[Filter.atTop] fun N => ↑N ^ (1 / 3)
sidon setsA3823972 sources
declared open · formalizederdos:158
∀ {A : Set ℕ}, Erdos158.B2 1 A ↔ IsSidon A
sidon setsN/A2 sources
declared open · formalized · $100erdos:241
True ↔ Asymptotics.IsEquivalent Filter.atTop (fun N => ↑(Erdos241.f N 3)) fun N => ↑N ^ (1 / 3)
additive combinatoricssidon setsA3877042 sources
declared open · formalizederdos:340
∀ ε > 0, (fun n => √↑n / ↑n ^ ε) =O[Filter.atTop] fun n => ↑(Set.range Finset.greedySidon ∩ Set.Icc 1 n).ncard
number theoryadditive combinatoricssidon setsA080200 · A0052822 sources
declared openerdos:425
Erdős problem 425
number theorysidon setspossible2 sources
declared openerdos:530
Erdős problem 530
number theorysidon setsA143824 · possible
declared open · formalizederdos:757
∀ {A : Set ℝ}, sorry = sSup {c | Erdos757.IsAdmissible c}
geometrydistancessidon setspossible2 sources
declared openerdos:773
Erdős problem 773
number theorysidon setssquaresA390813
declared openerdos:840
Erdős problem 840
additive combinatoricssidon setsN/A
declared openerdos:864
Erdős problem 864
number theorysidon setsadditive combinatoricsA3891822 sources
declared open · $1000erdos:1191
Erdős problem 1191
additive combinatoricssidon setspossible
declared openerdos:1194
Erdős problem 1194
additive combinatoricsadditive basissidon setspossible2 sources
declared openerdos:1206
Erdős problem 1206
number theorysidon setspossible

Search problems.science

Find a Problem, Result, source, or page