Erdős Problem 522

Reference: erdosproblems.com/522

structure KacPolynomial {k : Type u_1} (n : ℕ) [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 Kac Polynomial in n coefficients over some subset S of a field k is a polynomial whose n first coefficients are picked uniformely at random in S and whose other coefficients are all 0

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

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

instance instFunLikeKacPolynomialFinSuccForall {k : Type u_1} (n : ℕ) [Field k] [MeasurableSpace k] (S : Set k) (Ω : Type u_2) [MeasureTheory.MeasureSpace Ω] (μ : MeasureTheory.Measure k := by volume_tac) : FunLike (KacPolynomial n S Ω μ) (Fin n.succ) (Ω → k)

We can always view a Kac polynomial as a random vector

Equations

• instFunLikeKacPolynomialFinSuccForall n S Ω μ = { coe := fun (P : KacPolynomial n S Ω μ) => P.toFun, coe_injective' := ⋯ }

noncomputable def KacPolynomial.toRandomPolynomial {k : Type u_1} {n : ℕ} [Field k] [MeasurableSpace k] {S : Set k} {Ω : Type u_2} [MeasureTheory.MeasureSpace Ω] {μ : MeasureTheory.Measure k} (f : KacPolynomial n S Ω μ) : Ω → Polynomial k

The random polynomial associated to a Kac polynomial

Equations

• f.toRandomPolynomial ω = ∑ i : Fin n.succ, (Polynomial.monomial ↑i) (f i ω)

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

The random multiset of roots associated to a Kac polynomial

Equations

• f.roots ω = (f.toRandomPolynomial ω).roots

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

Let f(z)=∑_{0≤k≤n} ϵ_k z^k be a random polynomial, where ϵ_k∈{−1,1} independently uniformly at random for 0≤k≤n. Is it true that the number of roots of f(z) in {z∈C:|z|≤1} is, almost surely, (1/2+o(1))n?

Formalization note: here the goal seems to mean that ℙ(| #roots of f in unit disk - n/2 | ≥ o(1)) → 0 as n → ∞ This is quite awkward to formalise!

theorem 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 Ω] [inst_1 : MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] (n : ℕ), 2 ≤ n → ∀ (f : KacPolynomial n {-1, 1} Ω MeasureTheory.volume), (MeasureTheory.volume {ω : Ω | |↑(f.roots ω).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 erdos_522.variants.yakir_solution : ∃ (p : ℕ → ℝ), Filter.Tendsto p Filter.atTop (nhds 0) ∧ ∀ (Ω : Type u_3) [inst : MeasureTheory.MeasureSpace Ω] [inst_1 : MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] (n : ℕ), 2 ≤ n → ∀ (f : KacPolynomial n {-1, 1} Ω MeasureTheory.volume), (MeasureTheory.volume {ω : Ω | |↑(Multiset.countP (fun (x : ℂ) => x ∈ Metric.closedBall 0 1) (f.roots ω)) - ↑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}.