OAI/Probability/SLEGauge/KernelMeasurability.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

Hausdorff gauges, Loewner evolution and trace measures.

  1. lemma OAI.ExactSLEGreen.localState_parameter_measurable line 30
  2. lemma OAI.ExactSLEGreen.localState_parameter_joint_measurable line 63
  3. lemma OAI.ExactSLEHitting.boundedContact_parameter_measurable line 74
  4. lemma OAI.ExactSLEGreen.regionStop_parameter_measurable line 96
  5. def OAI.ExactSLEGreen.explicitRadialLocalization line 117
  6. lemma OAI.ExactSLEGreen.localizationApproximation_tendsto line 148
  7. theorem OAI.ExactSLEGreen.joint_radialWeight_measurable line 206
  8. def OAI.ExactSLEKernel.cappedDistance line 267
  9. def OAI.ExactSLEKernel.kernel line 270
  10. lemma OAI.ExactSLEKernel.le_cappedDistance_iff line 276
  11. lemma OAI.ExactSLEKernel.cappedDistance_le line 292
  12. lemma OAI.ExactSLEKernel.cappedDistance_le_dist line 294
  13. lemma OAI.ExactSLEKernel.cappedDistance_pos line 297
  14. lemma OAI.ExactSLEKernel.cappedDistance_nonneg line 307
  15. lemma OAI.ExactSLEKernel.cappedDistance_cons_succ line 310
  16. lemma OAI.ExactSLEKernel.half_cap_unique line 326
  17. lemma OAI.ExactSLEKernel.near_cap_nearest line 336
  18. def OAI.ExactSLEKernel.ipow line 353
  19. lemma OAI.ExactSLEKernel.ipow_anti line 354
  20. lemma OAI.ExactSLEKernel.ipow_pos line 358
  21. lemma OAI.ExactSLEKernel.ipow_finite line 361
  22. lemma OAI.ExactSLEKernel.ipow_mul line 363
  23. lemma OAI.ExactSLEKernel.ipow_twice line 367
  24. lemma OAI.ExactSLEKernel.cap_factor_sup line 370
  25. lemma OAI.ExactSLEKernel.measurable_kernel line 389
  26. lemma OAI.ExactSLEKernel.cap_cons_factor_sum line 404
  27. lemma OAI.ExactSLEKernel.far_cap_factor line 415
  28. lemma OAI.ExactSLEKernel.cap_compensated line 426