OAI/Combinatorics/TriangleRemoval/Process/TriangleDegreeMean.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SharpTerminalLeave.triangles_delete_eq_sdiff_hitting line 12
  2. lemma OAI.SharpTerminalLeave.triangle_edge_inter_card_le_one line 33
  3. lemma OAI.SharpTerminalLeave.triangle_incidence_swap line 47
  4. lemma OAI.SharpTerminalLeave.triangle_degree_sum line 68
  5. lemma OAI.SharpTerminalLeave.triangle_incidence_sum_on line 81
  6. lemma OAI.SharpTerminalLeave.triangle_hit_multiplicity line 95
  7. theorem OAI.SharpTerminalLeave.triangle_hitting_card_exact line 124
  8. theorem OAI.SharpTerminalLeave.triangle_count_delete line 149
  9. theorem OAI.SharpTerminalLeave.step_mean_triangle_count line 158
  10. def OAI.SharpTerminalLeave.triangleDegreeMean line 184
  11. def OAI.SharpTerminalLeave.triangleDegreeVariance line 187
  12. lemma OAI.SharpTerminalLeave.triangleDegreeVariance_nonneg line 190
  13. lemma OAI.SharpTerminalLeave.triangleDegreeMean_mass line 193
  14. theorem OAI.SharpTerminalLeave.triangle_degree_second_moment line 199
  15. lemma OAI.SharpTerminalLeave.graph_nonempty_of_triangles line 220
  16. theorem OAI.SharpTerminalLeave.step_mean_triangle_count_centered line 227
  17. lemma OAI.SharpTerminalLeave.triangle_degree_variance_shift line 240
  18. lemma OAI.SharpTerminalLeave.triangle_degree_variance_le line 258