OAI/Combinatorics/InfiniteMatroid/ProbeLimits.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.InfiniteMatroidCounterexample.finiteDensity_abs_sub line 11
  2. lemma OAI.InfiniteMatroidCounterexample.dProbe_zero line 24
  3. lemma OAI.InfiniteMatroidCounterexample.trace_prefix_card line 29
  4. lemma OAI.InfiniteMatroidCounterexample.prefix_card_atTop line 40
  5. lemma OAI.InfiniteMatroidCounterexample.pProbe_sum line 53
  6. lemma OAI.InfiniteMatroidCounterexample.pProbe_normalized_zero line 64
  7. def OAI.InfiniteMatroidCounterexample.errorTail line 72
  8. lemma OAI.InfiniteMatroidCounterexample.dProbe_abs_bdd line 74
  9. lemma OAI.InfiniteMatroidCounterexample.errorTail_nonneg line 79
  10. lemma OAI.InfiniteMatroidCounterexample.abs_dProbe_le_errorTail line 82
  11. lemma OAI.InfiniteMatroidCounterexample.errorTail_zero line 85
  12. lemma OAI.InfiniteMatroidCounterexample.small_iff_density line 89