OAI/Combinatorics/TriangleRemoval/Spectral/MovingStarDegree.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SharpTerminalLeave.moving_abs_sub_bound line 12
  2. def OAI.SharpTerminalLeave.movingStarDegree line 15
  3. def OAI.SharpTerminalLeave.movingStarMean line 20
  4. def OAI.SharpTerminalLeave.movingStarLift line 25
  5. def OAI.SharpTerminalLeave.movingStarOtherMean line 28
  6. lemma OAI.SharpTerminalLeave.movingStarDegree_nonneg line 34
  7. lemma OAI.SharpTerminalLeave.movingStarMean_congr line 38
  8. lemma OAI.SharpTerminalLeave.movingStarMean_sub line 49
  9. lemma OAI.SharpTerminalLeave.movingStarMean_zero_degree line 56
  10. lemma OAI.SharpTerminalLeave.movingStarMean_bound line 61
  11. lemma OAI.SharpTerminalLeave.movingStarLift_bound line 81
  12. lemma OAI.SharpTerminalLeave.movingStarOtherMean_bound line 91
  13. lemma OAI.SharpTerminalLeave.movingStarMean_lift line 118
  14. theorem OAI.SharpTerminalLeave.movingStar_vertex_step_bound line 136
  15. def OAI.SharpTerminalLeave.movingStarVertices line 169
  16. theorem OAI.SharpTerminalLeave.movingStarVertices_bound line 177
  17. theorem OAI.SharpTerminalLeave.movingStar_trajectory_representation line 195
  18. theorem OAI.SharpTerminalLeave.movingStar_trajectory_bound line 213
  19. lemma OAI.SharpTerminalLeave.movingStar_incidence_swap line 232
  20. lemma OAI.SharpTerminalLeave.movingStarMean_mass line 242
  21. theorem OAI.SharpTerminalLeave.movingStar_energy_identity line 255
  22. lemma OAI.SharpTerminalLeave.movingStar_lift_sq_bound line 267
  23. theorem OAI.SharpTerminalLeave.movingStar_euler_energy_le line 286
  24. theorem OAI.SharpTerminalLeave.movingStar_euler_energy_subset_le line 315