OAI/Combinatorics/MatchingCount/Graphs/Density.lean

GitHub source file

52 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatchingFPRAS.Replica.density line 13
  2. def OAI.MatchingFPRAS.Replica.dot line 15
  3. def OAI.MatchingFPRAS.Replica.average line 18
  4. lemma OAI.MatchingFPRAS.Replica.average_apply line 25
  5. lemma OAI.MatchingFPRAS.Replica.average_idem line 29
  6. lemma OAI.MatchingFPRAS.Replica.average_comm line 36
  7. def OAI.MatchingFPRAS.Replica.swapDraw line 51
  8. lemma OAI.MatchingFPRAS.Replica.density_swap line 58
  9. lemma OAI.MatchingFPRAS.Replica.average_adjoint line 73
  10. lemma OAI.MatchingFPRAS.Replica.dot_comm line 91
  11. lemma OAI.MatchingFPRAS.Replica.dot_zero_left line 94
  12. lemma OAI.MatchingFPRAS.Replica.dot_zero_right line 96
  13. lemma OAI.MatchingFPRAS.Replica.dot_add_left line 98
  14. lemma OAI.MatchingFPRAS.Replica.dot_add_right line 102
  15. lemma OAI.MatchingFPRAS.Replica.dot_sub_left line 106
  16. lemma OAI.MatchingFPRAS.Replica.dot_sub_right line 110
  17. lemma OAI.MatchingFPRAS.Replica.dot_const_left line 114
  18. lemma OAI.MatchingFPRAS.Replica.dot_nonneg line 119
  19. structure OAI.MatchingFPRAS.Replica.Projection line 125
  20. def OAI.MatchingFPRAS.Replica.Projection.identity line 134
  21. def OAI.MatchingFPRAS.Replica.Projection.complement line 139
  22. def OAI.MatchingFPRAS.Replica.Projection.comp line 149
  23. lemma OAI.MatchingFPRAS.Replica.Projection.dot_image line 159
  24. def OAI.MatchingFPRAS.Replica.avgProjection line 165
  25. def OAI.MatchingFPRAS.Replica.avgList line 170
  26. lemma OAI.MatchingFPRAS.Replica.avgList_nil line 175
  27. lemma OAI.MatchingFPRAS.Replica.avgList_cons line 178
  28. lemma OAI.MatchingFPRAS.Replica.average_comm_list line 182
  29. lemma OAI.MatchingFPRAS.Replica.avgList_idem line 190
  30. lemma OAI.MatchingFPRAS.Replica.avgList_adjoint line 198
  31. def OAI.MatchingFPRAS.Replica.listProjection line 205
  32. lemma OAI.MatchingFPRAS.Replica.average_list_mem line 211
  33. def OAI.MatchingFPRAS.Replica.outside line 231
  34. def OAI.MatchingFPRAS.Replica.pairCondition line 234
  35. def OAI.MatchingFPRAS.Replica.residual line 237
  36. lemma OAI.MatchingFPRAS.Replica.residual_apply line 242
  37. lemma OAI.MatchingFPRAS.Replica.residual_formula line 247
  38. lemma OAI.MatchingFPRAS.Replica.average_condition_comm line 253
  39. lemma OAI.MatchingFPRAS.Replica.average_residual_comm line 257
  40. lemma OAI.MatchingFPRAS.Replica.residual_center_x line 262
  41. lemma OAI.MatchingFPRAS.Replica.residual_center_y line 266
  42. lemma OAI.MatchingFPRAS.Replica.condition_invariant line 273
  43. lemma OAI.MatchingFPRAS.Replica.residual_invariant line 279
  44. lemma OAI.MatchingFPRAS.Replica.residual_projection line 286
  45. lemma OAI.MatchingFPRAS.Replica.residual_dot line 307
  46. lemma OAI.MatchingFPRAS.Replica.centered_invariant_orthogonal line 314
  47. lemma OAI.MatchingFPRAS.Replica.residual_orthogonal line 318
  48. lemma OAI.MatchingFPRAS.Replica.average_one line 336
  49. lemma OAI.MatchingFPRAS.Replica.residual_mean_zero line 340
  50. lemma OAI.MatchingFPRAS.Replica.dot_sum_right line 356
  51. lemma OAI.MatchingFPRAS.Replica.dot_sum_left line 362
  52. theorem OAI.MatchingFPRAS.Replica.residual_sum line 374