OAI/Combinatorics/MatchingCount/Sampling/Through.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatchingFPRAS.Transport.PatternCode.through line 13
  2. def OAI.MatchingFPRAS.Transport.PatternCode.closed line 15
  3. def OAI.MatchingFPRAS.Transport.PatternCode.total line 17
  4. def OAI.MatchingFPRAS.Transport.PatternCode.ofPath line 19
  5. lemma OAI.MatchingFPRAS.Transport.PatternCode.activated line 25
  6. lemma OAI.MatchingFPRAS.Transport.PatternCode.activated_injective line 51
  7. lemma OAI.MatchingFPRAS.Transport.PatternCode.activated_derivative line 67
  8. instance OAI.MatchingFPRAS.Transport.PatternCode.(instance at line 83) line 83
  9. theorem OAI.MatchingFPRAS.Transport.PatternCode.activated_sum_le line 86
  10. structure OAI.MatchingFPRAS.PairEnergy.Law line 124
  11. def OAI.MatchingFPRAS.PairEnergy.guideMass line 131
  12. def OAI.MatchingFPRAS.PairEnergy.guideMean line 134
  13. def OAI.MatchingFPRAS.PairEnergy.contextMass line 138
  14. def OAI.MatchingFPRAS.PairEnergy.swapSum line 143
  15. lemma OAI.MatchingFPRAS.PairEnergy.weighted_jensen line 149
  16. lemma OAI.MatchingFPRAS.PairEnergy.sum_contextMass line 172
  17. lemma OAI.MatchingFPRAS.PairEnergy.tagged_context_bound line 202
  18. theorem OAI.MatchingFPRAS.PairEnergy.error_demand_load line 252
  19. instance OAI.MatchingFPRAS.Transport.instFintypePM line 318
  20. def OAI.MatchingFPRAS.Transport.gibbsLaw line 320
  21. def OAI.MatchingFPRAS.Transport.PatternCode.throughStates line 328
  22. def OAI.MatchingFPRAS.Transport.PatternCode.closedStates line 332
  23. lemma OAI.MatchingFPRAS.Transport.PatternCode.mem_throughStates line 337
  24. lemma OAI.MatchingFPRAS.Transport.PatternCode.mem_closedStates line 343
  25. def OAI.MatchingFPRAS.Transport.PatternCode.firstDerivative line 348
  26. def OAI.MatchingFPRAS.Transport.PatternCode.secondDerivative line 351
  27. lemma OAI.MatchingFPRAS.Transport.CellDemands.ErrorDemand.X_long line 375
  28. def OAI.MatchingFPRAS.Transport.CellDemands.ErrorDemand.pattern line 382
  29. def OAI.MatchingFPRAS.Transport.CellDemands.ErrorDemand.choice line 396
  30. lemma OAI.MatchingFPRAS.Transport.CellDemands.ErrorDemand.choice_spec line 400
  31. lemma OAI.MatchingFPRAS.Transport.CellDemands.ErrorDemand.choice_injective line 415
  32. lemma OAI.MatchingFPRAS.Transport.CellDemands.ErrorDemand.choice_through line 420
  33. theorem OAI.MatchingFPRAS.Transport.CellDemands.ErrorDemand.context_load line 431