OAI/Probability/SLE/StripProbabilities.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

Strip Probabilities for chordal SLE.

  1. theorem OAI.SLEExactGauge.comparison_path_strip_zero line 14
  2. lemma OAI.SLEExactGauge.source_strip_log_locallyLipschitz line 50
  3. def OAI.SLEExactGauge.BeforeFirstModulus line 74
  4. def OAI.SLEExactGauge.SourceUniformConformalLocalizationTarget line 79
  5. lemma OAI.SLEExactGauge.beforeFirstModulus_norm_le line 97
  6. lemma OAI.SLEExactGauge.sphericalTruncatedLog_eq_height_of_notin_ball line 109
  7. lemma OAI.SLEExactGauge.escape_forces_strip_level line 123
  8. theorem OAI.SLEExactGauge.sourceUniformConformalLocalization line 149
  9. theorem OAI.SLEExactGauge.ordinary_survival_bound_regular line 209
  10. theorem OAI.SLEExactGauge.ordinary_survival_bound line 253
  11. lemma OAI.SLEExactGauge.greenLogNormSq_initial_norm line 286
  12. theorem OAI.SLEExactGauge.ordinary_survival_radial_tail line 297
  13. theorem OAI.SLEExactGauge.ordinary_survival_polynomial line 354
  14. lemma OAI.SLEExactGauge.linear_subsolution_initial_nonpos line 390
  15. lemma OAI.SLEExactGauge.IsCapacityTwoWitness.real_derivative line 418
  16. lemma OAI.SLEExactGauge.IsCapacityTwoWitness.initial_real_le line 428
  17. lemma OAI.SLEExactGauge.IsCapacityTwoWitness.initial_real_ge line 455
  18. lemma OAI.SLEExactGauge.IsCapacityTwoWitness.initial_imag_square_le line 482
  19. lemma OAI.SLEExactGauge.IsCapacityTwoWitness.trace_real_bounds line 518
  20. lemma OAI.SLEExactGauge.IsCapacityTwoWitness.trace_imag_square_le line 543
  21. lemma OAI.SLEExactGauge.IsCapacityTwoWitness.trace_norm_square_le line 564
  22. lemma OAI.SLEExactGauge.exists_compact_square_field line 585
  23. lemma OAI.SLEExactGauge.brownian_stopped_square line 606