OAI/Combinatorics/SquareDifference/MixedEnergy.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SquareDifference.directedCrossEdge line 10
  2. lemma OAI.SquareDifference.directedCrossEdge_injective line 16
  3. lemma OAI.SquareDifference.directedCrossEdge_noloop line 23
  4. lemma OAI.SquareDifference.directedCrossEdge_noopp line 29
  5. def OAI.SquareDifference.listKernel line 39
  6. lemma OAI.SquareDifference.copied_graph_count line 44
  7. lemma OAI.SquareDifference.centered_product_moment_bound line 81
  8. def OAI.SquareDifference.fourListsEquiv line 115
  9. lemma OAI.SquareDifference.expect_fourLists line 127
  10. lemma OAI.SquareDifference.list_four_cycle line 141
  11. lemma OAI.SquareDifference.square_delta_le line 182
  12. lemma OAI.SquareDifference.list_mixing line 192
  13. lemma OAI.SquareDifference.posSemidef_entrywise_pow line 254
  14. lemma OAI.SquareDifference.posSemidef_entrywise_exp line 261
  15. lemma OAI.SquareDifference.posSemidef_entrywise_prod line 292
  16. lemma OAI.SquareDifference.posSemidef_product_gap line 304
  17. lemma OAI.SquareDifference.posSemidef_equality line 336
  18. lemma OAI.SquareDifference.posSemidef_exp_agreement_gap line 342
  19. lemma OAI.SquareDifference.posSemidef_gram line 362
  20. def OAI.SquareDifference.indexCross line 371
  21. lemma OAI.SquareDifference.posSemidef_indexCross line 375
  22. lemma OAI.SquareDifference.indexCross_sub_scalar_one line 393
  23. lemma OAI.SquareDifference.exponential_index_matrix_lower line 410
  24. lemma OAI.SquareDifference.posSemidef_of_diagonal_dominance line 453
  25. lemma OAI.SquareDifference.matrix_gap_of_diagonal_dominance line 470
  26. lemma OAI.SquareDifference.matrix_lower_quadratic line 486