OAI/Combinatorics/BalancedRyser/Local/LocalExposureTiming.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Balanced.Local.Timing.prefixTokens line 14
  2. theorem OAI.Balanced.Local.Timing.inl_mem_prefixTokens line 18
  3. theorem OAI.Balanced.Local.Timing.inr_mem_prefixTokens line 23
  4. theorem OAI.Balanced.Local.Timing.card_token_set_le line 28
  5. theorem OAI.Balanced.Local.Timing.rootsFirstRank_phase line 33
  6. theorem OAI.Balanced.Local.Timing.currentOldIndices_in_prefix line 43
  7. theorem OAI.Balanced.Local.Timing.injectionAverage_later_usedTest_le line 58
  8. theorem OAI.Balanced.Local.Timing.injectionAverage_usedTest_le_of_projected line 83