OAI/Combinatorics/Progressions/Dynamics/PreparedComparisonPrecisionLogBudget.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.VectorPolynomial.modularRankChargeFactor_le_preparedComparisonPower line 10
  2. theorem OAI.Erdos3.VectorPolynomial.preparedComparisonSourcePolynomial_le_square line 45
  3. theorem OAI.Erdos3.VectorPolynomial.preparedComparisonSmoothPolynomial_le_six line 50
  4. theorem OAI.Erdos3.VectorPolynomial.preparedComparisonGridPolynomial_le_power line 60
  5. theorem OAI.Erdos3.VectorPolynomial.forecastComparisonMeshPolynomial_le_power line 93
  6. theorem OAI.Erdos3.VectorPolynomial.preparedComparisonFloorPolynomial_le_power line 128
  7. def OAI.Erdos3.VectorPolynomial.preparedComparisonPrecisionPolynomial line 166
  8. theorem OAI.Erdos3.VectorPolynomial.preparedComparisonPrecisionPolynomial_nonneg line 170
  9. theorem OAI.Erdos3.VectorPolynomial.preparedComparisonPrecisionFloor_bounds line 186
  10. theorem OAI.Erdos3.VectorPolynomial.preparedComparisonPrecisionFloor_of_exp_bounds line 231
  11. theorem OAI.Erdos3.VectorPolynomial.preparedComparisonPrecisionFloor_power_bounds line 258
  12. theorem OAI.Erdos3.VectorPolynomial.preparedComparisonPrecisionFloor_of_power_bounds line 281
  13. theorem OAI.Erdos3.VectorPolynomial.preparedSlicedForecastComparisonFloorLog_le_power line 316
  14. theorem OAI.Erdos3.VectorPolynomial.preparedSlicedForecastJointGridAmbientLog_le_power line 347
  15. theorem OAI.Erdos3.VectorPolynomial.preparedComparisonPrecisionLog_le_polynomial line 397
  16. theorem OAI.Erdos3.VectorPolynomial.preparedComparisonPrecisionLog_le_power line 433