OAI/Probability/SLEGauge/RadialStopping.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

Hausdorff gauges, Loewner evolution and trace measures.

  1. lemma OAI.ExactSLEGreen.capTime_eq line 22
  2. lemma OAI.ExactSLEGreen.stopped_before_cap line 24
  3. lemma OAI.ExactSLEGreen.stopped_cap_measurable line 39
  4. lemma OAI.ExactSLEGreen.stopping_before_measurable line 45
  5. lemma OAI.ExactSLEGreen.eventually_before_nat line 49
  6. theorem OAI.ExactSLEGreen.radial_conditional_weight_all line 57
  7. def OAI.ExactSLEGreen.radialLaw line 145
  8. lemma OAI.ExactSLEGreen.radialTime_stopping line 149
  9. lemma OAI.ExactSLEGreen.radialTime_le_of_hit line 205
  10. lemma OAI.ExactSLEGreen.radialTime_strict_of_finite line 210
  11. lemma OAI.ExactSLEGreen.radialTime_strict_of_first_finite line 235
  12. lemma OAI.ExactSLEGreen.radialWeight_consistency line 244
  13. lemma OAI.ExactSLEGreen.radialLaw_apply line 270
  14. lemma OAI.ExactSLEGreen.radialLaw_probability line 283
  15. theorem OAI.ExactSLEGreen.finite_radial_laws_consistent line 293
  16. theorem OAI.ExactSLEGenerator.compact_test_optional_inequality line 321
  17. def OAI.ExactSLEGreen.physicalTheta line 395
  18. def OAI.ExactSLEGreen.thetaDeriv line 396
  19. def OAI.ExactSLEGreen.physicalV line 398
  20. def OAI.ExactSLEGreen.velocityDeriv line 399
  21. lemma OAI.ExactSLEGreen.physicalTheta_mem line 402
  22. lemma OAI.ExactSLEGreen.physicalTheta_cot line 407
  23. lemma OAI.ExactSLEGreen.hasFDerivAt_physicalTheta line 411
  24. lemma OAI.ExactSLEGreen.thetaDeriv_noise line 427