OAI/Probability/SpanningForest/DyadicTimes.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem336.DyadicTimes.grid line 12
  2. def OAI.Problem336.DyadicTimes.enumeration line 14
  3. theorem OAI.Problem336.DyadicTimes.enumeration_pair line 16
  4. theorem OAI.Problem336.DyadicTimes.enumeration_zero line 19
  5. theorem OAI.Problem336.DyadicTimes.coe_grid line 22
  6. theorem OAI.Problem336.DyadicTimes.grid_zero line 26
  7. theorem OAI.Problem336.DyadicTimes.grid_level_zero line 28
  8. lemma OAI.Problem336.DyadicTimes.grid_refine_even line 30
  9. lemma OAI.Problem336.DyadicTimes.grid_refine_midpoint line 35
  10. lemma OAI.Problem336.DyadicTimes.grid_increment line 42
  11. lemma OAI.Problem336.DyadicTimes.grid_le_one_iff line 48
  12. def OAI.Problem336.DyadicTimes.approximant line 53
  13. lemma OAI.Problem336.DyadicTimes.approximant_le line 56
  14. lemma OAI.Problem336.DyadicTimes.sub_approximant_nonneg line 62
  15. lemma OAI.Problem336.DyadicTimes.sub_approximant_lt line 66
  16. lemma OAI.Problem336.DyadicTimes.tendsto_approximant line 75
  17. lemma OAI.Problem336.DyadicTimes.approximant_mem_range line 83
  18. theorem OAI.Problem336.DyadicTimes.denseRange_enumeration line 87