OAI/Probability/FirstPassage/OrientedProbability.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PlanarFPP.SeparatedGoodIndependent line 13

   Also declared: OAI/Probability/GammaPassage/OrientedProbability.lean:16 (same declaration text).

2. theorem OAI.PlanarFPP.independent_complement_inter line 18

   Also declared: OAI/Probability/GammaPassage/OrientedProbability.lean:21 (same declaration text).

3. theorem OAI.PlanarFPP.contour_bad_probability line 29

   Also declared: OAI/Probability/GammaPassage/OrientedProbability.lean:34 (same declaration text).

4. theorem OAI.PlanarFPP.enclosingLoop_card_geometric line 53

   Also declared: OAI/Probability/GammaPassage/OrientedProbability.lean:58 (same declaration text).