OAI/Probability/FirstPassage/HighDensityOriented.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PlanarFPP.badContourEvent line 11

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

2. theorem OAI.PlanarFPP.no_infinite_path_subset_contours line 15

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

3. theorem OAI.PlanarFPP.bad_contours_fixed_length line 27

   Also declared: OAI/Probability/GammaPassage/HighDensityOriented.lean:28 (same declaration text).

4. theorem OAI.PlanarFPP.no_infinite_path_probability line 52

   Also declared: OAI/Probability/GammaPassage/HighDensityOriented.lean:53 (same declaration text).

5. theorem OAI.PlanarFPP.high_density_oriented_paths line 69

   Also declared: OAI/Probability/GammaPassage/HighDensityOriented.lean:70 (same declaration text).

6. theorem OAI.PlanarFPP.high_density_oriented_paths_real_bound line 83

   Also declared: OAI/Probability/GammaPassage/HighDensityOriented.lean:85 (same declaration text).

7. theorem OAI.PlanarFPP.high_density_oriented_paths_real line 96

   Also declared: OAI/Probability/GammaPassage/HighDensityOriented.lean:99 (same declaration text).

8. theorem OAI.PlanarFPP.high_density_oriented_paths_uniform line 104

   Also declared: OAI/Probability/GammaPassage/HighDensityOriented.lean:109 (same declaration text).