Vela Mathematics Program: problems

Problem ledger

79 problems · 2/2Number SourcesGraph view

declared falsifiable · formalizederdos:1041

∀ (n : ℕ) (f : Polynomial ℂ), n ≥ 2 → f.natDegree = n → f.Monic → f.rootSet ℂ ⊆ Metric.ball 0 1 → ∃ z₁ z₂, ∃ (_ : {z₁, z₂} ≤ f.roots), ∃ γ, Set.range ⇑γ ⊆ {z | ‖Polynomial.eval z f‖ < 1} ∧ Erdos1041.length (Set.range ⇑γ) < 2

analysisN/A3 sources

declared provederdos:1042

Erdős problem 1042

analysisN/A

declared disproved (Lean) · formalizederdos:1043

False ↔ ∀ (f : Polynomial ℂ), f.Monic → f.degree ≥ 1 → ∃ u, ‖u‖ = 1 ∧ MeasureTheory.volume (⇑(ℝ ∙ u).orthogonalProjection '' Erdos1043.levelSet f) ≤ 2

analysisN/A5 sources

declared solved (Lean) · formalizederdos:1044

IsGLB {L | ∃ f, Erdos1044.IsAdmissible f ∧ Erdos1044.maxBoundaryLength f = L} 2

analysisN/A5 sources

declared openerdos:1045

Erdős problem 1045

analysisN/A

declared disprovederdos:1046

Erdős problem 1046

analysisN/A

declared disproved (Lean) · formalizederdos:1047

False ↔ ∀ (f : Polynomial ℂ) (m : ℕ) (c : ℝ), f.Monic → (f.rootSet ℂ).ncard = m → 0 < c → (Erdos1047.componentsIn (Erdos1047.sublevelSet f c)).ncard = m → ∀ t ∈ Erdos1047.componentsIn (Erdos1047.sublevelSet f c), Convex ℝ t

analysisN/A5 sources

declared disproved (Lean) · formalizederdos:1048

False ↔ ∀ (r : ℝ) (f : Polynomial ℂ), r < 2 → f.Monic → f.degree ≥ 1 → (∀ z ∈ f.roots, ‖z‖ ≤ r) → ∃ z ∈ Erdos1048.openLevelSet f, ENNReal.ofReal (2 - r) < Metric.ediam (connectedComponentIn (Erdos1048.openLevelSet f) z)

analysisN/A5 sources

declared provederdos:1114

Erdős problem 1114

analysispolynomialsN/A

declared solvederdos:1115

Erdős problem 1115

analysisN/A

declared solvederdos:1116

Erdős problem 1116

analysisN/A

declared openerdos:1117

Erdős problem 1117

analysisN/A

declared solvederdos:1118

Erdős problem 1118

analysisN/A

declared independent · formalizederdos:1119

True ↔ ∀ (m : Cardinal.{0}), Cardinal.aleph0 < m → m < Cardinal.continuum → ∀ (F : Set (ℂ → ℂ)), (∀ f ∈ F, Differentiable ℂ f) → (∀ (z₀ : ℂ), Cardinal.mk ↑{y | ∃ f ∈ F, f z₀ = y} ≤ m) → Cardinal.mk ↑F ≤ m

analysisset theoryN/A2 sources

declared openerdos:1120

Erdős problem 1120

analysisN/A

declared proved (Lean) · formalizederdos:1125

True ↔ ∀ (f : ℝ → ℝ), (∀ (x h : ℝ), h > 0 → 2 * f x ≤ f (x + h) + f (x + 2 * h)) → Monotone f

analysisN/A5 sources

declared proved (Lean) · formalizederdos:1126

True ↔ ∀ (f : ℝ → ℝ), (∀ᵐ (p : ℝ × ℝ) ∂MeasureTheory.volume.prod MeasureTheory.volume, f (p.1 + p.2) = f p.1 + f p.2) → ∃ h, (∀ (x y : ℝ), h (x + y) = h x + h y) ∧ ∀ᵐ (x : ℝ), f x = h x

analysisN/A5 sources

declared provederdos:1129

Erdős problem 1129

analysispolynomialsN/A2 sources

declared provederdos:1130

Erdős problem 1130

analysispolynomialsN/A2 sources

declared openerdos:1131

Erdős problem 1131

analysispolynomialsN/A2 sources

declared openerdos:1132

Erdős problem 1132

analysispolynomialsN/A2 sources

declared open · formalizederdos:1133

Must every sufficiently large node set admit bounded labels that force any polynomial fitting almost all labels at degree below

(1+\varepsilon)n

to have arbitrarily large uniform norm? Claimed via Beurling density for Bernstein spaces.

analysispolynomialsN/A4 sources

declared open · formalizederdos:1150

True ↔ ∃ c > 0, ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (P : Polynomial ℂ), (∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1) → P.natDegree = n → ⨆ z, ‖Polynomial.eval (↑z) P‖ > (1 + c) * √↑n

analysispolynomialsN/A2 sources

declared openerdos:1151

Let

\mathcal{L}^nf

be the Lagrange interpolation polynomials of a continuous

f

on the Chebyshev nodes. Prove that, for any closed

A\subseteq [-1,1]

, there exists a continuous function

f

such that

A

is the set of limit points of

\mathcal{L}^nf(x)

analysispolynomialsN/A3 sources

declared openerdos:1152

Erdős problem 1152

analysispolynomialsN/A

declared provederdos:1153

Erdős problem 1153

analysispolynomialsN/A3 sources

declared not disprovableerdos:1154

Erdős problem 1154

analysisN/A

declared disproved (Lean)erdos:1197

Erdős problem 1197

analysisN/A5 sources

declared disprovederdos:1215

Erdős problem 1215

analysisN/A

Problems · Vela Mathematics Program

Problem ledger

Search problems.science