OAI/NumberTheory/Ostmann/Arithmetic/HistoryBulkFibreGiantErrorAverageCompensation.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.Arithmetic.HistoryBulkFibreGiantErrorAverage.choiceCompensation line 19
2. def OAI.Ostmann.Arithmetic.HistoryBulkFibreGiantErrorAverage.pairedChoiceCompensation line 26
3. theorem OAI.Ostmann.Arithmetic.HistoryBulkFibreGiantErrorAverage.choiceCompensation_nonneg line 31
4. theorem OAI.Ostmann.Arithmetic.HistoryBulkFibreGiantErrorAverage.pairedChoiceCompensation_nonneg line 36
5. theorem OAI.Ostmann.Arithmetic.HistoryBulkFibreGiantErrorAverage.assigned_compensationProduct line 41
6. theorem OAI.Ostmann.Arithmetic.HistoryBulkFibreGiantErrorAverage.frame_left_compensation line 53
7. theorem OAI.Ostmann.Arithmetic.HistoryBulkFibreGiantErrorAverage.frame_right_compensation line 57
8. theorem OAI.Ostmann.Arithmetic.HistoryBulkFibreGiantErrorAverage.frame_oldCompensation line 61
9. theorem OAI.Ostmann.Arithmetic.HistoryBulkFibreGiantErrorAverage.frame_norm_oldCompensation line 69
10. theorem OAI.Ostmann.Arithmetic.HistoryBulkFibreGiantErrorAverage.selected_pairedChoiceCompensation_error_eventually line 75