OAI/NumberTheory/Ostmann/Arithmetic/PairedFrequencyTreeSumData.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.Arithmetic.PairedFrequencyTreeSum.defaultData line 11
2. def OAI.Ostmann.Arithmetic.PairedFrequencyTreeSum.assignmentDataForward line 17
3. def OAI.Ostmann.Arithmetic.PairedFrequencyTreeSum.assignmentData line 27
4. theorem OAI.Ostmann.Arithmetic.PairedFrequencyTreeSum.assignmentData_left line 31
5. theorem OAI.Ostmann.Arithmetic.PairedFrequencyTreeSum.assignmentData_right line 36
6. theorem OAI.Ostmann.Arithmetic.PairedFrequencyTreeSum.budget_eq_weight_shift line 41
7. theorem OAI.Ostmann.Arithmetic.PairedFrequencyTreeSum.budget_eq_weight line 68