OAI/NumberTheory/Ostmann/Construction/InitialCoordinatesTemplate.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.Construction.InitialCoordinatesTemplate.stateIndex line 14
2. def OAI.Ostmann.Construction.InitialCoordinatesTemplate.outsideIndex line 18
3. theorem OAI.Ostmann.Construction.InitialCoordinatesTemplate.stateIndex_val line 21
4. theorem OAI.Ostmann.Construction.InitialCoordinatesTemplate.outsideIndex_val line 24
5. def OAI.Ostmann.Construction.InitialCoordinatesTemplate.coordinates line 27
6. theorem OAI.Ostmann.Construction.InitialCoordinatesTemplate.coordinates_positive line 36
7. theorem OAI.Ostmann.Construction.InitialCoordinatesTemplate.small_product line 46
8. theorem OAI.Ostmann.Construction.InitialCoordinatesTemplate.spectator_product line 56
9. theorem OAI.Ostmann.Construction.InitialCoordinatesTemplate.coordinates_product line 60
10. theorem OAI.Ostmann.Construction.InitialCoordinatesTemplate.bulk_index_membership line 74
11. theorem OAI.Ostmann.Construction.InitialCoordinatesTemplate.spectator_index_membership line 98
12. theorem OAI.Ostmann.Construction.InitialCoordinatesTemplate.bulk_log_sum line 107
13. theorem OAI.Ostmann.Construction.InitialCoordinatesTemplate.spectator_log_sum line 116
14. theorem OAI.Ostmann.Construction.InitialCoordinatesTemplate.coordinates_bins line 125