OAI/Probability/SLE/Geometry/WaypointAngleNumerics.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The quantitative conversion from the two half-plane exit-arc probabilities to the exact sine normalization used by guide compactness.

  1. theorem OAI.SLEExactGauge.CrosscutSides.sine_lower_bound_of_two_arc_bounds line 14
  2. theorem OAI.SLEExactGauge.CrosscutSides.positive_angle_of_two_exit_probability_bounds line 41