OAI/Probability/SLEGauge/EulerMeasurability.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Hausdorff gauges, Loewner evolution and trace measures.

  1. lemma OAI.SLEExactGauge.BrownianCalculus.measurable_nodes_driver line 27
  2. lemma OAI.SLEExactGauge.BrownianCalculus.expected_nodes_step line 33
  3. theorem OAI.SLEExactGauge.BrownianCalculus.expected_nodes line 58
  4. theorem OAI.SLEExactGauge.BrownianCalculus.expected_nodes_limit line 90
  5. lemma OAI.SLEExactGauge.BrownianCalculus.expected_shifted_taylor line 139
  6. lemma OAI.SLEExactGauge.BrownianCalculus.expected_shift_with_drift line 190
  7. lemma OAI.SLEExactGauge.BrownianCalculus.SmoothTest.euler_generator_error line 247
  8. lemma OAI.SLEExactGauge.BrownianCalculus.expected_active_euler_step line 265
  9. def OAI.SLEExactGauge.BrownianCalculus.frozenNodes line 344
  10. lemma OAI.SLEExactGauge.BrownianCalculus.measurable_frozenNodes line 353
  11. lemma OAI.SLEExactGauge.BrownianCalculus.frozenNodes_congr line 364
  12. lemma OAI.SLEExactGauge.BrownianCalculus.frozenNodes_history line 382
  13. lemma OAI.SLEExactGauge.BrownianCalculus.expected_frozen_step line 392