OAI/NumberTheory/Ostmann/Arithmetic/HistoryPairedFrequencyAverageData.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.Arithmetic.HistoryPairedFrequencyAverage.LabelsDivide line 9
2. theorem OAI.Ostmann.Arithmetic.HistoryPairedFrequencyAverage.labelsDivide_mono line 15
3. def OAI.Ostmann.Arithmetic.HistoryPairedFrequencyAverage.assignmentModulus line 22
4. theorem OAI.Ostmann.Arithmetic.HistoryPairedFrequencyAverage.labelsDivide_assignmentModulus line 28
5. theorem OAI.Ostmann.Arithmetic.HistoryPairedFrequencyAverage.assignmentModulus_ne_zero line 41
6. def OAI.Ostmann.Arithmetic.HistoryPairedFrequencyAverage.localDataForward line 54
7. def OAI.Ostmann.Arithmetic.HistoryPairedFrequencyAverage.localData line 63
8. theorem OAI.Ostmann.Arithmetic.HistoryPairedFrequencyAverage.localData_left line 67
9. theorem OAI.Ostmann.Arithmetic.HistoryPairedFrequencyAverage.localData_right line 73
10. theorem OAI.Ostmann.Arithmetic.HistoryPairedFrequencyAverage.localData_budget_eq_weight_shift line 79
11. theorem OAI.Ostmann.Arithmetic.HistoryPairedFrequencyAverage.localData_budget_eq_weight line 107