OAI/NumberTheory/PiExponent/Analysis/AnalyticCollision.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PiExponent.AnalyticCollision.exponentialMonomial line 10
  2. theorem OAI.PiExponent.AnalyticCollision.differentiable_exponentialMonomial line 13
  3. theorem OAI.PiExponent.AnalyticCollision.norm_exponentialMonomial_le line 18
  4. def OAI.PiExponent.AnalyticCollision.normalizedTaylorCoeff line 31
  5. theorem OAI.PiExponent.AnalyticCollision.norm_normalizedTaylorCoeff_le line 34
  6. theorem OAI.PiExponent.AnalyticCollision.hasSum_normalizedTaylorCoeff line 50
  7. theorem OAI.PiExponent.AnalyticCollision.coefficient_det_eq_zero_of_collision line 62
  8. theorem OAI.PiExponent.AnalyticCollision.norm_det_le_factorial_mul_pow line 69
  9. def OAI.PiExponent.AnalyticCollision.rowTest line 88
  10. theorem OAI.PiExponent.AnalyticCollision.norm_rowTest_le line 91
  11. theorem OAI.PiExponent.AnalyticCollision.norm_shifted_log_div_le_half line 108
  12. theorem OAI.PiExponent.AnalyticCollision.norm_rowTest_shifted_power_le line 117
  13. theorem OAI.PiExponent.AnalyticCollision.period_center_radius_bound line 127
  14. theorem OAI.PiExponent.AnalyticCollision.norm_exponentialMonomial_le_exp_budget line 140