OAI/Combinatorics/Sidorenko/Symmetrization.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.SidorenkoCounterexample.OrientedKernel line 11
  2. lemma OAI.SidorenkoCounterexample.exists_oriented_kernel line 25
  3. lemma OAI.SidorenkoCounterexample.four_means_factor line 71
  4. def OAI.SidorenkoCounterexample.crossedKernel line 77
  5. lemma OAI.SidorenkoCounterexample.crossedKernel_symm line 79
  6. lemma OAI.SidorenkoCounterexample.crossedKernel_nonneg line 81
  7. lemma OAI.SidorenkoCounterexample.crossedKernel_mean line 83
  8. lemma OAI.SidorenkoCounterexample.crossedKernel_moment line 90
  9. lemma OAI.SidorenkoCounterexample.kernelMean_div line 99
  10. lemma OAI.SidorenkoCounterexample.bipartiteMoment_div line 102
  11. structure OAI.SidorenkoCounterexample.SymmetricCounterKernel line 109
  12. lemma OAI.SidorenkoCounterexample.exists_symmetric_kernel line 121
  13. lemma OAI.SidorenkoCounterexample.FiniteLaw.independent_mean_sum line 159
  14. lemma OAI.SidorenkoCounterexample.FiniteLaw.independent_mean_injective line 173
  15. def OAI.SidorenkoCounterexample.FiniteLaw.bind line 185
  16. lemma OAI.SidorenkoCounterexample.FiniteLaw.mean_bind line 189
  17. lemma OAI.SidorenkoCounterexample.FiniteLaw.mean_pow_le line 193
  18. lemma OAI.SidorenkoCounterexample.FiniteLaw.exists_lt_of_mean_lt line 197
  19. def OAI.SidorenkoCounterexample.edgeIndicator line 214
  20. lemma OAI.SidorenkoCounterexample.edgeIndicator_nonneg line 215
  21. lemma OAI.SidorenkoCounterexample.edgeIndicator_le_one line 217
  22. lemma OAI.SidorenkoCounterexample.edgeIndicator_symm line 219
  23. lemma OAI.SidorenkoCounterexample.mem_faces_iff line 221
  24. lemma OAI.SidorenkoCounterexample.hom_iff_corners line 230
  25. def OAI.SidorenkoCounterexample.homIndicator line 249
  26. lemma OAI.SidorenkoCounterexample.homIndicator_eq line 251
  27. lemma OAI.SidorenkoCounterexample.homIndicator_nonneg line 254
  28. lemma OAI.SidorenkoCounterexample.homIndicator_le_one line 256
  29. lemma OAI.SidorenkoCounterexample.homDensity_eq_mean line 258
  30. lemma OAI.SidorenkoCounterexample.edgeDensity_eq_mean line 264
  31. lemma OAI.SidorenkoCounterexample.homDensity_nonneg line 276
  32. lemma OAI.SidorenkoCounterexample.edgeDensity_nonneg line 278
  33. lemma OAI.SidorenkoCounterexample.edgeDensity_eq_zero_of_edgeless line 280
  34. lemma OAI.SidorenkoCounterexample.sourceMoment_eq_bipartite line 283