OAI/Probability/SLE/StoppedMeasures.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Stopped Measures for chordal SLE.

  1. def OAI.SLEExactGauge.sourceDriverPath line 23
  2. def OAI.SLEExactGauge.sourceTracePath line 27
  3. def OAI.SLEExactGauge.sourceRestartDriverPath line 30
  4. def OAI.SLEExactGauge.SourceStoppedTraceLawTarget line 39
  5. lemma OAI.SLEExactGauge.source_path_evaluation_embedding line 68
  6. lemma OAI.SLEExactGauge.source_path_measurable line 78
  7. lemma OAI.SLEExactGauge.source_trace_factor line 90
  8. lemma OAI.SLEExactGauge.source_reverseField_sub_real line 119
  9. lemma OAI.SLEExactGauge.IsCapacityTwoWitness.source_shifted_reverse_identifies line 127
  10. lemma OAI.SLEExactGauge.source_canonical_reverse_flow line 186
  11. lemma OAI.SLEExactGauge.source_restart_continuous_driver_law line 216
  12. theorem OAI.SLEExactGauge.sourceStoppedTraceLaw line 255
  13. lemma OAI.SLEExactGauge.IsCapacityTwoWitness.source_shifted_forward_approximation line 381
  14. theorem OAI.SLEExactGauge.sourceStoppedTraceLaw_forward line 433
  15. lemma OAI.SLEExactGauge.source_parameter_joint_law line 579
  16. lemma OAI.SLEExactGauge.source_parameter_condExp line 600
  17. theorem OAI.SLEExactGauge.source_killedChart_progressive line 647