OAI/NumberTheory/Jacobsthal/Partitions/FiniteWeightedChoiceBox.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos970.NumberTheoryLean.FiniteWeightedChoiceBox.points line 14
2. def OAI.Erdos970.NumberTheoryLean.FiniteWeightedChoiceBox.pointWeight line 15
3. def OAI.Erdos970.NumberTheoryLean.FiniteWeightedChoiceBox.boxMass line 16
4. def OAI.Erdos970.NumberTheoryLean.FiniteWeightedChoiceBox.restrictedPoints line 18
5. theorem OAI.Erdos970.NumberTheoryLean.FiniteWeightedChoiceBox.mass_factorizes line 21
6. theorem OAI.Erdos970.NumberTheoryLean.FiniteWeightedChoiceBox.weight_nonnegative line 25
7. theorem OAI.Erdos970.NumberTheoryLean.FiniteWeightedChoiceBox.restricted_eq line 28
8. theorem OAI.Erdos970.NumberTheoryLean.FiniteWeightedChoiceBox.restriction_mass_bound line 49
9. theorem OAI.Erdos970.NumberTheoryLean.FiniteWeightedChoiceBox.coordinate_mass_bound line 68
10. theorem OAI.Erdos970.NumberTheoryLean.FiniteWeightedChoiceBox.union_mass_bound line 78