OAI/Combinatorics/Progressions/Geometry/ActualFixedSpatialRetainedModulusBudget.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.crtPolynomialInputLaw_integerLong_density_of_output line 10
  2. def OAI.Erdos3.VectorPolynomial.ActualFixedSpatialForecastPath.retainedLabelDecidableEq line 69
  3. def OAI.Erdos3.VectorPolynomial.ActualFixedSpatialForecastPath.referenceRetainedCRTModulus line 74
  4. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialForecastPath.referenceRetainedCRTModulus_eq line 78
  5. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialForecastPath.referenceRetainedCRTModulus_dvd line 84
  6. def OAI.Erdos3.VectorPolynomial.ActualFixedSpatialForecastPath.referenceRetainedCRTInputLaw line 96
  7. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialForecastPath.referenceRetainedCRT_density_eq line 109
  8. def OAI.Erdos3.VectorPolynomial.ActualFixedSpatialForecastPath.retainedCRTReferenceForecast line 139
  9. def OAI.Erdos3.VectorPolynomial.ActualFixedSpatialForecastPath.retainedCRTIndependentForecast line 152
  10. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialForecastPath.retainedCRTIndependentForecast_eq line 177
  11. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialForecastPath.retainedCRTReferenceForecast_eq_independent line 200
  12. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialForecastPath.retainedCRTReferenceForecast_eq line 216
  13. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialForecastPath.referenceRetainedCRTModulus_pos line 228
  14. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialForecastPath.reference_inactive_goodPrimeDeletion_retainedCRT line 238
  15. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialForecastPath.referenceRetainedCRTModulus_log_le_tested line 295
  16. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialForecastPath.referenceRetainedCRTModulus_le_exp_tested line 310