OAI/Combinatorics/MatchingCount/Probability/LocalVariance.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatchingFPRAS.Replica.localVariance line 17
  2. def OAI.MatchingFPRAS.Replica.PairPoincare line 20
  3. lemma OAI.MatchingFPRAS.Replica.invariant_update line 24
  4. lemma OAI.MatchingFPRAS.Replica.pairEnergy_shift_invariant line 30
  5. lemma OAI.MatchingFPRAS.Replica.pair_poincare_global line 42
  6. lemma OAI.MatchingFPRAS.Replica.projection_contraction line 66
  7. def OAI.MatchingFPRAS.Replica.baseEnergy line 72
  8. lemma OAI.MatchingFPRAS.Replica.baseEnergy_nonneg line 76
  9. lemma OAI.MatchingFPRAS.Replica.increment_base_bound line 82
  10. lemma OAI.MatchingFPRAS.Replica.one_pair line 93
  11. def OAI.MatchingFPRAS.Replica.allowed line 144
  12. lemma OAI.MatchingFPRAS.Replica.sum_allowed line 148
  13. def OAI.MatchingFPRAS.Replica.pairTotal line 157
  14. def OAI.MatchingFPRAS.Replica.baseTotal line 160
  15. def OAI.MatchingFPRAS.Replica.scanEnergy line 163
  16. theorem OAI.MatchingFPRAS.Replica.replica_gap line 168
  17. structure OAI.MatchingFPRAS.Replica.SymmetricProposal line 247
  18. def OAI.MatchingFPRAS.Replica.offCapacity line 253
  19. def OAI.MatchingFPRAS.Replica.metropolisCapacity line 256
  20. lemma OAI.MatchingFPRAS.Replica.offCapacity_nonneg line 261
  21. lemma OAI.MatchingFPRAS.Replica.offCapacity_le line 266
  22. lemma OAI.MatchingFPRAS.Replica.offCapacity_symmetric line 271
  23. lemma OAI.MatchingFPRAS.Replica.offCapacity_sum_le line 275
  24. lemma OAI.MatchingFPRAS.Replica.metropolisCapacity_nonneg line 284
  25. lemma OAI.MatchingFPRAS.Replica.metropolisCapacity_symmetric line 291
  26. lemma OAI.MatchingFPRAS.Replica.metropolisCapacity_row line 298
  27. lemma OAI.MatchingFPRAS.Replica.metropolisCapacity_col line 309
  28. def OAI.MatchingFPRAS.Replica.metropolis line 314
  29. lemma OAI.MatchingFPRAS.Replica.metropolis_row line 317
  30. lemma OAI.MatchingFPRAS.Replica.metropolis_nonneg line 322
  31. lemma OAI.MatchingFPRAS.Replica.metropolis_acceptance line 326
  32. lemma OAI.MatchingFPRAS.Replica.metropolis_detailed line 334
  33. lemma OAI.MatchingFPRAS.Replica.metropolis_energy line 341
  34. theorem OAI.MatchingFPRAS.Replica.metropolis_energy_domination line 351
  35. def OAI.MatchingFPRAS.Transport.firstLift line 384
  36. lemma OAI.MatchingFPRAS.Transport.firstLift_row line 387
  37. lemma OAI.MatchingFPRAS.Transport.firstLift_symmetric line 392
  38. def OAI.MatchingFPRAS.Transport.pairProposalRaw line 396
  39. def OAI.MatchingFPRAS.Transport.pairProposal line 399
  40. def OAI.MatchingFPRAS.Transport.pairLaw line 419
  41. lemma OAI.MatchingFPRAS.Transport.firstLift_energy line 428