Erdős Problem 495 to Erdős Problem 499

TheoremErdős Problem 495#

Reference: erdosproblems.com/495

Quoted from FormalConjectures/ErdosProblems/495.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The problem's page on erdosproblems.com: https://www.erdosproblems.com/495.

The file states 1 research or textbook statement: 1 open.

Erdos495.erdos_495

Open: stated without proof.

Let \(\alpha,\beta \in \mathbb{R}\). Is it true that

\[\liminf_{n\to \infty} n \| n\alpha \| \| n\beta\| =0\]

? This is also known as the Littlewood conjecture.

theorem erdos_495 : ∀ α β : ℝ, liminf (fun n : ℕ ↦ (n : ℝ) * distToNearestInt (n * α)
  * distToNearestInt (n * β)) atTop = 0

Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/495.lean, line 37.

Sources
LeanErdos495.erdos_495

TheoremErdős Problem 497#

References: - erdosproblems.com/497 - [Er61] Erdős, Paul, Some unsolved problems. Magyar Tud. Akad. Mat. Kutató Int. Közl. (1961), 221-254. - [Kl69] Kleitman, Daniel, On Dedekind's problem: The number of monotone Boolean functions. Proc. Amer. Math. Soc. (1969), 677-682.

Quoted from FormalConjectures/ErdosProblems/497.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The problem's page on erdosproblems.com: https://www.erdosproblems.com/497.

The file states 1 research or textbook statement: 1 solved.

Erdos497.erdos_497

Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/1d7b3f00780b85ed0462e79a1cd5650ee9055655/src/v4.29.1/ErdosProblems/Erdos497.lean.

How many antichains in \([n]\) are there? That is, how many families of subsets of \([n]\) are there such that, if \(\mathcal{F}\) is such a family and \(A,B\in \mathcal{F}\), then \(A\not\subseteq B\)?

Sperner's theorem states that \(\lvert \mathcal{F}\rvert \leq \binom{n}{\lfloor n/2\rfloor}\). This is also known as Dedekind's problem. Resolved by Kleitman [Kl69], who proved that the number of such families is

\[2^{(1+o(1))\binom{n}{\lfloor n/2\rfloor}}.\]
theorem erdos_497 :
    ∃ (o : ℕ → ℝ) (_ : o =o[atTop] (1 : ℕ → ℝ)),
      ∀ n : ℕ, (DedekindNumber.M' n : ℝ) = 2 ^ ((1 + o n) * (n.choose (n / 2) : ℝ))

Category research solved; AMS 05 Combinatorics, 06 Order, lattices, ordered algebraic structures. Declared in FormalConjectures/ErdosProblems/497.lean, line 50.

Sources
LeanErdos497.erdos_497

TheoremErdős Problem 498#

References: - erdosproblems.com/498 - [Er61] Erdős, Paul, Some unsolved problems. Magyar Tud. Akad. Mat. Kutató Int. Közl. (1961), 221-254. - [Er45] Erdős, P., On a lemma of Littlewood and Offord. Bull. Amer. Math. Soc. (1945), 898-902. - [Kl65] Kleitman, Daniel J., On a lemma of Littlewood and Offord on the distribution of certain sums. Math. Z. (1965), 251-259. - [Kl70] Kleitman, Daniel J., On a lemma of Littlewood and Offord on the distributions of linear combinations of vectors. Advances in Math. (1970), 155-157.

Quoted from FormalConjectures/ErdosProblems/498.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The problem's page on erdosproblems.com: https://www.erdosproblems.com/498.

The file states 1 research or textbook statement: 1 solved.

Erdos498.erdos_498

Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/1268917deaaaa0d674f651287027baa26cea9920/src/latest/ErdosProblems/Erdos498.lean#L2006.

Let \(z_1,\ldots,z_n\in\mathbb{C}\) with \(1\leq \lvert z_i\rvert\) for \(1\leq i\leq n\). Let \(D\) be an arbitrary disc of radius \(1\). Is it true that the number of sums of the shape

\[\sum_{i=1}^n\epsilon_iz_i \textrm{ for }\epsilon_i\in \{-1,1\}\]

which lie in \(D\) is at most \(\binom{n}{\lfloor n/2\rfloor}\)?

A strong form of the Littlewood-Offord problem. Erdős [Er45] proved this is true if \(z_i\in\mathbb{R}\), and for general \(z_i\in\mathbb{C}\) proved a weaker upper bound of

\[\ll \frac{2^n}{\sqrt{n}}.\]

This was solved in the affirmative by Kleitman [Kl65], who also later generalised this to arbitrary Hilbert spaces [Kl70].

See also [395].

theorem erdos_498 :
    ∀ (n : ℕ) (z : Fin n → ℂ), (∀ i, 1 ≤ ‖z i‖) → ∀ c : ℂ,
      {ε : Fin n → ℤ | (∀ i, ε i = -1 ∨ ε i = 1) ∧
        (∑ i, (ε i : ℂ) * z i) ∈ Metric.ball c 1}.ncard ≤ n.choose (n / 2)

Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/498.lean, line 54.

Sources
LeanErdos498.erdos_498

LemmaErdős Problem 499#

Reference: erdosproblems.com/499

Quoted from FormalConjectures/ErdosProblems/499.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The problem's page on erdosproblems.com: https://www.erdosproblems.com/499.

The file states 3 research or textbook statements: 3 solved.

Erdos499.erdos_499

Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/main/src/v4.29.1/ErdosProblems/Erdos499.lean.

Let \(M\) be a real \(n \times n\) doubly stochastic matrix. Does there exist some \(σ \in S_n\) such that

\[ \prod_{1 \leq i \leq n} M_{i, σ(i)} \geq n^{-n}? \]

This is true, and was proved by Marcus and Minc [MaMi62]

[MaMi62] Marcus, Marvin and Minc, Henryk, Some results on doubly stochastic matrices. Proc. Amer. Math. Soc. (1962), 571-579.

lemma erdos_499 :
    (∀ n, ∀ M ∈ doublyStochastic ℝ (Fin n), ∃ σ : Equiv.Perm (Fin n),
      n ^ (- n : ℤ) ≤ ∏ i, M i (σ i))

Category research solved; AMS 15 Linear and multilinear algebra; matrix theory. Declared in FormalConjectures/ErdosProblems/499.lean, line 42.

Erdos499.vanDerWaerden

Solved: stated here without proof.

The conjecture of van der Waerden, which states that the permanent of a doubly stochastic matrix is at least \(n^{-n} n!\).

Proved by Gyires [Gy80], Egorychev [Eg81], and Falikman [Fa81].

[Gy80] Gyires, B., The common source of several inequalities concerning doubly stochastic matrices. Publ. Math. Debrecen (1980), 291-304. [Eg81] Egorychev, G. P., The solution of the van der Waerden problem for permanents. Dokl. Akad. Nauk SSSR (1981), 1041-1044. [Fa81] Falikman, D. I., Proof of the van der Waerden conjecture on the permanent of a doubly stochastic matrix. Mat. Zametki (1981), 931-938, 957.

lemma vanDerWaerden (n : ℕ) (M : Matrix (Fin n) (Fin n) ℝ) (hM : M ∈ doublyStochastic ℝ (Fin n)) :
    n ^ (- n : ℤ) * n ! ≤ M.permanent

Category research solved; AMS 15 Linear and multilinear algebra; matrix theory. Declared in FormalConjectures/ErdosProblems/499.lean, line 58.

Erdos499.erdos_499.variants.one_le

Solved: stated here without proof.

A weaker version of Erdős' problem 499, which asks whether for every doubly stochastic matrix, there exists a permutation \(σ \in S_n\) with \(M_{i, σ(i)} ≠ 0\) and such that

\[ \sum_{1 \leq i \leq n} M_{i, σ(i)} \geq 1 \]

Proved by Marcus and Ree [MaRe59].

[MaRe59] Marcus, M. and Ree, R., Diagonals of doubly stochastic matrices. Quart. J. Math. Oxford Ser. (2) (1959), 296-302.

lemma erdos_499.variants.one_le :
    ∀ n > 0, ∀ M ∈ doublyStochastic ℝ (Fin n), ∃ σ : Equiv.Perm (Fin n),
      (∀ i, M i (σ i) ≠ 0) ∧ 1 ≤ ∑ i, M i (σ i)

Category research solved; AMS 15 Linear and multilinear algebra; matrix theory. Declared in FormalConjectures/ErdosProblems/499.lean, line 73.

Sources
LeanErdos499.erdos_499 · Erdos499.vanDerWaerden · Erdos499.erdos_499.variants.one_le

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.