OAI/Combinatorics/Sidorenko/Monomials.lean

GitHub source file

52 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SidorenkoCounterexample.starSign line 15
  2. theorem OAI.SidorenkoCounterexample.starSign_abs_le line 20
  3. theorem OAI.SidorenkoCounterexample.starSign_update_bound line 25
  4. theorem OAI.SidorenkoCounterexample.testedStar_update_bound line 40
  5. theorem OAI.SidorenkoCounterexample.testedStar_mean_bound line 57
  6. def OAI.SidorenkoCounterexample.pairLeft line 99
  7. def OAI.SidorenkoCounterexample.pairRight line 100
  8. theorem OAI.SidorenkoCounterexample.pair_endpoints line 101
  9. theorem OAI.SidorenkoCounterexample.pair_endpoints_ne line 102
  10. def OAI.SidorenkoCounterexample.pairOther line 104
  11. theorem OAI.SidorenkoCounterexample.pairOther_ne line 106
  12. theorem OAI.SidorenkoCounterexample.pair_vertices_other line 112
  13. def OAI.SidorenkoCounterexample.selectedIncident line 123
  14. theorem OAI.SidorenkoCounterexample.selectedIncident_card line 126
  15. theorem OAI.SidorenkoCounterexample.pairOther_injective line 131
  16. def OAI.SidorenkoCounterexample.pairSign line 142
  17. theorem OAI.SidorenkoCounterexample.pairSign_abs_le line 145
  18. theorem OAI.SidorenkoCounterexample.determinant_difference_even line 152
  19. theorem OAI.SidorenkoCounterexample.pairSign_other line 157
  20. theorem OAI.SidorenkoCounterexample.pairSign_product_abs_le line 169
  21. def OAI.SidorenkoCounterexample.nonincidentProduct line 188
  22. theorem OAI.SidorenkoCounterexample.nonincidentProduct_abs_le line 192
  23. theorem OAI.SidorenkoCounterexample.nonincidentProduct_update line 196
  24. theorem OAI.SidorenkoCounterexample.pairSign_product_split line 212
  25. theorem OAI.SidorenkoCounterexample.pairSign_moment_bound line 227
  26. theorem OAI.SidorenkoCounterexample.minorBadBound_tendsto line 246
  27. theorem OAI.SidorenkoCounterexample.sign_moment_dimension line 263
  28. theorem OAI.SidorenkoCounterexample.pairSign_moment_tendsto line 270
  29. theorem OAI.SidorenkoCounterexample.abs_prod_le_pow line 307
  30. theorem OAI.SidorenkoCounterexample.product_difference_bound line 312
  31. theorem OAI.SidorenkoCounterexample.product_difference_unit line 336
  32. theorem OAI.SidorenkoCounterexample.uniformMean_finset_sum line 344
  33. theorem OAI.SidorenkoCounterexample.uniformMean_pi_product line 349
  34. theorem OAI.SidorenkoCounterexample.uniformMean_point_difference line 370
  35. def OAI.SidorenkoCounterexample.pairSingular line 385
  36. theorem OAI.SidorenkoCounterexample.pairSingular_nonneg line 389
  37. theorem OAI.SidorenkoCounterexample.pairSingular_mean line 392
  38. def OAI.SidorenkoCounterexample.fullTransverse line 399
  39. theorem OAI.SidorenkoCounterexample.nonTransverse_pointwise line 403
  40. theorem OAI.SidorenkoCounterexample.nonTransverse_mean line 414
  41. def OAI.SidorenkoCounterexample.pairBool line 423
  42. def OAI.SidorenkoCounterexample.boolSign line 426
  43. theorem OAI.SidorenkoCounterexample.boolSign_abs line 427
  44. theorem OAI.SidorenkoCounterexample.boolSign_sq line 428
  45. theorem OAI.SidorenkoCounterexample.pairBool_error line 430
  46. theorem OAI.SidorenkoCounterexample.pairBool_moment_error line 442
  47. theorem OAI.SidorenkoCounterexample.pairBool_moment_tendsto line 459
  48. def OAI.SidorenkoCounterexample.fullGraphIntersection line 486
  49. def OAI.SidorenkoCounterexample.matrixLagrangian line 505
  50. theorem OAI.SidorenkoCounterexample.matrixLagrangian_injective line 509
  51. theorem OAI.SidorenkoCounterexample.matrixLagrangian_pair_rank line 515
  52. theorem OAI.SidorenkoCounterexample.matrixLagrangian_pair_zero line 526