OAI/Probability/GammaPassage/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/FirstPassage/BKRepeated.lean:12 (same declaration text).

2. def OAI.PlanarFPP.fairFamilyMass line 22

   Source documentation

   Uniform measure on the Boolean cube with ground set s.

   Also declared: OAI/Probability/FirstPassage/BKRepeated.lean:21 (same declaration text).

   noncomputable def fairFamilyMass (s : Finset α) (A : Finset (Finset α)) : ℝ :=
   …

3. lemma OAI.PlanarFPP.fairFamilyMass_nonneg line 26

   Also declared: OAI/Probability/FirstPassage/BKRepeated.lean:25 (same declaration text).

4. lemma OAI.PlanarFPP.fairFamilyMass_mono line 30

   Also declared: OAI/Probability/FirstPassage/BKRepeated.lean:29 (same declaration text).

5. lemma OAI.PlanarFPP.fairFamilyMass_powerset line 35

   Also declared: OAI/Probability/FirstPassage/BKRepeated.lean:34 (same declaration text).

6. lemma OAI.PlanarFPP.finite_fair_BK_mass line 38

   Also declared: OAI/Probability/FirstPassage/BKRepeated.lean:37 (same declaration text).

7. def OAI.PlanarFPP.iteratedDisjointOccurrence line 48

   Also declared: OAI/Probability/FirstPassage/BKRepeated.lean:47 (same declaration text).

8. lemma OAI.PlanarFPP.upward_iteratedDisjointOccurrence line 52

   Also declared: OAI/Probability/FirstPassage/BKRepeated.lean:51 (same declaration text).

9. theorem OAI.PlanarFPP.finite_fair_BK_repeated line 61

   Also declared: OAI/Probability/FirstPassage/BKRepeated.lean:60 (same declaration text).

10. lemma OAI.PlanarFPP.mem_foldr_union line 72

    Also declared: OAI/Probability/FirstPassage/BKRepeated.lean:71 (same declaration text).

11. theorem OAI.PlanarFPP.certificates_mem_iterated line 78

    Also declared: OAI/Probability/FirstPassage/BKRepeated.lean:77 (same declaration text).

12. def OAI.PlanarFPP.certifiedDisjointFamily line 104

    Also declared: OAI/Probability/FirstPassage/BKRepeated.lean:103 (same declaration text).

13. theorem OAI.PlanarFPP.finite_fair_BK_certificates line 110

    Also declared: OAI/Probability/FirstPassage/BKRepeated.lean:109 (same declaration text).