OAI/Probability/FirstPassage/BKRepeated.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.PlanarFPP.upward_disjointOccurrence line 12

   Also declared: OAI/Probability/GammaPassage/BKRepeated.lean:12 (same declaration text).

2. def OAI.PlanarFPP.fairFamilyMass line 21

   Also declared: OAI/Probability/GammaPassage/BKRepeated.lean:22 (same declaration text).

3. lemma OAI.PlanarFPP.fairFamilyMass_nonneg line 25

   Also declared: OAI/Probability/GammaPassage/BKRepeated.lean:26 (same declaration text).

4. lemma OAI.PlanarFPP.fairFamilyMass_mono line 29

   Also declared: OAI/Probability/GammaPassage/BKRepeated.lean:30 (same declaration text).

5. lemma OAI.PlanarFPP.fairFamilyMass_powerset line 34

   Also declared: OAI/Probability/GammaPassage/BKRepeated.lean:35 (same declaration text).

6. lemma OAI.PlanarFPP.finite_fair_BK_mass line 37

   Also declared: OAI/Probability/GammaPassage/BKRepeated.lean:38 (same declaration text).

7. def OAI.PlanarFPP.iteratedDisjointOccurrence line 47

   Also declared: OAI/Probability/GammaPassage/BKRepeated.lean:48 (same declaration text).

8. lemma OAI.PlanarFPP.upward_iteratedDisjointOccurrence line 51

   Also declared: OAI/Probability/GammaPassage/BKRepeated.lean:52 (same declaration text).

9. theorem OAI.PlanarFPP.finite_fair_BK_repeated line 60

   Also declared: OAI/Probability/GammaPassage/BKRepeated.lean:61 (same declaration text).

10. lemma OAI.PlanarFPP.mem_foldr_union line 71

    Also declared: OAI/Probability/GammaPassage/BKRepeated.lean:72 (same declaration text).

11. theorem OAI.PlanarFPP.certificates_mem_iterated line 77

    Also declared: OAI/Probability/GammaPassage/BKRepeated.lean:78 (same declaration text).

12. def OAI.PlanarFPP.certifiedDisjointFamily line 103

    Also declared: OAI/Probability/GammaPassage/BKRepeated.lean:104 (same declaration text).

13. theorem OAI.PlanarFPP.finite_fair_BK_certificates line 109

    Also declared: OAI/Probability/GammaPassage/BKRepeated.lean:110 (same declaration text).