OAI/Combinatorics/Chromatic/Walls/StationaryIntegerSequences.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ElementaryPositivity.TriangularDynamics.period_total_nonpos line 9
  2. lemma OAI.ElementaryPositivity.TriangularDynamics.monotone_int_stabilizes line 28
  3. lemma OAI.ElementaryPositivity.TriangularDynamics.finite_coordinates_stabilize line 38
  4. lemma OAI.ElementaryPositivity.TriangularDynamics.nonnegative_affine_slope line 57
  5. lemma OAI.ElementaryPositivity.TriangularDynamics.concave_nonpositive_zero line 71
  6. abbrev OAI.ElementaryPositivity.TriangularDynamics.Vertex line 110
  7. abbrev OAI.ElementaryPositivity.TriangularDynamics.Lattice line 111
  8. def OAI.ElementaryPositivity.TriangularDynamics.anchor line 113
  9. def OAI.ElementaryPositivity.TriangularDynamics.bridge line 114
  10. def OAI.ElementaryPositivity.TriangularDynamics.delta line 116
  11. def OAI.ElementaryPositivity.TriangularDynamics.eventRoot line 119
  12. def OAI.ElementaryPositivity.TriangularDynamics.levelTotal line 122
  13. def OAI.ElementaryPositivity.TriangularDynamics.cutContains line 132
  14. instance OAI.ElementaryPositivity.TriangularDynamics.cutContains_decidable line 136
  15. def OAI.ElementaryPositivity.TriangularDynamics.cutPrefix line 140
  16. lemma OAI.ElementaryPositivity.TriangularDynamics.cutPrefix_single line 150
  17. lemma OAI.ElementaryPositivity.TriangularDynamics.levelTotal_anchor line 160
  18. lemma OAI.ElementaryPositivity.TriangularDynamics.levelTotal_bridge line 163
  19. lemma OAI.ElementaryPositivity.TriangularDynamics.total_levels line 173
  20. lemma OAI.ElementaryPositivity.TriangularDynamics.eventRoot_bridge line 180
  21. lemma OAI.ElementaryPositivity.TriangularDynamics.cutPrefix_eventRoot line 184
  22. lemma OAI.ElementaryPositivity.TriangularDynamics.levelTotal_eventRoot line 193
  23. def OAI.ElementaryPositivity.TriangularDynamics.periodFunctional line 198
  24. lemma OAI.ElementaryPositivity.TriangularDynamics.periodFunctional_eventRoot line 201
  25. def OAI.ElementaryPositivity.TriangularDynamics.rotate line 209
  26. def OAI.ElementaryPositivity.TriangularDynamics.period line 212
  27. def OAI.ElementaryPositivity.TriangularDynamics.history line 215
  28. lemma OAI.ElementaryPositivity.TriangularDynamics.rotate_bridge_mono line 220
  29. lemma OAI.ElementaryPositivity.TriangularDynamics.period_bridge_mono line 227
  30. lemma OAI.ElementaryPositivity.TriangularDynamics.periodFunctional_rotate line 234
  31. lemma OAI.ElementaryPositivity.TriangularDynamics.periodFunctional_period line 239
  32. lemma OAI.ElementaryPositivity.TriangularDynamics.history_bridge_mono line 249
  33. lemma OAI.ElementaryPositivity.TriangularDynamics.history_total_mono line 255
  34. def OAI.ElementaryPositivity.TriangularDynamics.cutDeficit line 264
  35. lemma OAI.ElementaryPositivity.TriangularDynamics.history_deficit_step line 267
  36. lemma OAI.ElementaryPositivity.TriangularDynamics.history_total_nonpos line 278
  37. lemma OAI.ElementaryPositivity.TriangularDynamics.history_bridge_stabilizes line 285