OAI/Probability/SpanningForest/SampledUnitPath.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem336.SampledUnitPath.pathBlock line 15
  2. theorem OAI.Problem336.SampledUnitPath.measurable_pathBlock line 22
  3. theorem OAI.Problem336.SampledUnitPath.measurable_pathBlocks line 26
  4. lemma OAI.Problem336.SampledUnitPath.shift_grid line 32
  5. lemma OAI.Problem336.SampledUnitPath.shift_grid_succ line 39
  6. def OAI.Problem336.SampledUnitPath.bound line 45
  7. lemma OAI.Problem336.SampledUnitPath.bound_nonneg line 47
  8. lemma OAI.Problem336.SampledUnitPath.summable_bound line 50
  9. theorem OAI.Problem336.SampledUnitPath.ae_block_increment_bound line 62
  10. theorem OAI.Problem336.SampledUnitPath.ae_pathBlock_grid line 74
  11. theorem OAI.Problem336.SampledUnitPath.ae_sample_zero line 83
  12. theorem OAI.Problem336.SampledUnitPath.ae_pathBlock_endpoints line 89
  13. theorem OAI.Problem336.SampledUnitPath.ae_canonical_pathBlock_grid line 101