Vela Mathematics Program: problems

Narrowed toformalized ×analysis ×Clear all

Problem ledger

declared proved (Lean) · formalizederdos:115

True ↔ ∀ ε > 0, ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (p : Polynomial ℂ), p.Monic → p.natDegree = n → IsConnected {z | ‖Polynomial.eval z p‖ ≤ 1} → ∀ (z : ℂ), ‖Polynomial.eval z p‖ ≤ 1 → ‖Polynomial.eval z (Polynomial.derivative p)‖ ≤ (1 / 2 + ε) * ↑n ^ 2

polynomialsanalysisN/A5 sources

declared solved · formalized · $100erdos:119

For unit-modulus complex numbers

z_i

, let

p_n(z)=\prod_{i\le n}(z-z_i)

and

M_n=\max_{|z|=1}|p_n(z)|

. Erdős's prize question: is there

c>0

with

\sum_{k\le n} M_k > n^{1+c}

analysispolynomialsN/A4 sources

declared proved (Lean) · formalizederdos:226

True ↔ ∃ F, Differentiable ℂ F ∧ (∀ (x : ℝ), (F ↑x).im = 0) ∧ (∀ (g : ℝ →ᵃ[ℝ] ℝ), (fun x => (F ↑x).re) ≠ ⇑g) ∧ Erdos226.PreservesRationality fun x => (F ↑x).re

analysisN/A5 sources

declared proved · formalizederdos:228

True ↔ ∃ c₁ c₂, ∀ᶠ (n : ℕ) in Filter.atTop, ∃ p, p.degree = ↑n ∧ (∀ i ≤ n, p.coeff i = 1 ∨ p.coeff i = -1) ∧ ∀ (z : ℂ), ‖z‖ = 1 → √↑n < c₁ * ‖Polynomial.eval z p‖ ∧ ‖Polynomial.eval z p‖ < c₂ * √↑n

analysispolynomialsN/A2 sources

declared proved (Lean) · formalizederdos:229

True ↔ ∀ (S : ℕ → Set ℂ), (∀ (n : ℕ), derivedSet (S n) = ∅) → ∃ f, Transcendental (Polynomial ℂ) f ∧ Differentiable ℂ f ∧ ∀ n ≥ 1, ∃ k, ∀ z ∈ S n, iteratedDeriv k f z = 0

analysisiterated functionsN/A5 sources

declared proved · formalizederdos:494

∀ (k card p : ℕ), Nat.Prime p → k ∈ Set.Ioo 0 p → p ∣ card → Erdos494.Erdos494Unique k card

analysisadditive combinatoricsN/A2 sources

declared proved (Lean) · formalizederdos:498

True ↔ ∀ (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)

combinatoricsanalysisN/A5 sources

declared open · formalizederdos:509

∀ {M : Type u} [inst : MetricSpace M] (S : Set M), S.Nonempty → ∀ (r : ℝ) (ι : Type v) (bdc : Erdos509.BoundedDiscCover S r ι), 0 < r

analysisN/A2 sources

declared open · formalizederdos:510

sorry ↔ ∃ c, ∃ (_ : 0 < c), ∀ᶠ (N : ℕ) in Filter.atTop, ∀ (A : Finset ℕ), 0 ∉ A → A.card = N → ∃ θ, ∑ n ∈ A, Real.cos (↑n * θ) < -c * √↑N

analysisN/A2 sources

declared proved (Lean) · formalizederdos:512

True ↔ ∃ c > 0, ∀ (N : ℕ) (A : Finset ℤ), A.card = N → c * Real.log ↑N ≤ ∫ (θ : ℝ) in 0..1, ‖∑ n ∈ A, additiveChar (↑n * θ)‖

analysisN/A4 sources

declared open · formalizederdos:513

sorry = ⨆ f, Filter.liminf (fun r => Erdos513.ratio r ↑f) Filter.atTop

analysisN/A3 sources

declared proved · formalizederdos:516

∀ {f : ℂ → ℂ} {n : ℕ → ℕ}, HasFabryGaps n → ∀ {a : ℕ → ℂ}, (∀ (n : ℕ), a n ≠ 0) → (∀ (z : ℂ), HasSum (fun k => a k * z ^ n k) (f z)) → Erdos516.OfFiniteOrder f → Filter.limsup (fun r => Erdos516.ratio r f) Filter.atTop = 1

analysisN/A2 sources

declared open · formalizederdos:517

sorry ↔ ∀ {f : ℂ → ℂ} {n : ℕ → ℕ}, HasFabryGaps n → ∀ {a : ℕ → ℂ}, (∀ (k : ℕ), a k ≠ 0) → (∀ (z : ℂ), HasSum (fun k => a k * z ^ n k) (f z)) → ∀ (z : ℂ), {x | f x = z}.Infinite

analysisN/A3 sources

declared proved (Lean) · formalizederdos:519

True ↔ ∃ c, 0 < c ∧ ∀ (n : ℕ) (hn : 0 < n) (z : Fin n → ℂ), z ⟨0, hn⟩ = 1 → ∃ k, c < ‖Erdos519.powerSum z (↑k + 1)‖

analysisN/A5 sources

declared open · formalizederdos:521

False ↔ Erdos521.Claim

analysispolynomialsprobabilityN/A4 sources

declared open · formalizederdos:522

For

P_n(z) = \sum_{k=0}^n \varepsilon_k z^k

with independent uniform signs, does the number

R_n

of roots in

|z| \le 1

satisfy

R_n/(n/2) \to 1

almost surely? The manuscript proves the strong law with

R_n = n/2 + O_\omega(n^{149/150})

analysispolynomialsprobabilityN/A4 sources

declared open · formalizederdos:906

Is there an entire non-zero function

f:\mathbb{C}\to \mathbb{C}

such that, for any infinite sequence

n_1<n_2<\cdots

, the set

\{ z: f^{(n_k)}(z)=0 \textrm{ for some }k\geq 1\}

is everywhere dense? The literal question is trivial for polynomials, so the claims address the transcendental entire case, in the affirmative.

analysisiterated functionsN/A5 sources

declared proved (Lean) · formalizederdos:907

True ↔ ∀ (f : ℝ → ℝ), (∀ (h : ℝ), 0 < h → Continuous fun x => f (x + h) - f x) → ∃ g a, Continuous g ∧ (∀ (x y : ℝ), a (x + y) = a x + a y) ∧ f = g + a

analysisN/A5 sources

declared disproved (Lean) · formalizederdos:967

False ↔ ∀ (a : ℕ → ℕ), StrictMono a → 1 < a 0 → (Summable fun k => 1 / ↑(a k)) → ∀ (t : ℝ), 1 + ∑' (k : ℕ), Erdos967.summand t (a k) ≠ 0

number theoryanalysisN/A5 sources

declared open · formalizederdos:973

True ↔ ∃ C > 1, ∀ n ≥ 2, ∃ z, z 1 = 1 ∧ (∀ i ∈ Finset.Icc 1 n, 1 ≤ ‖z i‖) ∧ ∀ k ∈ Finset.Icc 2 (n + 1), ‖∑ i ∈ Finset.Icc 1 n, z i ^ k‖ < C ^ (-↑n)

analysisN/A2 sources

declared proved (Lean) · formalizederdos:974

∀ {n : ℕ} [inst : NeZero n] (z : Fin n → ℂ), z 0 = 1 → {k | ∀ j < n - 1, ∑ i, z i ^ (k + j) = 0}.Infinite → Erdos974.IsTuranConfiguration z

analysisN/A5 sources

declared proved · formalizederdos:987

True ↔ ∀ (x : ℕ → ℝ), (∀ (j : ℕ), x j ∈ Set.Ioo 0 1) → Filter.limsup (fun k => Erdos987.A x k) Filter.atTop = ⊤

analysisdiscrepancyN/A4 sources

declared disproved (Lean) · formalizederdos:990

False ↔ ∃ C, ∀ (f : Polynomial ℂ), f.coeff 0 ≠ 0 → ∀ (α β : ℝ), 0 ≤ α → α ≤ β → β ≤ 2 * Real.pi → |↑(Erdos990.rootArgCount f (Set.Icc α β)) - (β - α) / (2 * Real.pi) * ↑f.natDegree| ≤ C * √(↑f.support.card * Real.log (Erdos990.M f))

analysisN/A6 sources

declared open · formalizederdos:996

Let

n_1<n_2<\cdots

be a lacunary sequence of integers and

f\in L^2([0,1])

with

n

th Fourier partial sum

f_n

. Is there an absolute constant

C>0

such that if

\| f-f_n\|_2 \ll (\log\log\log n)^{-C}

then

\frac{1}{N}\sum_{k\leq N}f(\{\alpha n_k\})\to\int_0^1 f

for almost every

\alpha

? A preprint answers this negatively via a dyadic spike-block counterexample.

analysisN/A4 sources

declared proved (Lean) · formalizederdos:997

True ↔ ∀ (α : ℝ), ¬Erdos997.IsWellDistributed fun n => Int.fract (α * ↑(Nat.nth Nat.Prime n))

analysisdiscrepancyprimesN/A6 sources

declared open · formalizederdos:1002

sorry ↔ ∃ g, Monotone g ∧ Filter.Tendsto g Filter.atBot (nhds 0) ∧ Filter.Tendsto g Filter.atTop (nhds 1) ∧ ∀ (c : ℝ), Filter.Tendsto (fun n => (MeasureTheory.volume {α | α ∈ Set.Ioo 0 1 ∧ (fun α n => 1 / Real.log ↑n * ∑ k ∈ Finset.Icc 1 n, (1 / 2 - Int.fract (α * ↑k))) α n ≤ c}).toReal) Filter.atTop (nhds (g c))

analysisdiophantine approximationN/A2 sources

declared open · formalizederdos:1038

Among all nonconstant monic polynomials

f

whose roots lie in

[-1, 1]

, determine

\inf_f |\{x \in \mathbb{R} : |f(x)| < 1\}|

analysisN/A4 sources

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 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 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 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 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 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

Problems · Vela Mathematics Program

Problem ledger