OAI/Probability/FirstPassage/BKContinuous.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PlanarFPP.StrictPathEvent line 10
  2. lemma OAI.PlanarFPP.dyadicPathFamily_subset line 13
  3. lemma OAI.PlanarFPP.dyadicDisjointPathFamily_subset line 18
  4. lemma OAI.PlanarFPP.dyadic_single_cell_original line 26
  5. lemma OAI.PlanarFPP.ExponentialEnvironment.dyadic_single_mass_le line 33
  6. lemma OAI.PlanarFPP.rounded_disjoint_cell_mem line 46
  7. lemma OAI.PlanarFPP.ExponentialEnvironment.rounded_disjoint_mass_le line 57
  8. lemma OAI.PlanarFPP.strict_path_probabilities_nonneg line 71
  9. lemma OAI.PlanarFPP.ExponentialEnvironment.dyadic_factors_le line 78
  10. theorem OAI.PlanarFPP.ExponentialEnvironment.rounded_strict_path_BK line 90
  11. theorem OAI.PlanarFPP.exponential_strict_path_BK line 97