OAI/Probability/SLE/SwallowExit.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

Swallow Exit for chordal SLE.

  1. lemma OAI.SLEExactGauge.nonnegative_integral_tail line 15
  2. lemma OAI.SLEExactGauge.RadialLocalization.exit_probability line 37
  3. structure OAI.SLEExactGauge.BoundaryLocalization line 96
  4. lemma OAI.SLEExactGauge.exists_boundaryLocalization line 115
  5. lemma OAI.SLEExactGauge.BoundaryLocalization.density_crossing_probability line 173
  6. def OAI.SLEExactGauge.IsPositiveBoundaryClockPath line 200
  7. lemma OAI.SLEExactGauge.IsPositiveBoundaryClockPath.continuousOn line 210
  8. lemma OAI.SLEExactGauge.IsPositiveBoundaryClockPath.positive_lower_bound line 213
  9. lemma OAI.SLEExactGauge.IsPositiveBoundaryClockPath.clock_identity line 222
  10. lemma OAI.SLEExactGauge.IsPositiveBoundaryClockPath.clipped_identification line 244
  11. def OAI.SLEExactGauge.greenDensity line 276
  12. def OAI.SLEExactGauge.initialGreen line 284
  13. def OAI.SLEExactGauge.radiusLevelTime line 290
  14. def OAI.SLEExactGauge.stoppedGreen line 296
  15. lemma OAI.SLEExactGauge.logCoordinates_re line 302
  16. lemma OAI.SLEExactGauge.logCoordinates_im line 308
  17. lemma OAI.SLEExactGauge.logCoordinates_snd line 314
  18. lemma OAI.SLEExactGauge.greenLogNormSq_logCoordinates line 318
  19. lemma OAI.SLEExactGauge.logAngleSq_logCoordinates line 329
  20. lemma OAI.SLEExactGauge.greenLogDensity_logCoordinates line 340
  21. lemma OAI.SLEExactGauge.greenLogDensity_initial line 370
  22. lemma OAI.SLEExactGauge.RadialLocalization.alive_forces_radial_or_time_boundary line 408
  23. lemma OAI.SLEExactGauge.measure_eventually_sets_le line 428
  24. lemma OAI.SLEExactGauge.BoundaryLocalization.true_crossing_forces_density_boundary line 462
  25. theorem OAI.SLEExactGauge.exists_measurable_brownian_version line 498
  26. theorem OAI.SLEExactGauge.exists_continuous_measurable_brownian_version line 529
  27. theorem OAI.SLEExactGauge.exists_regular_brownian_version line 566
  28. theorem OAI.SLEExactGauge.boundary_maximal_density_regular line 600
  29. theorem OAI.SLEExactGauge.boundary_maximal_density line 670
  30. theorem OAI.SLEExactGauge.IsCapacityTwoWitness.forward_flow_survives line 706