OAI/Combinatorics/SquareDifference/MatrixBounds.lean

GitHub source file

54 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SquareDifference.weighted_matrix_lower_quadratic line 10
  2. lemma OAI.SquareDifference.marked_index_average line 23
  3. abbrev OAI.SquareDifference.WordVertex line 41
  4. abbrev OAI.SquareDifference.PositionPair line 43
  5. def OAI.SquareDifference.vertexSwap line 45
  6. def OAI.SquareDifference.reflect line 49
  7. def OAI.SquareDifference.cutPlus line 53
  8. instance OAI.SquareDifference.cutPlusDecidable line 56
  9. lemma OAI.SquareDifference.vertexSwap_involutive line 60
  10. lemma OAI.SquareDifference.reflect_involutive line 69
  11. lemma OAI.SquareDifference.reflect_vertexSwap line 78
  12. lemma OAI.SquareDifference.reflect_cutPlus line 85
  13. lemma OAI.SquareDifference.reflect_ne_self line 90
  14. lemma OAI.SquareDifference.swap_reverse_gap line 98
  15. lemma OAI.SquareDifference.vertexSwap_symm_apply line 104
  16. lemma OAI.SquareDifference.reflect_eq_positional line 109
  17. lemma OAI.SquareDifference.ordered_swap_injective line 121
  18. lemma OAI.SquareDifference.vertexSwap_ne_self line 138
  19. lemma OAI.SquareDifference.vertexSwap_generator_injective line 146
  20. def OAI.SquareDifference.interaction line 161
  21. lemma OAI.SquareDifference.interaction_nonneg line 166
  22. lemma OAI.SquareDifference.interaction_self line 172
  23. lemma OAI.SquareDifference.interaction_neighbour line 177
  24. lemma OAI.SquareDifference.interaction_eq_zero_of_not_neighbour line 194
  25. lemma OAI.SquareDifference.interaction_symm line 203
  26. lemma OAI.SquareDifference.interaction_reflect line 218
  27. lemma OAI.SquareDifference.cross_gap line 229
  28. abbrev OAI.SquareDifference.CutHalf line 253
  29. def OAI.SquareDifference.crossInteraction line 256
  30. lemma OAI.SquareDifference.crossInteraction_symmetric line 261
  31. lemma OAI.SquareDifference.crossInteraction_diagonal_lower line 273
  32. lemma OAI.SquareDifference.crossInteraction_generator_bound line 293
  33. lemma OAI.SquareDifference.crossInteraction_offdiag_bound line 323
  34. lemma OAI.SquareDifference.crossInteraction_diagonal_dominance line 352
  35. def OAI.SquareDifference.tupleH line 376
  36. def OAI.SquareDifference.tupleT line 378
  37. def OAI.SquareDifference.tupleBlocks line 380
  38. def OAI.SquareDifference.tupleDelta line 382
  39. def OAI.SquareDifference.tupleKappa line 384
  40. lemma OAI.SquareDifference.tupleDelta_pos line 386
  41. lemma OAI.SquareDifference.tupleDelta_le_one line 388
  42. lemma OAI.SquareDifference.tupleDelta_scale line 390
  43. lemma OAI.SquareDifference.tupleKappa_pos line 393
  44. lemma OAI.SquareDifference.cutPlus_reflect_iff_not line 397
  45. def OAI.SquareDifference.halfSumEquiv line 404
  46. lemma OAI.SquareDifference.card_cutHalf line 425
  47. def OAI.SquareDifference.addressEdge line 432
  48. lemma OAI.SquareDifference.addressEdge_irrefl line 436
  49. lemma OAI.SquareDifference.addressEdge_asymm line 444
  50. lemma OAI.SquareDifference.addressEdge_left_translate line 469
  51. lemma OAI.SquareDifference.addressEdge_mono_blocks line 474
  52. lemma OAI.SquareDifference.addressEdge_full_shift line 484
  53. lemma OAI.SquareDifference.crossInteraction_gap line 489
  54. lemma OAI.SquareDifference.marked_interaction_index_average line 497