OAI/Combinatorics/Progressions/Lattices/ActualFixedSpatialGoodPrimeDeletion.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.retainedPrimeProduct_le_chargedProduct_mul_smallProduct line 13
2. theorem OAI.Erdos3.retainedPrimePowerModulus_le_power_of_primeProduct line 49
3. theorem OAI.Erdos3.retainedPrimePowerModulus_le_charged_cutoff line 58
4. theorem OAI.Erdos3.retainedPrimePowerModulus_filter_le_charged_cutoff line 75
5. theorem OAI.Erdos3.retainedPrimePowerModulus_le_exp_charged_cutoff line 99
6. theorem OAI.Erdos3.retainedPrimePowerModulus_filter_le_exp_charged_cutoff line 138
7. theorem OAI.Erdos3.primePowerProduct_expBudget_nonneg line 165
8. theorem OAI.Erdos3.retainedPrimePower_cutoff_logCost_nonneg line 173
9. theorem OAI.Erdos3.retainedPrimePowerModulus_le_exp_depthBudget line 180
10. theorem OAI.Erdos3.log_retainedPrimePowerModulus_le_depthBudget line 201
11. theorem OAI.Erdos3.log_retainedPrimePowerModulus_filter_le_depthBudget line 221
12. def OAI.Erdos3.VectorPolynomial.ActualFixedSpatialForecastPath.referenceRetainedPrimes line 279
13. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialForecastPath.referenceRetainedPrimes_omitted line 284
14. def OAI.Erdos3.VectorPolynomial.ActualFixedSpatialForecastPath.referenceLocalDensity line 291
15. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialForecastPath.referenceLocalDensity_nonneg line 307
16. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialForecastPath.reference_rational_density_product line 316
17. def OAI.Erdos3.VectorPolynomial.ActualFixedSpatialForecastPath.retainedReferenceForecast line 332
18. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialForecastPath.reference_inactive_density_product line 342
19. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialForecastPath.reference_inactive_goodPrimeDeletion line 358
20. def OAI.Erdos3.VectorPolynomial.ActualFixedSpatialForecastPath.referenceRetainedModulus line 392
21. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialForecastPath.referenceRetainedModulus_le line 396
22. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialForecastPath.referenceRetainedModulus_le_exp line 412
23. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialForecastPath.referenceRetainedModulus_pos line 427
24. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialForecastPath.referenceRetainedModulus_dvd line 434
25. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialForecastPath.referenceRetainedModulus_log_le line 441