OAI/Probability/SLEGauge/BrownianNodes.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

Hausdorff gauges, Loewner evolution and trace measures.

  1. lemma OAI.SLEExactGauge.BrownianCalculus.increment_indep_history line 26
  2. lemma OAI.SLEExactGauge.BrownianCalculus.increment_indep_past_function line 31
  3. lemma OAI.SLEExactGauge.BrownianCalculus.predictable_increment_centered line 35
  4. lemma OAI.SLEExactGauge.BrownianCalculus.increment_pow_integrable line 46
  5. lemma OAI.SLEExactGauge.BrownianCalculus.predictable_innovation_centered line 53
  6. lemma OAI.SLEExactGauge.BrownianCalculus.predictable_compensated_square_centered line 67
  7. lemma OAI.SLEExactGauge.BrownianCalculus.increment_abs_cube_integrable line 76
  8. lemma OAI.SLEExactGauge.BrownianCalculus.abs_cube_bound line 83
  9. lemma OAI.SLEExactGauge.BrownianCalculus.increment_abs_cube_le line 100
  10. lemma OAI.SLEExactGauge.BrownianCalculus.taylor_second_bound line 125
  11. lemma OAI.SLEExactGauge.BrownianCalculus.expected_taylor_step line 162
  12. lemma OAI.SLEExactGauge.BrownianCalculus.state_taylor_bound line 238
  13. lemma OAI.SLEExactGauge.BrownianCalculus.state_euler_remainder line 267
  14. theorem OAI.SLEExactGauge.BrownianCalculus.expected_euler_step line 288
  15. structure OAI.SLEExactGauge.BrownianCalculus.SmoothTest line 385
  16. def OAI.SLEExactGauge.BrownianCalculus.extendHistory line 411
  17. lemma OAI.SLEExactGauge.BrownianCalculus.measurable_extendHistory line 414
  18. def OAI.SLEExactGauge.BrownianCalculus.stochasticNodes line 423
  19. lemma OAI.SLEExactGauge.BrownianCalculus.measurable_stochasticNodes line 428
  20. lemma OAI.SLEExactGauge.BrownianCalculus.stochasticNodes_congr line 436
  21. lemma OAI.SLEExactGauge.BrownianCalculus.stochasticNodes_history line 448