Erdős problem 521
Let be independently uniformly chosen at random from . If counts the number of real roots of then is it true that, almost surely,
Sources
FormalConjectures/ErdosProblems/
521.lean
Retained formal statement
fairCoin gives each of the two signs mass 1/2. Together with fairCoin_isProbabilityMeasure this pins the definition down, so a proof stating the same problem with a Bernoulli(1/2) measure is stating the same thing.
∀ (b : Bool), Erdos521.fairCoin {b} = 2⁻¹APIStatement only, no proofformal statement reference