OAI/Probability/SLEGauge/OptionalEstimates.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

Hausdorff gauges, Loewner evolution and trace measures.

  1. theorem OAI.ExactSLEGreen.discounted_regime_optional line 28
  2. theorem OAI.ExactSLEGenerator.compact_test_optional_on_event line 89
  3. lemma OAI.ExactSLEPasting.integral_weighted_le line 168
  4. lemma OAI.ExactSLEPasting.integral_weighted_le_on_event line 202
  5. theorem OAI.ExactSLEGreen.discounted_regime_weighted_optional line 225
  6. def OAI.ExactSLEGreen.scalarClamp line 301
  7. lemma OAI.ExactSLEGreen.scalarClamp_continuous line 302
  8. lemma OAI.ExactSLEGreen.scalarClamp_bounds line 304
  9. lemma OAI.ExactSLEGreen.scalarClamp_eq line 306
  10. lemma OAI.ExactSLEGreen.scalarClamp_idem line 308
  11. def OAI.ExactSLEGreen.regimeClamp line 310
  12. lemma OAI.ExactSLEGreen.regimeClamp_continuous line 312
  13. lemma OAI.ExactSLEGreen.regimeClamp_height line 325
  14. lemma OAI.ExactSLEGreen.regimeClamp_idem line 327
  15. lemma OAI.ExactSLEGreen.regimeClamp_bound line 337
  16. lemma OAI.ExactSLEGreen.regimeClamp_eq line 359
  17. lemma OAI.ExactSLEGreen.regimeDiscount_continuousAt line 373
  18. def OAI.ExactSLEGreen.regimeDiscountCut line 395
  19. lemma OAI.ExactSLEGreen.regimeDiscountCut_continuous line 398
  20. lemma OAI.ExactSLEGreen.regimeDiscountCut_bound line 405
  21. def OAI.ExactSLEGreen.vectorState line 423
  22. lemma OAI.ExactSLEGreen.vectorState_continuous line 425
  23. lemma OAI.ExactSLEGreen.vectorState_adapted line 428
  24. def OAI.ExactSLEGreen.regimeDrift line 432
  25. lemma OAI.ExactSLEGreen.regimeDrift_continuous line 435
  26. lemma OAI.ExactSLEGreen.regimeDrift_bound line 440