OAI/NumberTheory/Ostmann/Construction/GiantCoprimeRates.lean
3 declarations, 0 contain sorry, 0 declared as axioms
The top-giant coprimality loss is below the joint comparison error
- theorem
OAI.Ostmann.giant_coprime_error_rateline 12 - theorem
OAI.Ostmann.prime_pair_coprime_removal_rateline 24 - theorem
OAI.Ostmann.mixed_pair_coprime_removal_rateline 43