OAI/Probability/SLEGauge/TraceBoundary.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

Hausdorff gauges, Loewner evolution and trace measures.

  1. lemma OAI.SLEExactGauge.LiteralTrace.traceRatio_pos line 47
  2. lemma OAI.SLEExactGauge.LiteralTrace.traceRatio_lt_one line 49
  3. lemma OAI.SLEExactGauge.LiteralTrace.traceMeshBase_eq line 52
  4. lemma OAI.SLEExactGauge.LiteralTrace.traceRate_eq line 58
  5. lemma OAI.SLEExactGauge.LiteralTrace.traceMesh_inv line 64
  6. lemma OAI.SLEExactGauge.LiteralTrace.traceHeight_eq line 71
  7. lemma OAI.SLEExactGauge.LiteralTrace.traceGridTime_eq line 77
  8. lemma OAI.SLEExactGauge.LiteralTrace.traceGridCard_eq line 85
  9. lemma OAI.SLEExactGauge.LiteralTrace.traceRate_div line 91
  10. lemma OAI.SLEExactGauge.LiteralTrace.traceMesh_div line 97
  11. lemma OAI.SLEExactGauge.LiteralTrace.traceMesh_eventually line 105
  12. lemma OAI.SLEExactGauge.LiteralTrace.traceError_summable line 115
  13. theorem OAI.SLEExactGauge.LiteralTrace.radial_uniform_bands line 136
  14. lemma OAI.SLEExactGauge.TraceChaining.radial_limit_of_bands line 220
  15. lemma OAI.SLEExactGauge.TraceChaining.radial_uniform_limit_of_bands line 263
  16. theorem OAI.SLEExactGauge.LiteralTrace.trace_limit_all_positive line 300
  17. lemma OAI.SLEExactGauge.LiteralTrace.radial_time_modulus_symmetric line 327
  18. lemma OAI.SLEExactGauge.LiteralTrace.radialValue_continuousOn line 342
  19. theorem OAI.SLEExactGauge.LiteralTrace.trace_continuous_positive line 372
  20. lemma OAI.SLEExactGauge.TraceChaining.initial_le_of_outward_deriv line 424
  21. lemma OAI.SLEExactGauge.LiteralTrace.PositiveSolution.re_hasDeriv line 459