FormalConjectures/ErdosProblems/522.lean

GitHub source file

9 declarations, 4 contain sorry, 0 declared as axioms

1. structure Erdos522.KacCoefficients Documented declaration: KacCoefficients line 54 source

   Source documentation

   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 with respect to the reference measure μ. The default reference measure is the counting measure, so that for a finite set S each coefficient takes every value of S with probability 1 / |S|.

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

   standard axioms: Classical.choice, Quot.sound, propext what this means

   Statement uses: Field, MeasurableSpace, Set, MeasureTheory.MeasureSpace, optParam, MeasureTheory.Measure, MeasureTheory.Measure.count

   Tactic trace: 1 steps

   Open to load the checked before-and-after goal states.

   structure KacCoefficients
       {k : Type*} [Field k] [MeasurableSpace k] (S : Set k)
       (Ω : Type*) [MeasureSpace Ω] (μ : Measure k := Measure.count) where
   …

2. instance Erdos522.(instance at line 67) line 67 source

   Source documentation

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

   instance : FunLike (KacCoefficients S Ω μ) ℕ (Ω → k) where
   …

   Mentions: Erdos522.KacCoefficients

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

   Source documentation

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

   standard axioms: Classical.choice, Quot.sound, propext what this means

   Statement uses: Field, MeasurableSpace, Set, MeasureTheory.MeasureSpace, MeasureTheory.Measure, Erdos522.KacCoefficients, Nat, Polynomial

   Proof uses: Finset.sum, Finset.range, HAdd.hAdd, OfNat.ofNat, LinearMap, RingHom.id, Polynomial.monomial

   17 instances, coercions and auxiliary constants left out.

   noncomputable def polynomial (c : KacCoefficients S Ω μ) (n : ℕ) :
       Ω → k[X] := fun ω => ∑ i ∈ Finset.range (n + 1), Polynomial.monomial i (c i ω)

   Mentions: c, Erdos522.KacCoefficients

4. def Erdos522.KacCoefficients.roots The random multiset of roots associated to a Kac polynomial line 87 source

   Source documentation

   The random multiset of roots associated to a Kac polynomial

   standard axioms: Classical.choice, Quot.sound, propext what this means

   Statement uses: Field, MeasurableSpace, Set, MeasureTheory.MeasureSpace, MeasureTheory.Measure, Erdos522.KacCoefficients, Nat, Multiset

   Proof uses: Polynomial.roots, Erdos522.KacCoefficients.polynomial

   2 instances, coercions and auxiliary constants left out.

   noncomputable def roots (c : KacCoefficients S Ω μ) (n : ℕ) : Ω → Multiset k :=
   …

   Mentions: c, Erdos522.KacCoefficients

5. def Erdos522.KacCoefficients.numRootsInUnitDisk Counts the number of roots of a Kac polynomial in the unit disk with multiplicity line 91 source

   Source documentation

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

   standard axioms: Classical.choice, Quot.sound, propext what this means

   Statement uses: Field, MeasurableSpace, Set, MeasureTheory.MeasureSpace, MeasureTheory.Measure, PseudoMetricSpace, Erdos522.KacCoefficients, Nat

   Proof uses: Multiset.countP, Membership.mem, Metric.closedBall, OfNat.ofNat, Real, Classical.propDecidable, Erdos522.KacCoefficients.roots

   9 instances, coercions and auxiliary constants left out.

   noncomputable def numRootsInUnitDisk [PseudoMetricSpace k] (c : KacCoefficients S Ω μ) (n : ℕ)
       (ω : Ω) : ℕ :=
   …

   Mentions: c, Erdos522.KacCoefficients

6. theorem Erdos522.erdos_522 sorry line 126 source

   depends on sorry what this means

   Statement uses: Iff, True, MeasureTheory.MeasureSpace, MeasureTheory.IsProbabilityMeasure, MeasureTheory.MeasureSpace.volume, Erdos522.KacCoefficients, Complex, Insert.insert, Set, Neg.neg, OfNat.ofNat, Singleton.singleton, MeasureTheory.Measure.count, Eq, ENNReal, MeasureTheory.Measure, Set.ofPred, Filter.Tendsto, Nat, Real and 5 more

   Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

   64 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

   Open to load the checked before-and-after goal states.

7. theorem Erdos522.erdos_522.variants.zero_one sorry line 148 source

   depends on sorry what this means

   Statement uses: Iff, True, MeasureTheory.MeasureSpace, MeasureTheory.IsProbabilityMeasure, MeasureTheory.MeasureSpace.volume, Nat, LE.le, OfNat.ofNat, Erdos522.KacCoefficients, Complex, Insert.insert, Set, Singleton.singleton, MeasureTheory.Measure.count, Eq, ENNReal, MeasureTheory.Measure, Set.ofPred, Filter.Tendsto, Real and 5 more

   Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

   68 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

   Open to load the checked before-and-after goal states.

8. theorem Erdos522.erdos_522.variants.number_real_roots 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 sorry line 159 source

   Source documentation

   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.

   depends on sorry what this means

   Statement uses: Exists, Nat, Real, And, Filter.Tendsto, Filter.atTop, nhds, OfNat.ofNat, MeasureTheory.MeasureSpace, MeasureTheory.IsProbabilityMeasure, MeasureTheory.MeasureSpace.volume, LE.le, Erdos522.KacCoefficients, Insert.insert, Set, Neg.neg, Singleton.singleton, MeasureTheory.Measure.count, ENNReal.toReal, MeasureTheory.Measure and 10 more

   Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

   62 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

   Open to load the checked before-and-after goal states.

   theorem erdos_522.variants.number_real_roots : ∃ p o : ℕ → ℝ,
       atTop.Tendsto o (𝓝 0) ∧ atTop.Tendsto p (𝓝 0) ∧
       ∀ (Ω : Type*) [MeasureSpace Ω] [IsProbabilityMeasure (ℙ : Measure Ω)]
         (n : ℕ) (hn : 2 ≤ n) (f : KacCoefficients ({-1, 1} : Set ℝ) Ω),
         (ℙ {ω | |(f.roots n ω).card / (n : ℝ).log - 2 / π| ≥ o n}).toReal ≤ p n := by
   …

   Mentions: Erdos522.KacCoefficients

9. theorem Erdos522.erdos_522.variants.yakir_solution Yakir proved that almost all Kac polynomials have n/2+O(n^(9/10)) many roots in {z∈C:|z|≤1} sorry line 171 source

   Source documentation

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

   depends on sorry what this means

   Statement uses: Exists, Nat, Real, And, Filter.Tendsto, Filter.atTop, nhds, OfNat.ofNat, MeasureTheory.MeasureSpace, MeasureTheory.IsProbabilityMeasure, MeasureTheory.MeasureSpace.volume, LE.le, Erdos522.KacCoefficients, Complex, Insert.insert, Set, Neg.neg, Singleton.singleton, MeasureTheory.Measure.count, ENNReal.toReal and 13 more

   Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

   82 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

   Open to load the checked before-and-after goal states.

   theorem erdos_522.variants.yakir_solution :
       ∃ p : ℕ → ℝ, atTop.Tendsto p (𝓝 0) ∧
       ∀ (Ω : Type*) [MeasureSpace Ω] [IsProbabilityMeasure (ℙ : Measure Ω)]
         (n : ℕ) (hn : 2 ≤ n) (f : KacCoefficients ({-1, 1} : Set ℂ) Ω),
          (ℙ {ω | |(f.roots n ω).countP
            (· ∈ Metric.closedBall 0 1) - (n / 2 : ℝ)| ≥ n^(9/10 : ℝ) }).toReal ≤ p n := by
   …

   Mentions: Erdos522.KacCoefficients