OAI/NumberTheory/Jacobsthal/Estimates/RegularImplicitArc.lean

GitHub source file

74 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos970.ErdosLatticeChain.vectorLength line 13
  2. def OAI.Erdos970.ErdosLatticeChain.totalLength line 15
  3. def OAI.Erdos970.ErdosLatticeChain.shortVectors line 17
  4. def OAI.Erdos970.ErdosLatticeChain.longVectors line 20
  5. def OAI.Erdos970.ErdosLatticeChain.shortSquareEmbedding line 23
  6. theorem OAI.Erdos970.ErdosLatticeChain.short_card_le_square line 41
  7. theorem OAI.Erdos970.ErdosLatticeChain.short_long_card line 46
  8. theorem OAI.Erdos970.ErdosLatticeChain.long_card_mul_le_length line 51
  9. theorem OAI.Erdos970.ErdosLatticeChain.card_le_square_add_div line 63
  10. theorem OAI.Erdos970.ErdosLatticeChain.consecutive_sum line 88
  11. def OAI.Erdos970.ErdosLatticeChain.coordinateVariation line 95
  12. theorem OAI.Erdos970.ErdosLatticeChain.variation_of_monotone line 98
  13. theorem OAI.Erdos970.ErdosLatticeChain.variation_of_antitone line 109
  14. theorem OAI.Erdos970.ErdosLatticeChain.variation_le_box line 124
  15. theorem OAI.Erdos970.ErdosLatticeChain.vector_card_bound line 140
  16. theorem OAI.Erdos970.ErdosLatticeChain.vector_card_bound_actual line 172
  17. def OAI.Erdos970.ErdosLatticeChain.earlierIndex line 184
  18. def OAI.Erdos970.ErdosLatticeChain.laterIndex line 185
  19. theorem OAI.Erdos970.ErdosLatticeChain.earlier_lt_later line 187
  20. def OAI.Erdos970.ErdosLatticeChain.consecutiveDifference line 190
  21. def OAI.Erdos970.ErdosLatticeChain.natIncrement line 194
  22. def OAI.Erdos970.ErdosLatticeChain.incrementVectors line 197
  23. theorem OAI.Erdos970.ErdosLatticeChain.int_eq_of_natAbs_eq_nonneg line 200
  24. theorem OAI.Erdos970.ErdosLatticeChain.int_eq_of_natAbs_eq_nonpos line 205
  25. theorem OAI.Erdos970.ErdosLatticeChain.natIncrement_injective line 212
  26. theorem OAI.Erdos970.ErdosLatticeChain.incrementVectors_card line 233
  27. theorem OAI.Erdos970.ErdosLatticeChain.incrementVectors_length line 237
  28. theorem OAI.Erdos970.ErdosLatticeChain.consecutive_first_pos line 249
  29. def OAI.Erdos970.ErdosImplicitCurvature.inflectionPolynomial line 260
  30. theorem OAI.Erdos970.ErdosImplicitCurvature.peval_inflectionPolynomial line 265
  31. theorem OAI.Erdos970.ErdosImplicitCurvature.curvature_scalar_identity line 272
  32. theorem OAI.Erdos970.ErdosImplicitCurvature.implicit_derivatives line 282
  33. theorem OAI.Erdos970.ErdosImplicitCurvature.implicit_second_derivative line 293
  34. theorem OAI.Erdos970.ErdosImplicitCurvature.curvature_zero_iff line 300
  35. theorem OAI.Erdos970.ErdosImplicitCurvature.curvature_ne_zero_iff line 308
  36. theorem OAI.Erdos970.ErdosLatticeChain.lattice_chain_bound line 321
  37. def OAI.Erdos970.ErdosLatticeChain.chainPoints line 351
  38. theorem OAI.Erdos970.ErdosLatticeChain.lattice_chain_card_bound line 354
  39. def OAI.Erdos970.ErdosLatticeChain.consecutiveSlope line 367
  40. theorem OAI.Erdos970.ErdosLatticeChain.difference_injective_of_slope line 370
  41. theorem OAI.Erdos970.ErdosLatticeChain.lattice_chain_strict_slopes line 377
  42. theorem OAI.Erdos970.ErdosConvexGraph.convex_secants_lt line 398
  43. theorem OAI.Erdos970.ErdosConvexGraph.concave_secants_lt line 408
  44. def OAI.Erdos970.ErdosConvexGraph.secantSlopes line 418
  45. theorem OAI.Erdos970.ErdosConvexGraph.consecutive_intervals_ordered line 422
  46. theorem OAI.Erdos970.ErdosConvexGraph.convex_secantSlopes_strictMono line 425
  47. theorem OAI.Erdos970.ErdosConvexGraph.concave_secantSlopes_strictAnti line 433
  48. theorem OAI.Erdos970.ErdosConvexGraph.consecutiveSlope_eq_secantSlopes line 441
  49. def OAI.Erdos970.ErdosConvexGraph.OnGraph line 455
  50. def OAI.Erdos970.ErdosConvexGraph.InSquare line 458
  51. theorem OAI.Erdos970.ErdosConvexGraph.graph_chain_y_monotone line 461
  52. theorem OAI.Erdos970.ErdosConvexGraph.graph_chain_slopes line 479
  53. theorem OAI.Erdos970.ErdosConvexGraph.graph_chain_bound line 493
  54. theorem OAI.Erdos970.ErdosConvexGraph.graph_chain_card_bound line 505
  55. def OAI.Erdos970.ErdosConvexGraph.graphAbscissae line 520
  56. def OAI.Erdos970.ErdosConvexGraph.graphEnumeration line 522
  57. theorem OAI.Erdos970.ErdosConvexGraph.onGraph_fst_injective line 527
  58. theorem OAI.Erdos970.ErdosConvexGraph.graphAbscissae_card line 533
  59. theorem OAI.Erdos970.ErdosConvexGraph.graphEnumeration_mem line 539
  60. theorem OAI.Erdos970.ErdosConvexGraph.graphEnumeration_strictMono line 553
  61. theorem OAI.Erdos970.ErdosConvexGraph.finite_graph_set_bound line 557
  62. def OAI.Erdos970.ErdosConvexGraph.graphLatticePoints line 575
  63. theorem OAI.Erdos970.ErdosConvexGraph.mem_graphLatticePoints line 578
  64. theorem OAI.Erdos970.ErdosConvexGraph.graph_arc_lattice_bound line 583
  65. theorem OAI.Erdos970.ErdosConvexGraph.closed_graph_arc_bound line 591
  66. theorem OAI.Erdos970.ErdosConvexGraph.open_graph_arc_bound line 597
  67. def OAI.Erdos970.ErdosImplicitCurvature.curvatureRatio line 609
  68. theorem OAI.Erdos970.ErdosImplicitCurvature.strictConvexOn_of_curvatureRatio line 612
  69. theorem OAI.Erdos970.ErdosImplicitCurvature.strictConcaveOn_of_curvatureRatio line 624
  70. theorem OAI.Erdos970.ErdosImplicitCurvature.implicit_graph_lattice_bound line 636
  71. theorem OAI.Erdos970.ErdosImplicitCurvature.continuous_nonzero_fixed_sign line 654
  72. theorem OAI.Erdos970.ErdosImplicitCurvature.regular_implicit_monotone line 672
  73. theorem OAI.Erdos970.ErdosImplicitCurvature.regular_implicit_convex_or_concave line 692
  74. theorem OAI.Erdos970.ErdosImplicitCurvature.regular_implicit_arc_lattice_bound line 714