OAI/Probability/SLEGauge/RadialMoments.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

Hausdorff gauges, Loewner evolution and trace measures.

  1. lemma OAI.SLEExactGauge.LiteralTrace.radial_length_moment line 44
  2. lemma OAI.SLEExactGauge.LiteralTrace.measurable_radialLength line 101
  3. lemma OAI.SLEExactGauge.LiteralTrace.radial_length_beta_tail line 105
  4. lemma OAI.SLEExactGauge.LiteralTrace.refined_ratio line 135
  5. lemma OAI.SLEExactGauge.LiteralTrace.refined_sum_term line 145
  6. def OAI.SLEExactGauge.LiteralTrace.refinedHeight line 154
  7. def OAI.SLEExactGauge.LiteralTrace.refinedGridTime line 156
  8. lemma OAI.SLEExactGauge.LiteralTrace.refinedGridTime_ge line 158
  9. def OAI.SLEExactGauge.LiteralTrace.radialGridBad line 162
  10. lemma OAI.SLEExactGauge.LiteralTrace.radialGridBad_measure line 167
  11. lemma OAI.SLEExactGauge.LiteralTrace.radialGridBad_summable line 189
  12. theorem OAI.SLEExactGauge.LiteralTrace.radial_length_refined_eventually line 203
  13. theorem OAI.SLEExactGauge.LiteralTrace.radial_length_all_refined_grids line 218
  14. lemma OAI.SLEExactGauge.LiteralTrace.radial_increment_le line 244
  15. lemma OAI.SLEExactGauge.LiteralTrace.halfPlane_sub_conj_ne_zero line 268
  16. lemma OAI.SLEExactGauge.LiteralTrace.halfPlane_disk_norm_lt_one line 275
  17. lemma OAI.SLEExactGauge.LiteralTrace.halfPlane_self_sub_conj_norm line 285
  18. lemma OAI.SLEExactGauge.LiteralTrace.ball_radius_le_conformal_radius line 295
  19. lemma OAI.SLEExactGauge.LiteralTrace.PositiveSolution.im_hasDeriv line 323
  20. lemma OAI.SLEExactGauge.LiteralTrace.PositiveSolution.im_antitone line 332
  21. lemma OAI.SLEExactGauge.LiteralTrace.PositiveSolution.im_sq_bound line 344
  22. lemma OAI.SLEExactGauge.LiteralTrace.inverseFlow_im_sq_bound line 368
  23. lemma OAI.SLEExactGauge.LiteralTrace.inverseFlow_im_pos line 375
  24. lemma OAI.SLEExactGauge.LiteralTrace.inverseFlow_deriv_absolute line 380
  25. lemma OAI.SLEExactGauge.LiteralTrace.PositiveSolution.displacement_le line 402
  26. lemma OAI.SLEExactGauge.LiteralTrace.inverseFlow_im_le line 420
  27. lemma OAI.SLEExactGauge.LiteralTrace.inverseFlow_lipschitz_strip line 433