From 6c37506b66c1ec0b259f42b4ca32826d9628cbf8 Mon Sep 17 00:00:00 2001 From: Ryan Tuck Date: Tue, 17 Mar 2026 15:29:10 +0000 Subject: [PATCH] feat(ErdosProblems): 6x probability-related formalizations --- FormalConjectures/ErdosProblems/1144.lean | 80 +++++++++++ FormalConjectures/ErdosProblems/1155.lean | 108 +++++++++++++++ FormalConjectures/ErdosProblems/1156.lean | 99 ++++++++++++++ FormalConjectures/ErdosProblems/521.lean | 154 ++++++++++++++++++++++ FormalConjectures/ErdosProblems/524.lean | 105 +++++++++++++++ FormalConjectures/ErdosProblems/529.lean | 110 ++++++++++++++++ 6 files changed, 656 insertions(+) create mode 100644 FormalConjectures/ErdosProblems/1144.lean create mode 100644 FormalConjectures/ErdosProblems/1155.lean create mode 100644 FormalConjectures/ErdosProblems/1156.lean create mode 100644 FormalConjectures/ErdosProblems/521.lean create mode 100644 FormalConjectures/ErdosProblems/524.lean create mode 100644 FormalConjectures/ErdosProblems/529.lean diff --git a/FormalConjectures/ErdosProblems/1144.lean b/FormalConjectures/ErdosProblems/1144.lean new file mode 100644 index 000000000..96a626a31 --- /dev/null +++ b/FormalConjectures/ErdosProblems/1144.lean @@ -0,0 +1,80 @@ +/- +Copyright 2026 The Formal Conjectures Authors. + +Licensed under the Apache License, Version 2.0 (the "License"); +you may not use this file except in compliance with the License. +You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + +Unless required by applicable law or agreed to in writing, software +distributed under the License is distributed on an "AS IS" BASIS, +WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +See the License for the specific language governing permissions and +limitations under the License. +-/ + +import FormalConjectures.Util.ProblemImports + +/-! +# Erdős Problem 1144 + +Let $f$ be a random completely multiplicative function, where for each prime $p$ we independently +choose $f(p) \in \{-1, 1\}$ uniformly at random. Is it true that the limsup of +$\sum_{m \leq N} f(m) / \sqrt{N}$ is infinite with probability 1? + +*Reference:* [erdosproblems.com/1144](https://www.erdosproblems.com/1144) + +[Va99] Montgomery, H.L. and Vaughan, R.C., *Multiplicative Number Theory I: Classical Theory*. +Cambridge Studies in Advanced Mathematics, Cambridge University Press, 2007. + +[At25] Atherfold, C., *Almost sure bounds for weighted sums of Rademacher random multiplicative +functions*. arXiv:2501.11076, 2025. +-/ + +open MeasureTheory ProbabilityTheory Filter Finset BigOperators + +namespace Erdos1144 + +/-- A random variable is Rademacher distributed: takes values $\pm 1$ with equal probability. -/ +def IsRademacher {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω) (X : Ω → ℝ) : Prop := + (∀ ω, X ω = 1 ∨ X ω = -1) ∧ + μ {ω | X ω = 1} = μ {ω | X ω = -1} + +/-- The random *completely* multiplicative function built from Rademacher signs at primes. +For $n \geq 1$: $f(n) = \prod_{p \in \operatorname{primeFactors}(n)} \varepsilon(p)^{v_p(n)}$. +For $n = 0$: $f(0) = 0$. +This is completely multiplicative (as opposed to merely multiplicative, cf. Problem 520). -/ +noncomputable def randMultFun {Ω : Type*} (ε : ℕ → Ω → ℝ) (ω : Ω) (n : ℕ) : ℝ := + if n = 0 then 0 + else ∏ p ∈ n.factorization.support, (ε p ω) ^ (n.factorization p) + +/-- The partial sum $\sum_{m=1}^{N} f(m)$. -/ +noncomputable def partialSum {Ω : Type*} (ε : ℕ → Ω → ℝ) (ω : Ω) (N : ℕ) : ℝ := + ∑ m ∈ Finset.Icc 1 N, randMultFun ε ω m + +/-- +Erdős Problem 1144 [Va99, 1.11]: + +Let $f$ be a random completely multiplicative function, where for each prime $p$ +we independently choose $f(p) \in \{-1, 1\}$ uniformly at random. Is it true that +$$\limsup_{N \to \infty} \frac{\sum_{m \leq N} f(m)}{\sqrt{N}} = \infty$$ +with probability 1? + +This model is sometimes called a Rademacher random multiplicative function. +Atherfold [At25] proved that, almost surely, +$$\sum_{m \leq N} f(m) \ll N^{1/2} (\log N)^{1+o(1)}.$$ +-/ +@[category research open, AMS 11 60] +theorem erdos_1144 : + answer(sorry) ↔ + ∀ (Ω : Type*) [MeasurableSpace Ω] (μ : Measure Ω) [IsProbabilityMeasure μ] + (ε : ℕ → Ω → ℝ), + (∀ k, IsRademacher μ (ε k)) → + iIndepFun ε μ → + (∀ᵐ ω ∂μ, ∀ C : ℝ, + ∃ᶠ N in atTop, + partialSum ε ω N > C * Real.sqrt (N : ℝ)) := by + sorry + +end Erdos1144 diff --git a/FormalConjectures/ErdosProblems/1155.lean b/FormalConjectures/ErdosProblems/1155.lean new file mode 100644 index 000000000..2ee83aeb5 --- /dev/null +++ b/FormalConjectures/ErdosProblems/1155.lean @@ -0,0 +1,108 @@ +/- +Copyright 2026 The Formal Conjectures Authors. + +Licensed under the Apache License, Version 2.0 (the "License"); +you may not use this file except in compliance with the License. +You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + +Unless required by applicable law or agreed to in writing, software +distributed under the License is distributed on an "AS IS" BASIS, +WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +See the License for the specific language governing permissions and +limitations under the License. +-/ + +import FormalConjectures.Util.ProblemImports + +/-! +# Erdős Problem 1155 + +*Reference:* [erdosproblems.com/1155](https://www.erdosproblems.com/1155) + +Construct a random graph on $n$ vertices in the following way: begin with the complete graph +$K_n$. At each stage, choose uniformly a random triangle in the graph and delete all the edges +of this triangle. Repeat until the graph is triangle-free. If $f(n)$ is the number of edges +remaining, is it true that $\mathbb{E}[f(n)] \asymp n^{3/2}$ and that $f(n) \ll n^{3/2}$ +almost surely? + +A problem of Bollobás and Erdős [Bo98, p.231][Va99, 3.61]. + +Bohman, Frieze, and Lubetzky [BFL15] proved that $f(n) = n^{3/2 + o(1)}$ a.s. + +[Bo98] Bollobás, B., _Modern Graph Theory_, Graduate Texts in Mathematics 184, Springer (1998). + +[Va99] Vu, V. H. (1999), 3.61. + +[Gr97] Grable, D. A., _On random greedy triangle packing_, Electronic Journal of +Combinatorics 4 (1997), Research Paper 11. + +[BFL15] Bohman, T., Frieze, A., and Lubetzky, E., _Random triangle removal_, +Advances in Mathematics 280 (2015), 379--438. +-/ + +open SimpleGraph Filter + +open scoped Topology + +namespace Erdos1155 + +/-- The triangle removal process on $K_n$: starting from the complete graph on $n$ + vertices, repeatedly choose a uniformly random triangle and remove all three + of its edges, until the graph is triangle-free. + + `triangleRemovalExpectedEdges n` is $\mathbb{E}[f(n)]$, the expected number of edges + remaining when the process terminates. -/ +opaque triangleRemovalExpectedEdges (n : ℕ) : ℝ + +/-- The probability that the number of edges remaining after the triangle + removal process on $K_n$ satisfies a given predicate $P$. -/ +opaque triangleRemovalEdgeProb (n : ℕ) (P : ℕ → Prop) : ℝ + +/-- +Erdős Problem #1155, Part 1 [Bo98, p.231]: + +$\mathbb{E}[f(n)] \asymp n^{3/2}$, i.e., there exist constants $c_1, c_2 > 0$ such that for all +sufficiently large $n$, $c_1 \cdot n^{3/2} \leq \mathbb{E}[f(n)] \leq c_2 \cdot n^{3/2}$. +-/ +@[category research open, AMS 5 60] +theorem erdos_1155 : answer(sorry) ↔ + ∃ c₁ c₂ : ℝ, 0 < c₁ ∧ 0 < c₂ ∧ + ∃ N₀ : ℕ, ∀ n : ℕ, n ≥ N₀ → + c₁ * (n : ℝ) ^ ((3 : ℝ) / 2) ≤ triangleRemovalExpectedEdges n ∧ + triangleRemovalExpectedEdges n ≤ c₂ * (n : ℝ) ^ ((3 : ℝ) / 2) := by + sorry + +/-- +Erdős Problem #1155, Part 2 [Bo98, p.231]: + +$f(n) \ll n^{3/2}$ almost surely, i.e., there exists $C > 0$ such that with +probability tending to $1$, $f(n) \leq C \cdot n^{3/2}$. +-/ +@[category research open, AMS 5 60] +theorem erdos_1155.variants.almost_sure : answer(sorry) ↔ + ∃ C : ℝ, 0 < C ∧ + Tendsto (fun n : ℕ => + triangleRemovalEdgeProb n (fun k => (k : ℝ) ≤ C * (n : ℝ) ^ ((3 : ℝ) / 2))) + atTop (nhds 1) := by + sorry + +/-- +Erdős Problem #1155, Variant (Bohman–Frieze–Lubetzky [BFL15]): + +$f(n) = n^{3/2 + o(1)}$ almost surely, i.e., for every $\varepsilon > 0$, the probability that +$n^{3/2 - \varepsilon} \leq f(n) \leq n^{3/2 + \varepsilon}$ tends to $1$ as $n \to \infty$. +This strengthens Part 2 by providing a matching almost-sure lower bound. +-/ +@[category research solved, AMS 5 60] +theorem erdos_1155.variants.bfl15 : answer(sorry) ↔ + ∀ ε : ℝ, 0 < ε → + Tendsto (fun n : ℕ => + triangleRemovalEdgeProb n (fun k => + (n : ℝ) ^ ((3 : ℝ) / 2 - ε) ≤ (k : ℝ) ∧ + (k : ℝ) ≤ (n : ℝ) ^ ((3 : ℝ) / 2 + ε))) + atTop (nhds 1) := by + sorry + +end Erdos1155 diff --git a/FormalConjectures/ErdosProblems/1156.lean b/FormalConjectures/ErdosProblems/1156.lean new file mode 100644 index 000000000..1a8a468e6 --- /dev/null +++ b/FormalConjectures/ErdosProblems/1156.lean @@ -0,0 +1,99 @@ +/- +Copyright 2026 The Formal Conjectures Authors. + +Licensed under the Apache License, Version 2.0 (the "License"); +you may not use this file except in compliance with the License. +You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + +Unless required by applicable law or agreed to in writing, software +distributed under the License is distributed on an "AS IS" BASIS, +WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +See the License for the specific language governing permissions and +limitations under the License. +-/ + +import FormalConjectures.Util.ProblemImports + +/-! +# Erdős Problem 1156 + +*Reference:* [erdosproblems.com/1156](https://www.erdosproblems.com/1156) + +Let $G$ be a random graph on $n$ vertices, in which every edge is included +independently with probability $1/2$ (the Erdős–Rényi model $G(n, 1/2)$). + +Bollobás [Bo88] proved that $\chi(G) \sim n / (2 \log_2 n)$ with high probability. +Shamir and Spencer [ShSp87] proved concentration within $o(\sqrt{n})$. +Heckel and Riordan [HeRi23] proved concentration cannot be within $n^c$ for $c < 1/2$. + +[AlSp92] Alon, N. and Spencer, J., _The Probabilistic Method_, Wiley, 1992. + +[AlSp16] Alon, N. and Spencer, J. H., _The Probabilistic Method_, 4th ed., Wiley, 2016. + +[Bo88] Bollobás, B., _The chromatic number of random graphs_. Combinatorica (1988), 49–55. + +[He21] Heckel, A., _Non-concentration of the chromatic number of a random graph_. +J. Amer. Math. Soc. (2021), 245–260. + +[HeRi23] Heckel, A. and Riordan, O., _How does the chromatic number of a random graph vary?_ +J. Lond. Math. Soc. (2) (2023), 1769–1815. + +[Sc17] Scott, A., _On the concentration of the chromatic number of random graphs_. +arXiv:0806.0178 (2017). + +[ShSp87] Shamir, E. and Spencer, J., _Sharp concentration of the chromatic number on random +graphs $G_{n,p}$_. Combinatorica (1987), 121–129. + +[Va99] Vu, V. H. (1999), 3.64. +-/ + +open Filter + +open scoped Topology + +namespace Erdos1156 + +/-- The probability that the chromatic number of a uniformly random graph +$G(n, 1/2)$ on $n$ vertices satisfies predicate $P$. Here $G(n, 1/2)$ is the +Erdős–Rényi model where each edge is included independently with +probability $1/2$, equivalently the uniform distribution over all simple +graphs on $n$ labelled vertices. -/ +opaque chromaticNumberProb (n : ℕ) (P : ℕ → Prop) : ℝ + +/-- +Erdős Problem 1156, Part 1 [AlSp92]: + +There exists a constant $C$ such that $\chi(G(n, 1/2))$ is almost surely concentrated +on at most $C$ values. That is, for every $\varepsilon > 0$ and all sufficiently large $n$, +there is a set $S$ of at most $C$ natural numbers with +$\mathbb{P}(\chi(G) \in S) \geq 1 - \varepsilon$. +-/ +@[category research open, AMS 5 60] +theorem erdos_1156 : + ∃ C : ℕ, ∀ ε : ℝ, 0 < ε → + ∀ᶠ n in atTop, + ∃ S : Finset ℕ, S.card ≤ C ∧ + chromaticNumberProb n (· ∈ S) ≥ 1 - ε := by + sorry + +/-- +Erdős Problem 1156, Part 2 [AlSp92] [Va99]: + +There exists a function $\omega : \mathbb{N} \to \mathbb{R}$ with $\omega(n) \to \infty$ such that +for every function $f : \mathbb{N} \to \mathbb{R}$, for all sufficiently large $n$, +$$ +\mathbb{P}(|\chi(G) - f(n)| < \omega(n)) < 1/2. +$$ +That is, the chromatic number cannot be concentrated in any interval of width +$2\omega(n)$ with probability $\geq 1/2$. +-/ +@[category research open, AMS 5 60] +theorem erdos_1156.variants.anticoncentration : + ∃ ω : ℕ → ℝ, Tendsto ω atTop atTop ∧ + ∀ f : ℕ → ℝ, ∀ᶠ n in atTop, + chromaticNumberProb n (fun k => |(k : ℝ) - f n| < ω n) < 1 / 2 := by + sorry + +end Erdos1156 diff --git a/FormalConjectures/ErdosProblems/521.lean b/FormalConjectures/ErdosProblems/521.lean new file mode 100644 index 000000000..90f5384c9 --- /dev/null +++ b/FormalConjectures/ErdosProblems/521.lean @@ -0,0 +1,154 @@ +/- +Copyright 2026 The Formal Conjectures Authors. + +Licensed under the Apache License, Version 2.0 (the "License"); +you may not use this file except in compliance with the License. +You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + +Unless required by applicable law or agreed to in writing, software +distributed under the License is distributed on an "AS IS" BASIS, +WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +See the License for the specific language governing permissions and +limitations under the License. +-/ + +import FormalConjectures.Util.ProblemImports + +/-! +# Erdős Problem 521 + +Let $(\varepsilon_k)_{k \geq 0}$ be independently uniformly chosen from $\{-1, 1\}$, +and let $R_n$ count the number of real roots of $f_n(z) = \sum_{k=0}^{n} \varepsilon_k z^k$. +Is it true that, almost surely, $\lim_{n \to \infty} R_n / \log n = 2/\pi$? + +Erdős and Offord [EO56] showed that the expected number of real roots is +$(2/\pi + o(1)) \log n$. This conjecture, posed by Erdős [Er61, p.252], asks whether +the convergence holds almost surely. Do [Do24] proved the partial result that for +roots restricted to $[-1, 1]$, the limit $R_n[-1,1] / \log n \to 1/\pi$ holds +almost surely. + +Note: Erdős's original formulation [Er61, p.252] is ambiguous about whether +the coefficients are from $\{-1, 1\}$ or $\{0, 1\}$. For $\{0, 1\}$ coefficients, +the expected constant is $1/\pi$ rather than $2/\pi$. This formalization uses +$\{-1, 1\}$ (Rademacher), which is the standard modern interpretation. + +## References + +[EO56] Erdős, P., Offord, A. C., _On the number of real roots of a random algebraic +equation_. Proc. London Math. Soc. (3) **6** (1956), 139–160. + +[Er61] Erdős, P., _Some unsolved problems_. Magyar Tud. Akad. Mat. Kutató Int. Közl. +**6** (1961), 221–254. + +[Do24] Do, Y., _A strong law of large numbers for real roots of random polynomials_. +arXiv:2403.06353 (2024). + +*Reference:* [erdosproblems.com/521](https://www.erdosproblems.com/521) +-/ + +open MeasureTheory ProbabilityTheory Polynomial Filter Finset + +open scoped BigOperators + +namespace Erdos521 + +/-- The polynomial with prescribed $\pm 1$ coefficients: +$f_n(z) = \sum_{k=0}^{n} \varepsilon(k) \cdot z^k$. -/ +noncomputable def signPoly (ε : ℕ → ℝ) (n : ℕ) : Polynomial ℝ := + ∑ k ∈ range (n + 1), C (ε k) * X ^ k + +/-- The number of distinct real roots of a real polynomial. -/ +noncomputable def numRealRoots (p : Polynomial ℝ) : ℕ := + Set.ncard {x : ℝ | p.IsRoot x} + +/-- A random variable is Rademacher distributed: it takes values in $\{-1, 1\}$ +with equal probability (each with probability $1/2$ on a probability space). -/ +def IsRademacher {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω) (X : Ω → ℝ) : Prop := + (∀ ω, X ω = 1 ∨ X ω = -1) ∧ + μ {ω | X ω = 1} = μ {ω | X ω = -1} + +/-- +Erdős Problem 521 [Er61, p.252]: +Let $(\varepsilon_k)_{k \geq 0}$ be independently uniformly chosen at random from $\{-1, 1\}$. +If $R_n$ counts the number of real roots of $f_n(z) = \sum_{k=0}^{n} \varepsilon_k z^k$, +then, almost surely, $\lim_{n \to \infty} R_n / \log n = 2/\pi$. + +Erdős and Offord [EO56] showed that the expected number of real roots is +$(2/\pi + o(1)) \log n$. This conjecture asks whether the convergence holds +almost surely. +-/ +@[category research open, AMS 12 60] +theorem erdos_521 : answer(sorry) ↔ + ∀ {Ω : Type*} [MeasurableSpace Ω] {μ : Measure Ω} [IsProbabilityMeasure μ] + {ε : ℕ → Ω → ℝ}, + (∀ k, IsRademacher μ (ε k)) → + iIndepFun ε μ → + ∀ᵐ ω ∂μ, Tendsto + (fun n => (numRealRoots (signPoly (fun k => ε k ω) n) : ℝ) / Real.log (n : ℝ)) + atTop (nhds (2 / Real.pi)) := by + sorry + +/-- The number of distinct real roots of a real polynomial in a given interval $[a, b]$. -/ +noncomputable def numRealRootsIn (p : Polynomial ℝ) (a b : ℝ) : ℕ := + Set.ncard {x : ℝ | p.IsRoot x ∧ a ≤ x ∧ x ≤ b} + +/-- +Do's partial result [Do24]: For random $\pm 1$ polynomials, the number of real roots +in $[-1, 1]$ satisfies $R_n[-1,1] / \log n \to 1/\pi$ almost surely. +This is a partial result towards Erdős Problem 521, resolving the conjecture +for roots restricted to $[-1, 1]$. +-/ +@[category research solved, AMS 12 60] +theorem erdos_521.variants.do_restricted_roots : + ∀ {Ω : Type*} [MeasurableSpace Ω] {μ : Measure Ω} [IsProbabilityMeasure μ] + {ε : ℕ → Ω → ℝ}, + (∀ k, IsRademacher μ (ε k)) → + iIndepFun ε μ → + ∀ᵐ ω ∂μ, Tendsto + (fun n => (numRealRootsIn (signPoly (fun k => ε k ω) n) (-1) 1 : ℝ) / Real.log (n : ℝ)) + atTop (nhds (1 / Real.pi)) := by + sorry + +/-- +Erdős–Offord expectation result [EO56]: The expected number of real roots of a +random degree $n$ polynomial with $\pm 1$ coefficients satisfies +$\mathbb{E}[R_n] / \log n \to 2/\pi$. +This is the convergence in expectation that motivates the almost sure conjecture +(Erdős Problem 521). +-/ +@[category research solved, AMS 12 60] +theorem erdos_521.variants.erdos_offord_expectation : + ∀ {Ω : Type*} [MeasurableSpace Ω] {μ : Measure Ω} [IsProbabilityMeasure μ] + {ε : ℕ → Ω → ℝ}, + (∀ k, IsRademacher μ (ε k)) → + iIndepFun ε μ → + Tendsto + (fun n => (∫ ω, (numRealRoots (signPoly (fun k => ε k ω) n) : ℝ) ∂μ) / Real.log (n : ℝ)) + atTop (nhds (2 / Real.pi)) := by + sorry + +/-- A random variable is Bernoulli(1/2) distributed: it takes values in $\{0, 1\}$ +with equal probability. -/ +def IsBernoulliHalf {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω) (X : Ω → ℝ) : Prop := + (∀ ω, X ω = 0 ∨ X ω = 1) ∧ + μ {ω | X ω = 0} = μ {ω | X ω = 1} + +/-- +$\{0, 1\}$ coefficient variant: Erdős's original formulation [Er61, p.252] may have +intended coefficients from $\{0, 1\}$ instead of $\{-1, 1\}$. For $\{0, 1\}$ coefficients, +the expected constant is $1/\pi$ rather than $2/\pi$. +-/ +@[category research open, AMS 12 60] +theorem erdos_521.variants.zero_one_coefficients : answer(sorry) ↔ + ∀ {Ω : Type*} [MeasurableSpace Ω] {μ : Measure Ω} [IsProbabilityMeasure μ] + {ε : ℕ → Ω → ℝ}, + (∀ k, IsBernoulliHalf μ (ε k)) → + iIndepFun ε μ → + ∀ᵐ ω ∂μ, Tendsto + (fun n => (numRealRoots (signPoly (fun k => ε k ω) n) : ℝ) / Real.log (n : ℝ)) + atTop (nhds (1 / Real.pi)) := by + sorry + +end Erdos521 diff --git a/FormalConjectures/ErdosProblems/524.lean b/FormalConjectures/ErdosProblems/524.lean new file mode 100644 index 000000000..934feece1 --- /dev/null +++ b/FormalConjectures/ErdosProblems/524.lean @@ -0,0 +1,105 @@ +/- +Copyright 2026 The Formal Conjectures Authors. + +Licensed under the Apache License, Version 2.0 (the "License"); +you may not use this file except in compliance with the License. +You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + +Unless required by applicable law or agreed to in writing, software +distributed under the License is distributed on an "AS IS" BASIS, +WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +See the License for the specific language governing permissions and +limitations under the License. +-/ + +import FormalConjectures.Util.ProblemImports + +/-! +# Erdős Problem 524 + +A problem of Salem and Zygmund [SaZy54]. For any $t \in (0,1)$ let +$t = \sum_{k=1}^{\infty} \varepsilon_k(t) 2^{-k}$ be the binary expansion (where +$\varepsilon_k(t) \in \{0,1\}$). What is the correct order of magnitude (for almost all +$t \in (0,1)$) of +$$M_n(t) = \max_{x \in [-1,1]} \left|\sum_{k \le n} (-1)^{\varepsilon_k(t)} x^k\right|?$$ + +The binary digits $\varepsilon_k(t)$ are i.i.d. Bernoulli$(1/2)$ under Lebesgue measure, so +$(-1)^{\varepsilon_k(t)}$ are i.i.d. Rademacher random variables. + +**Known partial results:** +- Erdős showed: for a.a. $t$ and every $\delta > 0$, + $\limsup_{n \to \infty} M_n(t)/n^{1/2 - \delta} = \infty$. +- Chung showed: for a.a. $t$, there exist infinitely many $n$ such that + $M_n(t) \ll (n / \log \log n)^{1/2}$. + +## References + +[Er61] Erdős, P., _Some unsolved problems_. Magyar Tud. Akad. Mat. Kutató Int. +Közl. **6** (1961), 221–254, p.253. + +[SaZy54] Salem, R., Zygmund, A., _Some properties of trigonometric series whose +terms have random signs_. Acta Mathematica (1954), 245–301. + +*Reference:* [erdosproblems.com/524](https://www.erdosproblems.com/524) +-/ + +open MeasureTheory ProbabilityTheory Filter Finset BigOperators Set Asymptotics + +namespace Erdos524 + +/-- A random variable is Rademacher distributed: it takes values in $\{-1, 1\}$ +with equal probability. -/ +def IsRademacher {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω) (X : Ω → ℝ) : Prop := + (∀ ω, X ω = 1 ∨ X ω = -1) ∧ + μ {ω | X ω = 1} = μ {ω | X ω = -1} + +/-- The supremum of $\left|\sum_{k=1}^n \varepsilon_k x^k\right|$ over $x \in [-1, 1]$. -/ +noncomputable def supNormInterval (ε : ℕ → ℝ) (n : ℕ) : ℝ := + sSup {y : ℝ | ∃ x : ℝ, x ∈ Icc (-1 : ℝ) 1 ∧ + y = |∑ k ∈ Finset.range n, ε (k + 1) * x ^ (k + 1)|} + +/-- What is the correct order of magnitude of $M_n(t)$ for almost all $t$? +The answer $f : \mathbb{N} \to \mathbb{R}$ should satisfy +$M_n(\omega) =\Theta(f(n))$ as $n \to \infty$ for a.a. $\omega$. -/ +@[category research open, AMS 42 60] +theorem erdos_524 + {Ω : Type*} [MeasurableSpace Ω] {μ : Measure Ω} [IsProbabilityMeasure μ] + {ε : ℕ → Ω → ℝ} + (hRad : ∀ k, IsRademacher μ (ε k)) + (hIndep : iIndepFun ε μ) : + ∀ᵐ ω ∂μ, + (fun n => supNormInterval (fun k => ε k ω) n) =Θ[atTop] + (answer(sorry) : ℕ → ℝ) := by + sorry + +/-- Erdős showed that for almost all $\omega$ and every $\delta > 0$, +$\limsup_{n \to \infty} M_n(\omega) / n^{1/2 - \delta} = \infty$. -/ +@[category research solved, AMS 42 60] +theorem erdos_524.variants.lower_bound + {Ω : Type*} [MeasurableSpace Ω] {μ : Measure Ω} [IsProbabilityMeasure μ] + {ε : ℕ → Ω → ℝ} + (hRad : ∀ k, IsRademacher μ (ε k)) + (hIndep : iIndepFun ε μ) : + ∀ᵐ ω ∂μ, ∀ δ > (0 : ℝ), ∀ C > (0 : ℝ), + ∃ᶠ n in atTop, + C ≤ supNormInterval (fun k => ε k ω) n / + (↑n : ℝ) ^ ((1 : ℝ)/2 - δ) := by + sorry + +/-- Chung showed that for almost all $\omega$, there exist infinitely many $n$ such that +$M_n(\omega) \ll (n / \log \log n)^{1/2}$. -/ +@[category research solved, AMS 42 60] +theorem erdos_524.variants.upper_bound + {Ω : Type*} [MeasurableSpace Ω] {μ : Measure Ω} [IsProbabilityMeasure μ] + {ε : ℕ → Ω → ℝ} + (hRad : ∀ k, IsRademacher μ (ε k)) + (hIndep : iIndepFun ε μ) : + ∃ C > (0 : ℝ), ∀ᵐ ω ∂μ, + ∃ᶠ n in atTop, + supNormInterval (fun k => ε k ω) n ≤ + C * ((↑n : ℝ) / Real.log (Real.log (↑n : ℝ))) ^ ((1 : ℝ)/2) := by + sorry + +end Erdos524 diff --git a/FormalConjectures/ErdosProblems/529.lean b/FormalConjectures/ErdosProblems/529.lean new file mode 100644 index 000000000..40c7e67ff --- /dev/null +++ b/FormalConjectures/ErdosProblems/529.lean @@ -0,0 +1,110 @@ +/- +Copyright 2026 The Formal Conjectures Authors. + +Licensed under the Apache License, Version 2.0 (the "License"); +you may not use this file except in compliance with the License. +You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + +Unless required by applicable law or agreed to in writing, software +distributed under the License is distributed on an "AS IS" BASIS, +WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +See the License for the specific language governing permissions and +limitations under the License. +-/ + +import FormalConjectures.Util.ProblemImports + +/-! +# Erdős Problem 529 + +Let $d_k(n)$ denote the expected Euclidean distance from the origin of the endpoint of a +uniformly random $n$-step self-avoiding walk on $\mathbb{Z}^k$. The problem asks whether +$d_2(n)/\sqrt{n} \to \infty$ (Part 1) and whether $d_k(n) \ll \sqrt{n}$ for $k \geq 3$ (Part 2). + +*Reference:* [erdosproblems.com/529](https://www.erdosproblems.com/529) + +[Er61] Erdős, P., _Some unsolved problems_, Magyar Tud. Akad. Mat. Kutató Int. Közl. 6 (1961), +221–254, p. 254. + +[Sl87] Slade, G., _The diffusion of self-avoiding random walk in high dimensions_, +Comm. Math. Phys. **108** (1987), 661–683. + +[HaSl91] Hara, T., Slade, G., _Critical behaviour of self-avoiding walk in five or more +dimensions_, Bull. Amer. Math. Soc. (N.S.) **25** (1991), 417–423. + +[HaSl92] Hara, T., Slade, G., _Self-avoiding walk in five or more dimensions. I. The critical +behaviour_, Comm. Math. Phys. **147** (1992), 101–136. + +[MaSl93] Madras, N., Slade, G., _The Self-Avoiding Walk_, Birkhäuser (1993), xiv+425 pp. + +[DuHa13] Duminil-Copin, H., Hammond, A., _Self-avoiding walk is sub-ballistic_, +Comm. Math. Phys. **324** (2013), 401–423. +-/ + +open BigOperators Filter Classical + +namespace Erdos529 + +/-- Two points in $\mathbb{Z}^k$ are adjacent in the integer lattice if their $\ell^1$ distance +is $1$ (i.e., they differ by $\pm 1$ in exactly one coordinate). -/ +def LatticeAdj {k : ℕ} (x y : Fin k → ℤ) : Prop := + (∑ i : Fin k, |x i - y i|) = 1 + +/-- The set of self-avoiding walks of $n$ steps in $\mathbb{Z}^k$ starting at the origin. -/ +def selfAvoidingWalks (n k : ℕ) : Set (Fin (n + 1) → (Fin k → ℤ)) := + {w | w 0 = 0 ∧ + (∀ i : Fin n, LatticeAdj (w ⟨i.val, by omega⟩) (w ⟨i.val + 1, by omega⟩)) ∧ + Function.Injective w} + +/-- The Euclidean distance of a point in $\mathbb{Z}^k$ from the origin. -/ +noncomputable def euclidDistFromOrigin {k : ℕ} (x : Fin k → ℤ) : ℝ := + Real.sqrt (∑ i : Fin k, ((x i : ℝ)) ^ 2) + +/-- The expected Euclidean distance from the origin of the endpoint of a uniformly +random self-avoiding walk of $n$ steps in $\mathbb{Z}^k$. +$$d_k(n) = \frac{1}{|\mathrm{SAW}(n,k)|} \cdot \sum_{w \in \mathrm{SAW}(n,k)} \|w(n)\|_2$$ -/ +noncomputable def expectedSAWDist (n k : ℕ) : ℝ := + if h : (selfAvoidingWalks n k).Finite then + (h.toFinset.sum (fun w => euclidDistFromOrigin (w ⟨n, by omega⟩))) / + (h.toFinset.card : ℝ) + else 0 + +/-- +Erdős Problem 529, Part 1: + +Let $d_k(n)$ be the expected distance from the origin after taking $n$ steps of a +uniformly random self-avoiding walk in $\mathbb{Z}^k$. Is it true that +$$\lim_{n \to \infty} \frac{d_2(n)}{n^{1/2}} = \infty?$$ + +That is, in two dimensions, does the expected endpoint distance grow strictly +faster than $\sqrt{n}$? + +Duminil-Copin and Hammond [DuHa13] proved $d_2(n) = o(n)$. It is conjectured +that $d_2(n) \sim D \cdot n^{3/4}$. +-/ +@[category research open, AMS 5 60] +theorem erdos_529 : answer(sorry) ↔ + Tendsto (fun n : ℕ => expectedSAWDist n 2 / (n : ℝ) ^ ((1 : ℝ) / 2)) + atTop atTop := by + sorry + +/-- +Erdős Problem 529, Part 2: + +Is it true that $d_k(n) \ll n^{1/2}$ for $k \geq 3$? + +Hara and Slade proved $d_k(n) \sim D \cdot n^{1/2}$ for all $k \geq 5$. It is now believed +that this is false for $k = 3$ and $k = 4$: the conjectured behavior is +$d_3(n) \sim n^{\nu}$ where $\nu \approx 0.59$ and +$d_4(n) \sim D \cdot (\log n)^{1/8} \cdot n^{1/2}$. +-/ +@[category research open, AMS 5 60] +theorem erdos_529.variants.part2 : answer(sorry) ↔ + ∀ k : ℕ, k ≥ 3 → + ∃ C : ℝ, 0 < C ∧ ∀ᶠ n in atTop, + expectedSAWDist n k ≤ C * (n : ℝ) ^ ((1 : ℝ) / 2) := by + sorry + +end Erdos529