OAI/NumberTheory/Ostmann/Construction/HarmonicPriorEvent.lean
2 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.Ostmann.Construction.harmonicPrimeSource_event_meanline 12 - theorem
OAI.Ostmann.Construction.broadBand_balanced_prior_eventuallyline 26