OAI/Probability/SLEGauge/InitialTrace.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

Hausdorff gauges, Loewner evolution and trace measures.

  1. lemma OAI.SLEExactGauge.LiteralTrace.PositiveSolution.initial_abs_re_le line 53
  2. lemma OAI.SLEExactGauge.LiteralTrace.inverseFlow_abs_re_le line 87
  3. lemma OAI.SLEExactGauge.LiteralTrace.radial_limit_early_bound line 96
  4. lemma OAI.SLEExactGauge.LiteralTrace.inverseFlow_zero line 124
  5. lemma OAI.SLEExactGauge.LiteralTrace.trace_zero line 133
  6. lemma OAI.SLEExactGauge.LiteralTrace.trace_limit_zero line 150
  7. lemma OAI.SLEExactGauge.LiteralTrace.trace_continuousWithinAt_zero line 162
  8. lemma OAI.SLEExactGauge.LiteralTrace.surviving_of_le line 204
  9. lemma OAI.SLEExactGauge.LiteralTrace.radial_limit_mem_closure line 208
  10. lemma OAI.SLEExactGauge.LiteralTrace.radial_limit_not_surviving line 217
  11. lemma OAI.SLEExactGauge.LiteralTrace.radial_limit_mem_frontier line 236
  12. theorem OAI.SLEExactGauge.LiteralTrace.trace_countable_boundary line 244
  13. theorem OAI.SLEExactGauge.LiteralTrace.trace_regular_all_times line 262
  14. def OAI.SLEExactGauge.LiteralTrace.unboundedHalfPlaneComponent line 299
  15. lemma OAI.SLEExactGauge.LiteralTrace.inverseFlow_image_upper line 303
  16. lemma OAI.SLEExactGauge.LiteralTrace.isPreconnected_surviving line 313
  17. lemma OAI.SLEExactGauge.LiteralTrace.not_isBounded_surviving line 319
  18. theorem OAI.SLEExactGauge.LiteralTrace.surviving_subset_trace_component line 337
  19. theorem OAI.SLEExactGauge.LiteralTrace.trace_generation_partial line 368
  20. def OAI.SLEExactGauge.LiteralTrace.MissingReverseTraceDomainObligation line 386