OAI/Combinatorics/SquareDifference/TupleEnergy.lean

GitHub source file

63 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SquareDifference.indexEnergy line 10
  2. def OAI.SquareDifference.indexWeight line 13
  3. lemma OAI.SquareDifference.indexEnergy_nonneg line 16
  4. lemma OAI.SquareDifference.one_le_indexWeight line 23
  5. lemma OAI.SquareDifference.indexCross_equiv line 27
  6. lemma OAI.SquareDifference.indexCross_transpose line 35
  7. lemma OAI.SquareDifference.indexCross_sum line 42
  8. lemma OAI.SquareDifference.indexWeight_factor line 54
  9. lemma OAI.SquareDifference.expect_sum_function line 74
  10. lemma OAI.SquareDifference.reflected_index_weight_lower line 85
  11. lemma OAI.SquareDifference.card_positionPair line 107
  12. lemma OAI.SquareDifference.interaction_row_sum line 110
  13. lemma OAI.SquareDifference.interaction_row_sum_le line 122
  14. abbrev OAI.SquareDifference.TupleVertex line 136
  15. abbrev OAI.SquareDifference.TupleAddress line 138
  16. def OAI.SquareDifference.tupleR line 141
  17. abbrev OAI.SquareDifference.TupleListIndex line 143
  18. abbrev OAI.SquareDifference.TupleListEntry line 145
  19. def OAI.SquareDifference.tupleProjection line 147
  20. def OAI.SquareDifference.tupleCycle line 150
  21. def OAI.SquareDifference.cycleVertex line 152
  22. lemma OAI.SquareDifference.tupleCycle_ne_one line 154
  23. lemma OAI.SquareDifference.tupleCycle_sq_ne_one line 156
  24. lemma OAI.SquareDifference.tupleCycle_pow line 158
  25. lemma OAI.SquareDifference.card_tupleVertex line 166
  26. lemma OAI.SquareDifference.tupleR_pos line 169
  27. instance OAI.SquareDifference.tupleListIndexNonempty line 171
  28. lemma OAI.SquareDifference.card_cleanBlocks line 174
  29. lemma OAI.SquareDifference.card_tupleAddress line 182
  30. def OAI.SquareDifference.tupleListEdges line 186
  31. lemma OAI.SquareDifference.tupleListEdges_no_loop line 192
  32. lemma OAI.SquareDifference.tupleListEdges_no_opp line 203
  33. lemma OAI.SquareDifference.cycle_addressEdge line 216
  34. lemma OAI.SquareDifference.cycle_listEdge line 228
  35. lemma OAI.SquareDifference.expect_precompose line 236
  36. lemma OAI.SquareDifference.indexWeight_equiv line 246
  37. lemma OAI.SquareDifference.marked_interaction_weight_lower line 251
  38. def OAI.SquareDifference.tupleWeight line 283
  39. def OAI.SquareDifference.tupleValidity line 286
  40. def OAI.SquareDifference.tupleOutput line 290
  41. def OAI.SquareDifference.tupleComponent line 294
  42. def OAI.SquareDifference.tupleCutForm line 299
  43. lemma OAI.SquareDifference.tupleValidity_nonneg line 303
  44. lemma OAI.SquareDifference.tupleValidity_le_one line 308
  45. lemma OAI.SquareDifference.tupleProjection_reflect line 313
  46. lemma OAI.SquareDifference.tuple_marked_lower line 320
  47. lemma OAI.SquareDifference.indexEnergy_le_of_row line 347
  48. def OAI.SquareDifference.tupleWeightBound line 364
  49. lemma OAI.SquareDifference.tupleWeightBound_pos line 368
  50. lemma OAI.SquareDifference.tupleWeight_one_le line 370
  51. lemma OAI.SquareDifference.tupleWeight_le line 374
  52. lemma OAI.SquareDifference.tupleComponent_nonneg line 388
  53. lemma OAI.SquareDifference.tupleComponent_mass_le line 398
  54. lemma OAI.SquareDifference.squareIndicator_ne_zero_iff line 416
  55. lemma OAI.SquareDifference.tupleValidity_edge line 422
  56. lemma OAI.SquareDifference.tuple_cycle_support line 428
  57. lemma OAI.SquareDifference.cycleVertex_period line 436
  58. lemma OAI.SquareDifference.tupleWeight_empty line 440
  59. lemma OAI.SquareDifference.tuple_leading_mass line 443
  60. def OAI.SquareDifference.reflectEquiv line 453
  61. lemma OAI.SquareDifference.interaction_zero_of_unmarked_word line 457
  62. lemma OAI.SquareDifference.unmarked_crossInteraction_zero line 468
  63. lemma OAI.SquareDifference.unmarked_weight_factor line 484