OAI/Probability/SLEGauge/ReverseFlow.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

Hausdorff gauges, Loewner evolution and trace measures.

  1. lemma OAI.SLEExactGauge.LiteralTrace.forward_integral_eq_reverse line 45
  2. theorem OAI.SLEExactGauge.LiteralTrace.inverseFlow_deriv_norm_eq_reverse line 75
  3. lemma OAI.SLEExactGauge.LiteralTrace.measurable_reverse_log line 89
  4. lemma OAI.SLEExactGauge.LiteralTrace.measurable_inverse_deriv_norm line 95
  5. theorem OAI.SLEExactGauge.LiteralTrace.inverse_deriv_moment line 102
  6. lemma OAI.SLEExactGauge.LiteralTrace.lambda_gt_one line 126
  7. lemma OAI.SLEExactGauge.LiteralTrace.inverse_deriv_first_moment line 131
  8. def OAI.SLEExactGauge.LiteralTrace.radialCoeff line 165
  9. lemma OAI.SLEExactGauge.LiteralTrace.continuousOn_radialCoeff line 168
  10. lemma OAI.SLEExactGauge.LiteralTrace.measurable_positive_radial_norm line 179
  11. lemma OAI.SLEExactGauge.LiteralTrace.measurable_radial_norm line 195
  12. lemma OAI.SLEExactGauge.LiteralTrace.radial_length_ae_finite line 224
  13. lemma OAI.SLEExactGauge.LiteralTrace.measurable_radialCoeff line 250
  14. lemma OAI.SLEExactGauge.LiteralTrace.hasDerivAt_radial line 262
  15. lemma OAI.SLEExactGauge.LiteralTrace.radial_limit_of_integrable line 271
  16. theorem OAI.SLEExactGauge.LiteralTrace.radial_limit_ae line 305
  17. theorem OAI.SLEExactGauge.LiteralTrace.trace_limit_countable line 316
  18. def OAI.SLEExactGauge.LiteralTrace.traceBeta line 334
  19. def OAI.SLEExactGauge.LiteralTrace.traceEta line 337
  20. lemma OAI.SLEExactGauge.LiteralTrace.trace_exponents line 339
  21. lemma OAI.SLEExactGauge.LiteralTrace.inverse_deriv_moment_away line 357
  22. lemma OAI.SLEExactGauge.LiteralTrace.inverse_deriv_tail_away line 381
  23. lemma OAI.SLEExactGauge.LiteralTrace.inverse_deriv_beta_tail line 407
  24. lemma OAI.SLEExactGauge.LiteralTrace.lintegral_pow_le_mass line 423
  25. def OAI.SLEExactGauge.LiteralTrace.radialLength line 445