OAI/NumberTheory/Jacobsthal/Partitions/PaperGeometricRegularity.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos970.NumberTheoryLean.GeometricDefectPartition.geometric_defect_sum line 21
2. theorem OAI.Erdos970.NumberTheoryLean.GeometricRegularMass.geometric_regular_defect_mass line 55
3. theorem OAI.Erdos970.NumberTheoryLean.UniformGeometricRegularMass.geometric_defect_uniform_in_L line 106
4. def OAI.Erdos970.NumberTheoryLean.ExpandedCompactPartition.listedWord line 161
5. def OAI.Erdos970.NumberTheoryLean.ExpandedCompactPartition.unlistedGeometric line 167
6. theorem OAI.Erdos970.NumberTheoryLean.ExpandedCompactPartition.expanded_geometric_mass_split line 173
7. theorem OAI.Erdos970.NumberTheoryLean.ExpandedCompactPartition.bad_compact_reference_data line 207
8. theorem OAI.Erdos970.NumberTheoryLean.PaperGeometricRegularity.paper_geometric_defect_mass line 229