OAI/Combinatorics/Sidorenko/Dilution.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SidorenkoCounterexample.FiniteLaw.diluted line 13
  2. lemma OAI.SidorenkoCounterexample.FiniteLaw.someFunction_injective line 18
  3. lemma OAI.SidorenkoCounterexample.FiniteLaw.exists_none_of_not_some line 22
  4. lemma OAI.SidorenkoCounterexample.FiniteLaw.diluted_independent_mean line 30
  5. def OAI.SidorenkoCounterexample.dilutedPairLaw line 57
  6. lemma OAI.SidorenkoCounterexample.dilutedPairLaw_zero line 61
  7. lemma OAI.SidorenkoCounterexample.coefficient_dilution_left line 67
  8. lemma OAI.SidorenkoCounterexample.coefficient_dilution_right line 80
  9. lemma OAI.SidorenkoCounterexample.exists_dilution_gap line 97
  10. def OAI.SidorenkoCounterexample.neighborHistogram line 127
  11. lemma OAI.SidorenkoCounterexample.histogram_weighted line 129
  12. structure OAI.SidorenkoCounterexample.VertexPairScores line 140
  13. def OAI.SidorenkoCounterexample.VertexPairScores.score line 144
  14. def OAI.SidorenkoCounterexample.roundScores line 146
  15. lemma OAI.SidorenkoCounterexample.roundScore_formula line 151
  16. lemma OAI.SidorenkoCounterexample.roundScore_loss line 168