OAI/Combinatorics/Sidorenko/Pinning.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SidorenkoCounterexample.exists_positive_perturbation line 13
  2. lemma OAI.SidorenkoCounterexample.sum_hist_sq_nonneg line 41
  3. lemma OAI.SidorenkoCounterexample.sum_hist_sq_eq_zero line 45
  4. lemma OAI.SidorenkoCounterexample.roundScore_loss_properties line 52
  5. def OAI.SidorenkoCounterexample.VertexPairScores.mix line 66
  6. lemma OAI.SidorenkoCounterexample.VertexPairScores.score_mix line 71
  7. def OAI.SidorenkoCounterexample.PreservesColors line 76
  8. lemma OAI.SidorenkoCounterexample.pinning_step line 78
  9. lemma OAI.SidorenkoCounterexample.pinning_complex line 117
  10. def OAI.SidorenkoCounterexample.exponentialNormalizer line 186
  11. lemma OAI.SidorenkoCounterexample.exponentialNormalizer_pos line 187
  12. def OAI.SidorenkoCounterexample.exponentialPrior line 189
  13. lemma OAI.SidorenkoCounterexample.prod_exp_weight line 193
  14. lemma OAI.SidorenkoCounterexample.exponentialPrior_product line 196
  15. lemma OAI.SidorenkoCounterexample.exponential_dominant_limit line 201
  16. lemma OAI.SidorenkoCounterexample.exponential_dominant_negative line 212
  17. def OAI.SidorenkoCounterexample.gibbsThinning line 240
  18. lemma OAI.SidorenkoCounterexample.gibbsThinning_pos line 243
  19. lemma OAI.SidorenkoCounterexample.gibbsThinning_le_one line 246
  20. def OAI.SidorenkoCounterexample.gibbsPrefactor line 250
  21. lemma OAI.SidorenkoCounterexample.gibbsPrefactor_pos line 252
  22. lemma OAI.SidorenkoCounterexample.gibbs_weight_formula line 255
  23. lemma OAI.SidorenkoCounterexample.averagedCoefficient_gibbs line 279
  24. lemma OAI.SidorenkoCounterexample.exists_negative_coefficient line 295