OAI/Combinatorics/MatchingCount/Probability/Mean.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatchingFPRAS.Replica.mean line 16
  2. def OAI.MatchingFPRAS.Replica.variance line 18
  3. lemma OAI.MatchingFPRAS.Replica.mean_dot line 21
  4. lemma OAI.MatchingFPRAS.Replica.density_sum line 23
  5. lemma OAI.MatchingFPRAS.Replica.mean_average line 29
  6. lemma OAI.MatchingFPRAS.Replica.mean_avgList line 36
  7. lemma OAI.MatchingFPRAS.Replica.average_update line 43
  8. lemma OAI.MatchingFPRAS.Replica.invariant_constant line 47
  9. lemma OAI.MatchingFPRAS.Replica.average_all line 66
  10. lemma OAI.MatchingFPRAS.Replica.avgList_fixed line 78
  11. lemma OAI.MatchingFPRAS.Replica.avgList_comm_list line 86
  12. lemma OAI.MatchingFPRAS.Replica.avgList_congr line 93
  13. lemma OAI.MatchingFPRAS.Replica.projection_pythagoras line 102
  14. def OAI.MatchingFPRAS.Replica.future line 119
  15. def OAI.MatchingFPRAS.Replica.increment line 121
  16. lemma OAI.MatchingFPRAS.Replica.martingale_partial line 124
  17. lemma OAI.MatchingFPRAS.Replica.martingale_variance line 169
  18. lemma OAI.MatchingFPRAS.Replica.increment_center line 179
  19. lemma OAI.MatchingFPRAS.Replica.average_pair_future line 183
  20. lemma OAI.MatchingFPRAS.Replica.increment_pair_formula line 198
  21. def OAI.MatchingFPRAS.Replica.localEnergy line 212
  22. lemma OAI.MatchingFPRAS.Replica.localEnergy_nonneg line 215
  23. lemma OAI.MatchingFPRAS.Replica.localEnergy_sub line 220
  24. lemma OAI.MatchingFPRAS.Replica.localEnergy_shift line 236
  25. lemma OAI.MatchingFPRAS.Replica.square_average line 244
  26. lemma OAI.MatchingFPRAS.Replica.localEnergy_average line 252
  27. lemma OAI.MatchingFPRAS.Replica.localEnergy_bound line 277
  28. lemma OAI.MatchingFPRAS.Replica.density_nonneg line 306
  29. lemma OAI.MatchingFPRAS.Replica.mean_mono line 309
  30. lemma OAI.MatchingFPRAS.Replica.mean_nonneg line 313
  31. lemma OAI.MatchingFPRAS.Replica.mean_add line 316
  32. lemma OAI.MatchingFPRAS.Replica.mean_mul line 319
  33. lemma OAI.MatchingFPRAS.Replica.mean_square line 322
  34. structure OAI.MatchingFPRAS.Replica.PairCapacity line 325
  35. def OAI.MatchingFPRAS.Replica.replacePair line 331
  36. def OAI.MatchingFPRAS.Replica.slice line 334
  37. def OAI.MatchingFPRAS.Replica.pairEnergy line 337
  38. lemma OAI.MatchingFPRAS.Replica.slice_sub line 341
  39. lemma OAI.MatchingFPRAS.Replica.pairEnergy_nonneg line 344
  40. lemma OAI.MatchingFPRAS.Replica.pairEnergy_sub line 348
  41. lemma OAI.MatchingFPRAS.Replica.slice_square_mean line 357
  42. lemma OAI.MatchingFPRAS.Replica.pairEnergy_bound line 369
  43. lemma OAI.MatchingFPRAS.Replica.replacePair_update line 378
  44. lemma OAI.MatchingFPRAS.Replica.slice_average line 385
  45. lemma OAI.MatchingFPRAS.Replica.pairEnergy_average line 391
  46. lemma OAI.MatchingFPRAS.Replica.pairEnergy_avgList line 402