Erdős Problem #522

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.poly

We can always view a Kac polynomial as a random variable on `ℕ`. -/ instance : FunLike (KacCoefficients S Ω μ) ℕ (Ω → k) where coe P := P.toFun coe_injective P Q h := by aesop namespace KacCoefficients open scoped Polynomial variable {S Ω} {μ : Measure 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`.

The random multiset of roots associated to a Kac polynomial