OAI/Probability/FreeIsing/Trees/BranchingSurvivalLaw.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Problem367.BranchingSurvival.Labels line 11
  2. def OAI.Problem367.BranchingSurvival.wordMeasure line 13
  3. instance OAI.Problem367.BranchingSurvival.wordMeasure_probability line 16
  4. def OAI.Problem367.BranchingSurvival.branches line 20
  5. lemma OAI.Problem367.BranchingSurvival.measurable_branches line 22
  6. lemma OAI.Problem367.BranchingSurvival.map_branches line 26
  7. lemma OAI.Problem367.BranchingSurvival.indepFun_root_branches line 44
  8. lemma OAI.Problem367.BranchingSurvival.map_root_branches line 53
  9. def OAI.Problem367.BranchingSurvival.survives line 62
  10. def OAI.Problem367.BranchingSurvival.live line 66
  11. lemma OAI.Problem367.BranchingSurvival.measurableSet_survives line 69
  12. lemma OAI.Problem367.BranchingSurvival.measurableSet_live line 82
  13. def OAI.Problem367.BranchingSurvival.anyLive line 87
  14. lemma OAI.Problem367.BranchingSurvival.measurableSet_anyLive line 90
  15. lemma OAI.Problem367.BranchingSurvival.survives_succ_eq_preimage line 97
  16. lemma OAI.Problem367.BranchingSurvival.uniform01_Iic line 102
  17. lemma OAI.Problem367.BranchingSurvival.root_open_mass line 111
  18. theorem OAI.Problem367.BranchingSurvival.live_mass line 118
  19. theorem OAI.Problem367.BranchingSurvival.survives_succ_compl_mass line 132
  20. def OAI.Problem367.BranchingSurvival.probability line 144
  21. theorem OAI.Problem367.BranchingSurvival.probability_zero line 147
  22. lemma OAI.Problem367.BranchingSurvival.probability_nonneg line 150
  23. lemma OAI.Problem367.BranchingSurvival.probability_le_one line 153
  24. theorem OAI.Problem367.BranchingSurvival.probability_succ line 156