OAI/Probability/GammaPassage/ContourLocalization.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

A loop with nonzero ray-crossing count starts within O(m) of zero. This supplies the location factor in the source's contour enumeration.

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

    Also declared: OAI/Probability/FirstPassage/ContourLocalization.lean:11 (same declaration text).

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

    Also declared: OAI/Probability/FirstPassage/ContourLocalization.lean:17 (same declaration text).

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

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

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

    Distinct definitions of this name: OAI/Probability/FirstPassage/ContourLocalization.lean:25 (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 33

    Distinct definitions of this name: OAI/Probability/FirstPassage/ContourLocalization.lean:30 (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 44

    Also declared: OAI/Probability/FirstPassage/ContourLocalization.lean:40 (same declaration text).

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

    Also declared: OAI/Probability/FirstPassage/ContourLocalization.lean:45 (same declaration text).

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

    Also declared: OAI/Probability/FirstPassage/ContourLocalization.lean:62 (same declaration text).

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

    Source documentation

    With the source's length m, every enclosing loop has a permitted starting point in a deterministic box of cardinality (2m+3)^2.

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

    theorem start_mem_box (c : SquareLoop m) (hm : 0 < m) (hc : c.winding ≠ 0) :
    (c.side ⟨0,hm⟩).tail ∈ orientedSelectionBox (m+1) := by
…

    Mentions: OAI.PlanarFPP.SquareLoop, OAI.PlanarFPP.orientedSelectionBox