OAI/Probability/SLEGauge/StoppedLimits.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

Hausdorff gauges, Loewner evolution and trace measures.

  1. theorem OAI.SLEExactGauge.BrownianCalculus.expected_stopped_local_eq line 42
  2. abbrev OAI.SLEExactGauge.OnePoint.State line 83
  3. def OAI.SLEExactGauge.OnePoint.domain line 85
  4. def OAI.SLEExactGauge.OnePoint.field line 86
  5. def OAI.SLEExactGauge.OnePoint.green line 89
  6. lemma OAI.SLEExactGauge.OnePoint.isOpen_domain line 92
  7. lemma OAI.SLEExactGauge.OnePoint.green_nonneg line 95
  8. lemma OAI.SLEExactGauge.OnePoint.green_le line 98
  9. lemma OAI.SLEExactGauge.OnePoint.contDiffOn_green line 108
  10. lemma OAI.SLEExactGauge.OnePoint.green_generator line 119
  11. theorem OAI.SLEExactGauge.BrownianCalculus.expected_stopped_smooth_grid line 160
  12. theorem OAI.SLEExactGauge.BrownianCalculus.expected_stopped_local_grid line 206
  13. theorem OAI.SLEExactGauge.BrownianCalculus.expected_stopped_local_grid_eq line 263
  14. theorem OAI.SLEExactGauge.Localization.bounded_lipschitz_ode line 309
  15. def OAI.SLEExactGauge.ODEPath.mesh line 342
  16. lemma OAI.SLEExactGauge.ODEPath.mesh_pos line 343
  17. lemma OAI.SLEExactGauge.ODEPath.mesh_zero line 344
  18. def OAI.SLEExactGauge.ODEPath.drift line 347
  19. def OAI.SLEExactGauge.ODEPath.flow line 348
  20. lemma OAI.SLEExactGauge.ODEPath.measurable_nodes line 352
  21. lemma OAI.SLEExactGauge.ODEPath.measurable_interpolate line 361
  22. lemma OAI.SLEExactGauge.ODEPath.measurable_flow line 368
  23. lemma OAI.SLEExactGauge.ODEPath.nodes_past line 373
  24. lemma OAI.SLEExactGauge.ODEPath.interpolate_past line 387
  25. lemma OAI.SLEExactGauge.ODEPath.flow_past line 397
  26. theorem OAI.SLEExactGauge.ODEPath.flow_solution line 407
  27. lemma OAI.SLEExactGauge.ODEPath.continuousOn_flow line 431
  28. def OAI.SLEExactGauge.RationalStop.sample line 442
  29. lemma OAI.SLEExactGauge.RationalStop.sample_mem line 443
  30. lemma OAI.SLEExactGauge.RationalStop.sample_self line 445
  31. lemma OAI.SLEExactGauge.RationalStop.continuous_sample line 447
  32. def OAI.SLEExactGauge.RationalStop.Safe line 451
  33. lemma OAI.SLEExactGauge.RationalStop.safe_iff line 454