OAI/Probability/SLE/ChartMeasurability.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

Chart Measurability for chordal SLE.

  1. lemma OAI.SLEExactGauge.source_killedChart_stopped_measurable line 17
  2. lemma OAI.SLEExactGauge.source_measurable_inverse_chart line 41
  3. lemma OAI.SLEExactGauge.source_stopped_inverseChart_measurable line 106
  4. lemma OAI.SLEExactGauge.source_halfplane_cmap_measurable line 143
  5. def OAI.SLEExactGauge.sourceStoppedInversePath line 158
  6. lemma OAI.SLEExactGauge.source_stopped_inversePath_measurable line 167
  7. def OAI.SLEExactGauge.square line 197
  8. def OAI.SLEExactGauge.upperExterior line 199
  9. def OAI.SLEExactGauge.lowerExterior line 201
  10. lemma OAI.SLEExactGauge.square_isCompact line 203
  11. lemma OAI.SLEExactGauge.bounded_subset_square line 212
  12. lemma OAI.SLEExactGauge.upperExterior_eq line 220
  13. lemma OAI.SLEExactGauge.upperExterior_preconnected line 239
  14. lemma OAI.SLEExactGauge.upperExterior_unbounded line 251
  15. lemma OAI.SLEExactGauge.upperExterior_subset_survivingDomain line 266
  16. lemma OAI.SLEExactGauge.source_live_compact_bridge line 287
  17. lemma OAI.SLEExactGauge.source_live_of_bridge line 349
  18. def OAI.SLEExactGauge.sourceRescaledPath line 375
  19. lemma OAI.SLEExactGauge.sourceRescaledPath_continuous line 378
  20. lemma OAI.SLEExactGauge.sourceRescaledPath_mapsTo line 383
  21. lemma OAI.SLEExactGauge.source_survival_open line 395
  22. abbrev OAI.SLEExactGauge.SourceDiskParameter line 419
  23. lemma OAI.SLEExactGauge.source_physical_disk_kernel_open line 421
  24. lemma OAI.SLEExactGauge.source_high_vertical_survives line 466
  25. lemma OAI.SLEExactGauge.IsCapacityTwoWitness.source_later_image_unbounded line 487
  26. lemma OAI.SLEExactGauge.IsCapacityTwoWitness.source_surviving_preconnected line 530
  27. lemma OAI.SLEExactGauge.source_stopped_live_transfer line 543
  28. def OAI.SLEExactGauge.SourcePathInteriorDense line 588
  29. lemma OAI.SLEExactGauge.source_path_interior_dense_measurable line 591
  30. lemma OAI.SLEExactGauge.IsCapacityTwoWitness.radius_le_of_domain_subset line 629