OAI/Probability/SLEGauge/HalfPlaneDistortion.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

Hausdorff gauges, Loewner evolution and trace measures.

  1. lemma OAI.SLEExactGauge.LoewnerGeometry.lineMap_im_lower line 18
  2. lemma OAI.SLEExactGauge.LoewnerGeometry.lineMap_hasDerivAt_complex_comp line 26
  3. lemma OAI.SLEExactGauge.LoewnerGeometry.norm_exp_bound_on_halfPlane_segment line 36
  4. theorem OAI.SLEExactGauge.LoewnerGeometry.inverseMap_deriv_segment_bound line 67
  5. theorem OAI.SLEExactGauge.LoewnerGeometry.inverseMap_deriv_two_sided line 77
  6. lemma OAI.SLEExactGauge.LoewnerGeometry.im_lower_of_mem_closedBall line 107
  7. lemma OAI.SLEExactGauge.LoewnerGeometry.smallBall_im_half line 114
  8. lemma OAI.SLEExactGauge.LoewnerGeometry.inverseMap_deriv_smallBall_bound line 119
  9. lemma OAI.SLEExactGauge.LoewnerGeometry.inverseMap_second_deriv_smallBall_bound line 132
  10. lemma OAI.SLEExactGauge.LoewnerGeometry.inverseMap_deriv_close_on_smallBall line 144
  11. lemma OAI.SLEExactGauge.LoewnerGeometry.inverseMap_approximates_smallBall line 166
  12. def OAI.SLEExactGauge.LoewnerGeometry.spanRightInverse line 192
  13. theorem OAI.SLEExactGauge.LoewnerGeometry.inverseMap_inner_ball line 201
  14. def OAI.SLEExactGauge.LoewnerGeometry.diskAt line 234
  15. def OAI.SLEExactGauge.LoewnerGeometry.centeredRegion line 236
  16. def OAI.SLEExactGauge.LoewnerGeometry.subdiskReach line 238
  17. def OAI.SLEExactGauge.LoewnerGeometry.subdiskHeight line 239
  18. def OAI.SLEExactGauge.LoewnerGeometry.subdiskDistortion line 240
  19. lemma OAI.SLEExactGauge.LoewnerGeometry.subdiskReach_nonneg line 242
  20. lemma OAI.SLEExactGauge.LoewnerGeometry.subdiskHeight_pos line 245
  21. lemma OAI.SLEExactGauge.LoewnerGeometry.subdiskHeight_le_one line 248
  22. lemma OAI.SLEExactGauge.LoewnerGeometry.subdiskDistortion_pos line 251
  23. lemma OAI.SLEExactGauge.LoewnerGeometry.subdiskDistortion_ge_one line 252
  24. lemma OAI.SLEExactGauge.LoewnerGeometry.diskAt_denominator_ne line 257
  25. lemma OAI.SLEExactGauge.LoewnerGeometry.diskAt_affine line 263
  26. lemma OAI.SLEExactGauge.LoewnerGeometry.centeredRegion_bounds line 275
  27. lemma OAI.SLEExactGauge.LoewnerGeometry.smallBall_subset_centeredRegion line 296
  28. lemma OAI.SLEExactGauge.LoewnerGeometry.centeredRegion_deriv_bounds line 314
  29. lemma OAI.SLEExactGauge.LoewnerGeometry.centeredRegion_image_bound line 329
  30. theorem OAI.SLEExactGauge.LoewnerGeometry.inverseMap_centered_localization line 370
  31. lemma OAI.SLEExactGauge.LoewnerGeometry.diskAt_hasDerivAt line 381
  32. lemma OAI.SLEExactGauge.LoewnerGeometry.diskAt_deriv_norm line 390
  33. lemma OAI.SLEExactGauge.LoewnerGeometry.diskAt_deriv_bound line 396
  34. theorem OAI.SLEExactGauge.LoewnerGeometry.centered_disk_deriv_ratio line 428
  35. lemma OAI.SLEExactGauge.LoewnerGeometry.centered_im_pos line 464
  36. lemma OAI.SLEExactGauge.LoewnerGeometry.inverseMap_spatial_radius line 468
  37. theorem OAI.SLEExactGauge.LoewnerGeometry.radius_ball_subset_alive line 480
  38. theorem OAI.SLEExactGauge.LoewnerGeometry.centered_localization_at_alive line 492