OAI/Probability/SLEGauge/CommonStoppedMass.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

Hausdorff gauges, Loewner evolution and trace measures.

  1. theorem OAI.ExactSLEGreen.recoveredMass_all_stopping line 21
  2. lemma OAI.SLEExactGauge.TraceRestriction.firstVisit_finite_of_exhaustion line 106
  3. lemma OAI.SLEExactGauge.TraceRestriction.firstVisit_fiber_subset line 132
  4. lemma OAI.SLEExactGauge.TraceRestriction.firstVisit_fiber_null line 148
  5. lemma OAI.SLEExactGauge.TraceRestriction.restrict_strictFirstVisit line 156
  6. structure OAI.SLEExactGauge.TraceMassContinuity.TraceMassFacts line 184
  7. lemma OAI.SLEExactGauge.TraceMassContinuity.traceMassFacts_of_restrictions line 209
  8. lemma OAI.SLEExactGauge.TraceMassContinuity.TraceMassFacts.capacity_increment_support line 261
  9. def OAI.SLEExactGauge.TraceMassContinuity.massTimeList line 291
  10. lemma OAI.SLEExactGauge.TraceMassContinuity.massTimeList_top line 296
  11. lemma OAI.SLEExactGauge.TraceMassContinuity.massTimeList_nat line 298
  12. lemma OAI.SLEExactGauge.TraceMassContinuity.massTimeList_small line 301
  13. lemma OAI.SLEExactGauge.TraceMassContinuity.massTimeList_dense line 304
  14. lemma OAI.SLEExactGauge.TraceMassContinuity.massTimeList_is_dense line 308
  15. theorem OAI.SLEExactGauge.TraceMassContinuity.actual_common_trace_mass line 331
  16. def OAI.SLEExactGauge.LoewnerRestart.concatenate line 399
  17. lemma OAI.SLEExactGauge.LoewnerRestart.concatenate_apply line 407
  18. lemma OAI.SLEExactGauge.LoewnerRestart.continuous_concatenate line 410
  19. lemma OAI.SLEExactGauge.LoewnerRestart.concatenate_before line 421
  20. lemma OAI.SLEExactGauge.LoewnerRestart.concatenate_reconstruct line 425
  21. lemma OAI.SLEExactGauge.LoewnerRestart.raw_event_congr line 437
  22. lemma OAI.SLEExactGauge.LoewnerRestart.raw_stop_congr line 448
  23. def OAI.SLEExactGauge.LoewnerRestart.shiftStop line 465
  24. lemma OAI.SLEExactGauge.LoewnerRestart.shiftStop_isStoppingTime line 467
  25. lemma OAI.SLEExactGauge.LoewnerRestart.measurableSpace_le_shiftStop line 486
  26. lemma OAI.SLEExactGauge.LoewnerRestart.raw_stopped_event_congr line 492
  27. def OAI.SLEExactGauge.LoewnerRestart.concatenatedEvent line 502
  28. lemma OAI.SLEExactGauge.LoewnerRestart.concatenatedEvent_measurable line 507
  29. lemma OAI.SLEExactGauge.LoewnerRestart.concatenatedEvent_past line 517
  30. lemma OAI.SLEExactGauge.LoewnerRestart.concatenatedEvent_raw_joint line 544
  31. lemma OAI.SLEExactGauge.LoewnerRestart.concatenatedEvent_stoppedData line 560