OAI/Combinatorics/MatchingCount/Sampling/LadderL.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MatchingFPRAS.Transport.ladder_minimum_mass line 19
  2. def OAI.MatchingFPRAS.Transport.ladderL line 42
  3. def OAI.MatchingFPRAS.Transport.ladderQ line 44
  4. def OAI.MatchingFPRAS.Transport.ladderM line 46
  5. def OAI.MatchingFPRAS.Transport.ladderLambda line 48
  6. def OAI.MatchingFPRAS.Transport.ladderSteps line 51
  7. lemma OAI.MatchingFPRAS.FiniteChain.log_inv_le_ceil_logb line 58
  8. lemma OAI.MatchingFPRAS.FiniteChain.mixing_at_steps line 71
  9. theorem OAI.MatchingFPRAS.Transport.ideal_ladder_sampling line 107