OAI/NumberTheory/Ostmann/Arithmetic/LogCellPartitionBoundary.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.Arithmetic.LogCellPartition.log_eq_left_of_closed_not_assigned line 14
2. theorem OAI.Ostmann.Arithmetic.LogCellPartition.closed_assigned_difference_card_le line 26
3. theorem OAI.Ostmann.Arithmetic.LogCellPartition.norm_closed_assigned_test_error line 42
4. def OAI.Ostmann.Arithmetic.LogCellPartition.assignedResidueMass line 66
5. theorem OAI.Ostmann.Arithmetic.LogCellPartition.residueMass_assigned_error line 71