OAI/Probability/SLEGauge/InverseRegularity.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

Hausdorff gauges, Loewner evolution and trace measures.

  1. theorem OAI.SLEExactGauge.LiteralTrace.exists_inverseFlow line 22
  2. lemma OAI.SLEExactGauge.LiteralTrace.inverseFlow_surviving line 69
  3. lemma OAI.SLEExactGauge.LiteralTrace.flow_inverseFlow line 73
  4. lemma OAI.SLEExactGauge.LiteralTrace.cutoffFlow_dist_le line 82
  5. lemma OAI.SLEExactGauge.LiteralTrace.cutoffFlow_continuous_initial line 100
  6. lemma OAI.SLEExactGauge.LiteralTrace.surviving_eventually_cutoff_height line 110
  7. lemma OAI.SLEExactGauge.LiteralTrace.surviving_eventually_cutoff line 148
  8. lemma OAI.SLEExactGauge.LiteralTrace.isOpen_surviving line 155
  9. lemma OAI.SLEExactGauge.LiteralTrace.flow_continuousAt_initial line 162
  10. lemma OAI.SLEExactGauge.LiteralTrace.complex_linear_formula line 173
  11. lemma OAI.SLEExactGauge.LiteralTrace.surviving_centered_ne_zero line 204
  12. lemma OAI.SLEExactGauge.LiteralTrace.flow_difference_formula line 214
  13. lemma OAI.SLEExactGauge.LiteralTrace.surviving_centered_continuous_clip line 249
  14. def OAI.SLEExactGauge.LiteralTrace.flowDifferenceExponent line 256
  15. lemma OAI.SLEExactGauge.LiteralTrace.flowDifferenceExponent_continuousAt line 261
  16. theorem OAI.SLEExactGauge.LiteralTrace.flow_hasDerivAt_initial line 304
  17. lemma OAI.SLEExactGauge.LiteralTrace.flow_deriv_ne_zero line 322
  18. lemma OAI.SLEExactGauge.LiteralTrace.flow_differentiableOn line 327
  19. lemma OAI.SLEExactGauge.LiteralTrace.flow_hasStrictDerivAt_initial line 337
  20. lemma OAI.SLEExactGauge.LiteralTrace.inverseFlow_hasStrictDerivAt line 342
  21. theorem OAI.SLEExactGauge.LiteralTrace.flow_conformal_bijection line 356
  22. lemma OAI.SLEExactGauge.BrownianCalculus.integral_sq_gaussian line 378
  23. lemma OAI.SLEExactGauge.BrownianCalculus.integral_fourth_gaussian line 384
  24. abbrev OAI.SLEExactGauge.BrownianCalculus.Driver line 424
  25. instance OAI.SLEExactGauge.BrownianCalculus.(instance at line 425) line 425
  26. instance OAI.SLEExactGauge.BrownianCalculus.(instance at line 426) line 426
  27. def OAI.SLEExactGauge.BrownianCalculus.increment line 428
  28. def OAI.SLEExactGauge.BrownianCalculus.history line 430
  29. lemma OAI.SLEExactGauge.BrownianCalculus.measurable_increment line 432
  30. lemma OAI.SLEExactGauge.BrownianCalculus.measurable_history line 437
  31. lemma OAI.SLEExactGauge.BrownianCalculus.increment_law line 443
  32. lemma OAI.SLEExactGauge.BrownianCalculus.increment_mean line 446
  33. lemma OAI.SLEExactGauge.BrownianCalculus.increment_sq line 449
  34. lemma OAI.SLEExactGauge.BrownianCalculus.increment_fourth line 453