OAI/NumberTheory/Ostmann/Construction/TailBroadPriorBalance.lean
1 declarations, 0 contain sorry, 0 declared as axioms
The original broad bulk prior has balanced mass at least one half
- theorem
OAI.Ostmann.EventuallyPrimeSumset.tail_broad_prior_balanceline 13