OAI/Combinatorics/Progressions/Geometry/ActualFixedSpatialSlicedTargetReal.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.VectorPolynomial.ActualFixedSpatialForecastPath.referenceModulus line 37
  2. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialForecastPath.referenceModulus_pos line 40
  3. def OAI.Erdos3.VectorPolynomial.ActualFixedSpatialForecastPath.referencePolynomial line 48
  4. def OAI.Erdos3.VectorPolynomial.ActualFixedSpatialForecastPath.referenceInputLaw line 52
  5. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialForecastPath.reference_characteristic_decay line 63
  6. theorem OAI.Erdos3.boundedPrimes_log_prime_power_le_slicedTargetReal line 91
  7. theorem OAI.Erdos3.boundedPrimes_prime_slicedTargetReal line 96
  8. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialForecastPath.referenceModulus_eq_boundedPrimeProduct_slicedTargetReal line 131
  9. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialForecastPath.dvd_referenceModulus_of_le_bound_slicedTargetReal line 141
  10. theorem OAI.Erdos3.boundedPrimes_log_prime_power_le line 159
  11. theorem OAI.Erdos3.boundedPrimes_prime line 164
  12. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialForecastPath.referenceModulus_eq_boundedPrimeProduct line 199
  13. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialForecastPath.dvd_referenceModulus_of_le_bound line 209
  14. def OAI.Erdos3.VectorPolynomial.ActualFixedSpatialSlicedForecastPath.rawTarget line 261
  15. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialSlicedForecastPath.targetAt_eq_rawTarget line 273
  16. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialSlicedForecastPath.rawTarget_universal_approx line 281
  17. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialSlicedForecastPath.rawTarget_actualForecastData_approx line 342
  18. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialSlicedForecastPath.rawTarget_real line 411
  19. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialSlicedForecastPath.rawTarget_star line 418
  20. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialSlicedForecastPath.targetAt_real line 424
  21. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialSlicedForecastPath.targetAt_star line 430
  22. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialSlicedForecastPath.target_real line 436
  23. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialSlicedForecastPath.target_star line 441
  24. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialSlicedForecastPath.actualForecastData_target_real line 451
  25. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialSlicedForecastPath.actualForecastData_target_star line 457