OAI/NumberTheory/Ostmann/Arithmetic/HistoryBulkFibreGiantErrorAverageSelectedDefs.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.Arithmetic.HistoryBulkFibreGiantErrorAverage.leftChoices_mass_of_draws line 18
2. theorem OAI.Ostmann.Arithmetic.HistoryBulkFibreGiantErrorAverage.rightChoices_mass_of_draws line 24
3. theorem OAI.Ostmann.Arithmetic.HistoryBulkFibreGiantErrorAverage.spectatorList_source line 30
4. def OAI.Ostmann.Arithmetic.HistoryBulkFibreGiantErrorAverage.primeOriginalValue line 37
5. def OAI.Ostmann.Arithmetic.HistoryBulkFibreGiantErrorAverage.mixedOriginalValue line 45
6. def OAI.Ostmann.Arithmetic.HistoryBulkFibreGiantErrorAverage.primeSelectedPrincipal line 55
7. def OAI.Ostmann.Arithmetic.HistoryBulkFibreGiantErrorAverage.mixedSelectedPrincipal line 76