OAI/Probability/SLE/NearRealContraction.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

Near Real Contraction for chordal SLE.

  1. lemma OAI.SLEExactGauge.reciprocal_real_near_one line 15
  2. lemma OAI.SLEExactGauge.boundary_difference_coefficient line 34
  3. theorem OAI.SLEExactGauge.near_real_difference_bound line 51
  4. def OAI.SLEExactGauge.BoundaryComparisonFailure line 129
  5. lemma OAI.SLEExactGauge.BoundaryComparisonFailure.density_crossing line 137
  6. lemma OAI.SLEExactGauge.boundary_density_threshold_initial line 173
  7. lemma OAI.SLEExactGauge.boundary_density_threshold_quotient line 185
  8. lemma OAI.SLEExactGauge.near_real_first_contact line 207
  9. lemma OAI.SLEExactGauge.rightField_im line 232
  10. lemma OAI.SLEExactGauge.right_flow_im_pos line 242
  11. lemma OAI.SLEExactGauge.right_flow_unclipped_of_ratio line 270
  12. lemma OAI.SLEExactGauge.no_boundary_failure_gives_complex_flow line 282
  13. theorem OAI.SLEExactGauge.IsCapacityTwoWitness.half_ball_survives_before_boundary_collision line 346
  14. lemma OAI.SLEExactGauge.upper_mobius_norm_lt_one line 384
  15. lemma OAI.SLEExactGauge.radius_of_halfplane_map line 400
  16. lemma OAI.SLEExactGauge.ball_subset_survivingDomain line 448
  17. lemma OAI.SLEExactGauge.ball_subset_upperHalfPlane line 458
  18. lemma OAI.SLEExactGauge.IsCapacityTwoWitness.trace_approach_of_radius_lt line 470
  19. lemma OAI.SLEExactGauge.IsCapacityTwoWitness.trace_mem_closure_surviving line 502
  20. lemma OAI.SLEExactGauge.IsCapacityTwoWitness.surviving_of_free_ball_future_tip line 515
  21. lemma OAI.SLEExactGauge.IsCapacityTwoWitness.boundary_path_of_half_ball_survivor line 540
  22. lemma OAI.SLEExactGauge.IsCapacityTwoWitness.tip_avoids_half_ball_of_boundary_path line 603
  23. theorem OAI.SLEExactGauge.IsCapacityTwoWitness.all_time_real_center_avoidance line 634
  24. lemma OAI.SLEExactGauge.boundary_comparison_failure_probability_regular line 661
  25. theorem OAI.SLEExactGauge.boundary_comparison_failure_probability line 687
  26. theorem OAI.SLEExactGauge.boundary_comparison_failure_sle_exponent line 705
  27. lemma OAI.SLEExactGauge.stopping_grid_piece_measurable line 733
  28. lemma OAI.SLEExactGauge.grid_partition_union line 756
  29. lemma OAI.SLEExactGauge.grid_partition_disjoint line 763
  30. lemma OAI.SLEExactGauge.integral_stopping_grid_glue line 772