OAI/Probability/SLEGauge/GlobalAngleBudget.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

Hausdorff gauges, Loewner evolution and trace measures.

  1. def OAI.ExactSLEGreen.radialTestWeight line 19
  2. lemma OAI.ExactSLEGreen.radialTestWeight_nonneg line 24
  3. lemma OAI.ExactSLEGreen.sinePower_angleLift_pos line 31
  4. lemma OAI.ExactSLEGreen.physicalClock_initial line 35
  5. lemma OAI.ExactSLEGreen.angleBudgetFactor_initial_bound line 40
  6. theorem OAI.ExactSLEGreen.finite_level_angle_budget line 56
  7. theorem OAI.ExactSLEGreen.exists_finite_level_angle_bound line 144
  8. lemma OAI.ExactSLEGreen.localizationStop_eventually_eq line 172
  9. def OAI.ExactSLEGreen.radialState line 202
  10. lemma OAI.ExactSLEGreen.localizedState_eventually_eq line 206
  11. theorem OAI.ExactSLEGreen.joint_radialState_measurable line 238
  12. lemma OAI.ExactSLEGreen.radialTestWeight_eq_mul line 291
  13. lemma OAI.ExactSLEGreen.joint_radialTestWeight_measurable line 296
  14. lemma OAI.ExactSLEGreen.angleLift_sinePower_measurable line 304
  15. def OAI.SLEExactGauge.LoewnerScaling.scaleState line 323
  16. lemma OAI.SLEExactGauge.LoewnerScaling.scaleState_Y line 325
  17. lemma OAI.SLEExactGauge.LoewnerScaling.scaleState_X line 329
  18. lemma OAI.SLEExactGauge.LoewnerScaling.scaleState_Q line 333
  19. lemma OAI.SLEExactGauge.LoewnerScaling.scaleState_J line 338
  20. lemma OAI.SLEExactGauge.LoewnerScaling.scaleState_radius line 340
  21. lemma OAI.SLEExactGauge.LoewnerScaling.scaleState_logGreen line 345
  22. lemma OAI.SLEExactGauge.LoewnerScaling.scaleState_green line 357
  23. lemma OAI.SLEExactGauge.LoewnerScaling.physicalRadius_scaled line 365
  24. lemma OAI.SLEExactGauge.LoewnerScaling.image_radialHits line 373
  25. lemma OAI.SLEExactGauge.LoewnerScaling.radialTime_scaled line 401
  26. lemma OAI.SLEExactGauge.LoewnerScaling.radialTime_scaled_eq_top_iff line 413
  27. lemma OAI.SLEExactGauge.LoewnerScaling.Y_actual_pos line 436
  28. lemma OAI.SLEExactGauge.LoewnerScaling.radialTime_scaled_toNNReal line 442
  29. lemma OAI.SLEExactGauge.LoewnerScaling.radialTime_scaled_le_iff line 449
  30. lemma OAI.SLEExactGauge.LoewnerScaling.radialWeight_scaled line 457
  31. lemma OAI.SLEExactGauge.LoewnerScaling.massDensity_scaled_upper line 475
  32. lemma OAI.SLEExactGauge.LoewnerScaling.timeMassDensity_scaled_upper line 494