OAI/NumberTheory/Jacobsthal/Estimates/MinorizingCostRegularity.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos970.NumberTheoryLean.MinorizingCostRegularity.cost_strictAntiOn line 15
2. theorem OAI.Erdos970.NumberTheoryLean.MinorizingCostRegularity.cost_level_null line 23
3. theorem OAI.Erdos970.NumberTheoryLean.MinorizingCostRegularity.rectangleLaw_cost_level line 34
4. theorem OAI.Erdos970.NumberTheoryLean.MinorizingCostRegularity.minorizingLaw_cost_level line 48
5. theorem OAI.Erdos970.NumberTheoryLean.MinorizingCostRegularity.minorizingCost_nullSingletonClass line 54
6. theorem OAI.Erdos970.NumberTheoryLean.MinorizingCostRegularity.minorizingCost_countable_null line 61