Erdős Problem 522

Reference: erdosproblems.com/522

structure Erdos522.KacCoefficients {k : Type u_1} [Field k] [MeasurableSpace k] (S : Set k) (Ω : Type u_2) [MeasureTheory.MeasureSpace Ω] (μ : MeasureTheory.Measure k := by volume_tac) : Type (max u_1 u_2)

A sequence of Kac coefficients over a subset S of a field k is a countably infinite sequence of independent random variables, each uniformly distributed over S.

Such a sequence determines a Kac polynomial of degree n for each n, which is the random polynomial given by KacCoefficients.polynomial.

• toFun : ℕ → Ω → k
• h_indep : ProbabilityTheory.iIndepFun self.toFun MeasureTheory.volume
• h_unif (i : ℕ) : MeasureTheory.pdf.IsUniform (self.toFun i) S MeasureTheory.volume μ

theorem Erdos522.KacCoefficients.ext_iff {k : Type u_1} {inst✝ : Field k} {inst✝¹ : MeasurableSpace k} {S : Set k} {Ω : Type u_2} {inst✝² : MeasureTheory.MeasureSpace Ω} {μ : autoParam (MeasureTheory.Measure k) _auto_1} {x y : KacCoefficients S Ω μ} : x = y ↔ x.toFun = y.toFun

theorem Erdos522.KacCoefficients.ext {k : Type u_1} {inst✝ : Field k} {inst✝¹ : MeasurableSpace k} {S : Set k} {Ω : Type u_2} {inst✝² : MeasureTheory.MeasureSpace Ω} {μ : autoParam (MeasureTheory.Measure k) _auto_1} {x y : KacCoefficients S Ω μ} (toFun : x.toFun = y.toFun) : x = y

instance Erdos522.instFunLikeKacCoefficientsNatForall {k : Type u_1} [Field k] [MeasurableSpace k] (S : Set k) (Ω : Type u_2) [MeasureTheory.MeasureSpace Ω] (μ : MeasureTheory.Measure k := by volume_tac) : FunLike (KacCoefficients S Ω μ) ℕ (Ω → k)

We can always view a Kac polynomial as a random variable on ℕ.

Equations

• Erdos522.instFunLikeKacCoefficientsNatForall S Ω μ = { coe := fun (P : Erdos522.KacCoefficients S Ω μ) => P.toFun, coe_injective' := ⋯ }

noncomputable def Erdos522.KacCoefficients.polynomial {k : Type u_1} [Field k] [MeasurableSpace k] {S : Set k} {Ω : Type u_2} [MeasureTheory.MeasureSpace Ω] {μ : MeasureTheory.Measure k} (c : KacCoefficients S Ω μ) (n : ℕ) : Ω → Polynomial k

The random polynomial associated to a sequence c : KacCoefficients S Ω μ of Kac coefficients given by ∑ i ∈ Finset.range (n + 1), c i z^i.

Equations

• c.polynomial n ω = ∑ i ∈ Finset.range (n + 1), (Polynomial.monomial i) (c i ω)

noncomputable def Erdos522.KacCoefficients.roots {k : Type u_1} [Field k] [MeasurableSpace k] {S : Set k} {Ω : Type u_2} [MeasureTheory.MeasureSpace Ω] {μ : MeasureTheory.Measure k} (c : KacCoefficients S Ω μ) (n : ℕ) : Ω → Multiset k

The random multiset of roots associated to a Kac polynomial

Equations

• c.roots n ω = (c.polynomial n ω).roots

noncomputable def Erdos522.KacCoefficients.numRootsInUnitDisk {k : Type u_1} [Field k] [MeasurableSpace k] {S : Set k} {Ω : Type u_2} [MeasureTheory.MeasureSpace Ω] {μ : MeasureTheory.Measure k} [PseudoMetricSpace k] (c : KacCoefficients S Ω μ) (n : ℕ) (ω : Ω) : ℕ

Counts the number of roots of a Kac polynomial in the unit disk with multiplicity.

Equations

• c.numRootsInUnitDisk n ω = Multiset.countP (fun (x : k) => x ∈ Metric.closedBall 0 1) (c.roots n ω)

theorem Erdos522.erdos_522 : True ↔ ∀ {Ω : Type u_3} [inst : MeasureTheory.MeasureSpace Ω] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] (c : KacCoefficients {-1, 1} Ω MeasureTheory.volume), MeasureTheory.volume {ω : Ω | Filter.Tendsto (fun (n : ℕ) => 2 * ↑(c.numRootsInUnitDisk n ω) / ↑n) Filter.atTop (nhds 1)} = 1

Let $f(z)=\sum_{0\leq k\leq n} \epsilon_k z^k$ be a random polynomial, where $\epsilon_k\in \{-1,1\}$ independently uniformly at random for $0\leq k\leq n$.

Is it true that, if $R_n$ is the number of roots of $f(z)$ in $\{ z\in \mathbb{C} : \lvert z\rvert \leq 1\}$, then $$ \frac{R_n}{n/2}\to 1 $$ almost surely?

There is some ambiguity as to whether the intended coefficient set is $\{-1, 1\}$ or $\{0, 1\}$, see erdos_522.variants.zero_one for the alternate version.

theorem Erdos522.erdos_522.variants.zero_one : True ↔ ∀ {Ω : Type u_3} [inst : MeasureTheory.MeasureSpace Ω] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] {n : ℕ}, 1 ≤ n → ∀ (f : KacCoefficients {0, 1} Ω MeasureTheory.volume), MeasureTheory.volume {ω : Ω | Filter.Tendsto (fun (n : ℕ) => 2 * ↑(f.numRootsInUnitDisk n ω) / ↑n) Filter.atTop (nhds 1)} = 1

Let $f(z)=\sum_{0\leq k\leq n} \epsilon_k z^k$ be a random polynomial, where $\epsilon_k\in \{0,1\}$ independently uniformly at random for $0\leq k\leq n$.

Is it true that, if $R_n$ is the number of roots of $f(z)$ in $\{ z\in \mathbb{C} : \lvert z\rvert \leq 1\}$, then $$ \frac{R_n}{n/2}\to 1 $$ almost surely?

theorem Erdos522.erdos_522.variants.number_real_roots : ∃ (p : ℕ → ℝ) (o : ℕ → ℝ), Filter.Tendsto o Filter.atTop (nhds 0) ∧ Filter.Tendsto p Filter.atTop (nhds 0) ∧ ∀ (Ω : Type u_3) [inst : MeasureTheory.MeasureSpace Ω] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] (n : ℕ), 2 ≤ n → ∀ (f : KacCoefficients {-1, 1} Ω MeasureTheory.volume), (MeasureTheory.volume {ω : Ω | |↑(f.roots n ω).card / Real.log ↑n - 2 / Real.pi| ≥ o n}).toReal ≤ p n

Erdős and Offord showed that the number of real roots of a random degree n polynomial with ±1 coefficients is (2/π+o(1))log n.

theorem Erdos522.erdos_522.variants.yakir_solution : ∃ (p : ℕ → ℝ), Filter.Tendsto p Filter.atTop (nhds 0) ∧ ∀ (Ω : Type u_3) [inst : MeasureTheory.MeasureSpace Ω] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] (n : ℕ), 2 ≤ n → ∀ (f : KacCoefficients {-1, 1} Ω MeasureTheory.volume), (MeasureTheory.volume {ω : Ω | |↑(Multiset.countP (fun (x : ℂ) => x ∈ Metric.closedBall 0 1) (f.roots n ω)) - ↑n / 2| ≥ ↑n ^ (9 / 10)}).toReal ≤ p n

Yakir proved that almost all Kac polynomials have n/2+O(n^(9/10)) many roots in {z∈C:|z|≤1}.