OAI/NumberTheory/Ostmann/Arithmetic/GiantCollisionErrorBasic.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.Arithmetic.GiantCollisionError.weighted_error_of_agree_off line 11
2. theorem OAI.Ostmann.Arithmetic.GiantCollisionError.cmean_error_of_agree_off line 31
3. theorem OAI.Ostmann.Arithmetic.GiantCollisionError.equality_mass_le line 40
4. theorem OAI.Ostmann.Arithmetic.GiantCollisionError.primeSource_not_coprime_iff_eq line 51
5. theorem OAI.Ostmann.Arithmetic.GiantCollisionError.primeSource_collision_mass_le line 56
6. theorem OAI.Ostmann.Arithmetic.GiantCollisionError.logCellPrior_mass_le_exp line 61
7. theorem OAI.Ostmann.Arithmetic.GiantCollisionError.logCell_collision_mass_le line 68
8. theorem OAI.Ostmann.Arithmetic.GiantCollisionError.logCell_guard_error line 74