OAI/NumberTheory/Jacobsthal/Analysis/SmallModelMeasure.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos970.ErdosVarianceSmallModel.modelUnitIntegers line 14
2. def OAI.Erdos970.ErdosVarianceSmallModel.modelUniverse line 17
3. def OAI.Erdos970.ErdosVarianceSmallModel.atomWeight line 20
4. def OAI.Erdos970.ErdosVarianceSmallModel.modelMass line 24
5. theorem OAI.Erdos970.ErdosVarianceSmallModel.mem_modelUniverse line 27
6. theorem OAI.Erdos970.ErdosVarianceSmallModel.atomWeight_pos line 34
7. theorem OAI.Erdos970.ErdosVarianceSmallModel.modelMass_card line 47
8. theorem OAI.Erdos970.ErdosVarianceSmallModel.modelUniverse_card line 52
9. theorem OAI.Erdos970.ErdosVarianceSmallModel.model_total_mass line 57