OAI/NumberTheory/Jacobsthal/Estimates/RealCriticalPoints.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos970.ErdosCriticalGeometry.beval_nested line 14
  2. def OAI.Erdos970.ErdosCriticalGeometry.intersectionPoints line 17
  3. def OAI.Erdos970.ErdosCriticalGeometry.intersectionAbscissae line 20
  4. theorem OAI.Erdos970.ErdosCriticalGeometry.intersectionPoints_eq_nested line 22
  5. theorem OAI.Erdos970.ErdosCriticalGeometry.nonlinear_fibers_nonzero line 27
  6. theorem OAI.Erdos970.ErdosCriticalGeometry.nonlinear_resultant_nonzero line 32
  7. theorem OAI.Erdos970.ErdosCriticalGeometry.mv_resultant_degree_le line 42
  8. theorem OAI.Erdos970.ErdosCriticalGeometry.irreducible_intersection_bound line 55
  9. theorem OAI.Erdos970.ErdosCriticalGeometry.irreducible_abscissa_bound line 68
  10. def OAI.Erdos970.ErdosDivisibleInflection.affineLine line 99
  11. def OAI.Erdos970.ErdosDivisibleInflection.affineInner line 102
  12. theorem OAI.Erdos970.ErdosDivisibleInflection.nested_affineLine line 105
  13. theorem OAI.Erdos970.ErdosDivisibleInflection.eval_affine_substitution line 109
  14. theorem OAI.Erdos970.ErdosDivisibleInflection.affine_interval_factor line 117
  15. theorem OAI.Erdos970.ErdosDivisibleInflection.affineLine_not_unit line 136
  16. theorem OAI.Erdos970.ErdosDivisibleInflection.affineLine_degree_le line 143
  17. theorem OAI.Erdos970.ErdosDivisibleInflection.no_affine_interval line 157
  18. def OAI.Erdos970.ErdosCriticalGeometry.criticalPoints line 177
  19. def OAI.Erdos970.ErdosCriticalGeometry.criticalAbscissae line 180
  20. theorem OAI.Erdos970.ErdosCriticalGeometry.mem_criticalPoints line 182
  21. theorem OAI.Erdos970.ErdosCriticalGeometry.partial_intersection_bound line 194
  22. theorem OAI.Erdos970.ErdosCriticalGeometry.partial_abscissa_bound line 206
  23. theorem OAI.Erdos970.ErdosCriticalGeometry.critical_points_bound line 218
  24. theorem OAI.Erdos970.ErdosCriticalGeometry.critical_abscissae_bound line 228
  25. def OAI.Erdos970.ErdosCriticalGeometry.inflection line 248
  26. theorem OAI.Erdos970.ErdosCriticalGeometry.inflection_degree_le line 254
  27. theorem OAI.Erdos970.ErdosCriticalGeometry.inflection_intersection_bounds line 276
  28. theorem OAI.Erdos970.ErdosCriticalGeometry.inflection_zero_divisible line 292
  29. theorem OAI.Erdos970.ErdosCriticalGeometry.inflection_alternative line 296
  30. def OAI.Erdos970.ErdosCriticalGeometry.exceptionalPoints line 306
  31. def OAI.Erdos970.ErdosCriticalGeometry.exceptionalAbscissae line 308
  32. theorem OAI.Erdos970.ErdosCriticalGeometry.exceptional_points_bound line 310
  33. theorem OAI.Erdos970.ErdosCriticalGeometry.exceptional_abscissae_bound line 320
  34. def OAI.Erdos970.ErdosCriticalGeometry.complexify line 340
  35. theorem OAI.Erdos970.ErdosCriticalGeometry.complexify_totalDegree line 342
  36. theorem OAI.Erdos970.ErdosCriticalGeometry.complexify_partial line 347
  37. theorem OAI.Erdos970.ErdosCriticalGeometry.complexify_eval line 351
  38. def OAI.Erdos970.ErdosCriticalGeometry.realCriticalPoints line 360
  39. def OAI.Erdos970.ErdosCriticalGeometry.realCriticalAbscissae line 365
  40. def OAI.Erdos970.ErdosCriticalGeometry.complexPoint line 367
  41. theorem OAI.Erdos970.ErdosCriticalGeometry.complexPoint_injective line 369
  42. theorem OAI.Erdos970.ErdosCriticalGeometry.real_critical_iff line 375
  43. theorem OAI.Erdos970.ErdosCriticalGeometry.real_critical_points_bound line 381
  44. theorem OAI.Erdos970.ErdosCriticalGeometry.real_critical_abscissae_bound line 398