OAI/Probability/FirstPassage/ContourLocalization.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PlanarFPP.SquareSide.axisCross line 11

   Also declared: OAI/Probability/GammaPassage/ContourLocalization.lean:13 (same declaration text).

2. def OAI.PlanarFPP.SquareSide.aboveAxis line 17

   Also declared: OAI/Probability/GammaPassage/ContourLocalization.lean:19 (same declaration text).

3. theorem OAI.PlanarFPP.SquareSide.axisCross_eq line 19

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

4. theorem OAI.PlanarFPP.SquareSide.rayCross_eq_axisCross line 25

   Distinct definitions of this name: OAI/Probability/GammaPassage/ContourLocalization.lean:27 (same statement text; different proof or body). Qualify references as OAI.PlanarFPP.SquareSide.rayCross_eq_axisCross@path.

5. theorem OAI.PlanarFPP.SquareSide.rayCross_ne_zero_location line 30

   Distinct definitions of this name: OAI/Probability/GammaPassage/ContourLocalization.lean:33 (same statement text; different proof or body). Qualify references as OAI.PlanarFPP.SquareSide.rayCross_ne_zero_location@path.

6. theorem OAI.PlanarFPP.SquareLoop.sum_axisCross line 40

   Also declared: OAI/Probability/GammaPassage/ContourLocalization.lean:44 (same declaration text).

7. theorem OAI.PlanarFPP.SquareLoop.winding_locations line 45

   Also declared: OAI/Probability/GammaPassage/ContourLocalization.lean:49 (same declaration text).

8. theorem OAI.PlanarFPP.SquareLoop.tail_bounds line 62

   Also declared: OAI/Probability/GammaPassage/ContourLocalization.lean:66 (same declaration text).

9. theorem OAI.PlanarFPP.SquareLoop.start_mem_box line 85

   Distinct definitions of this name: OAI/Probability/GammaPassage/ContourLocalization.lean:91 (different declaration text). Qualify references as OAI.PlanarFPP.SquareLoop.start_mem_box@path.