OAI/NumberTheory/Jacobsthal/Partitions/SourceParentBin.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos970.NumberTheoryLean.SourceParentBin.index line 17
2. def OAI.Erdos970.NumberTheoryLean.SourceParentBin.initialConstant line 18
3. theorem OAI.Erdos970.NumberTheoryLean.SourceParentBin.initialConstant_pos line 20
4. theorem OAI.Erdos970.NumberTheoryLean.SourceParentBin.source_cell line 24
5. theorem OAI.Erdos970.NumberTheoryLean.SourceParentBin.source_left_valid line 34
6. theorem OAI.Erdos970.NumberTheoryLean.SourceParentBin.source_inverse_weight line 42
7. theorem OAI.Erdos970.NumberTheoryLean.SourceParentBin.source_coverage line 53
8. theorem OAI.Erdos970.NumberTheoryLean.SourceParentBin.source_grid_mass line 62
9. theorem OAI.Erdos970.NumberTheoryLean.SourceParentBin.bin_empty_above line 68
10. theorem OAI.Erdos970.NumberTheoryLean.SourceParentBin.mass_zero_above line 78