OAI/Probability/SLE/StochasticFubini.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Stochastic Fubini for chordal SLE.

  1. theorem OAI.SLEExactGauge.clipped_spatial_green_window_exponential line 55
  2. theorem OAI.SLEExactGauge.clipped_spatial_green_exponential line 227
  3. def OAI.SLEExactGauge.spatialFiltration line 366
  4. lemma OAI.SLEExactGauge.spatial_stopping_section line 372
  5. structure OAI.SLEExactGauge.SpatialLogLocalization line 383
  6. theorem OAI.SLEExactGauge.exists_spatial_log_localization line 402
  7. lemma OAI.SLEExactGauge.SpatialLogLocalization.measurable line 454
  8. lemma OAI.SLEExactGauge.SpatialLogLocalization.exponential line 457
  9. lemma OAI.SLEExactGauge.greenLogCoefficient_logCoordinates line 480
  10. lemma OAI.SLEExactGauge.clipped_chart_identification line 493
  11. lemma OAI.SLEExactGauge.SpatialLogLocalization.chart_identification line 517
  12. lemma OAI.SLEExactGauge.stopped_difference_max line 549
  13. theorem OAI.SLEExactGauge.closed_stop_limit_condExp line 558
  14. lemma OAI.SLEExactGauge.boundedSpatialHit_le_time line 637
  15. lemma OAI.SLEExactGauge.boundedSpatialHit_min line 643
  16. lemma OAI.SLEExactGauge.RegularSLEPresentation.spatialGreen_condExp_of_level line 654
  17. theorem OAI.SLEExactGauge.RegularSLEPresentation.spatialGreen_condExp line 696