OAI/Probability/SLEGauge/KernelBounds.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Hausdorff gauges, Loewner evolution and trace measures.

  1. lemma OAI.ExactSLEKernel.kernel_cons_bound line 29
  2. lemma OAI.ExactSLEKernel.singular_ball_finite line 87
  3. lemma OAI.ExactSLEKernel.singular_ball_translate line 102
  4. lemma OAI.ExactSLEKernel.singular_uniform line 109
  5. lemma OAI.ExactSLEKernel.conditional_kernel_bound line 134
  6. lemma OAI.ExactSLEKernel.cap_equiv line 174
  7. lemma OAI.ExactSLEKernel.kernel_equiv line 185
  8. lemma OAI.ExactSLEKernel.kernel_swap_cons line 190
  9. lemma OAI.ExactSLEKernel.lintegral_cons line 202
  10. theorem OAI.ExactSLEKernel.capped_distance_kernel_integral line 218
  11. theorem OAI.ExactSLEKernel.capped_distance_fixed_center line 231
  12. def OAI.ExactSLEGreen.fullRadialDensity line 262
  13. lemma OAI.ExactSLEGreen.fullRadialDensity_bound line 264
  14. lemma OAI.ExactSLEGreen.selective_hit_bound line 276
  15. theorem OAI.ExactSLEGreen.actual_density_product_bound line 316
  16. def OAI.ExactSLEGreen.massDensity line 380
  17. lemma OAI.ExactSLEGreen.massDensity_measurable line 382
  18. lemma OAI.ExactSLEGreen.lintegral_power_pi line 398
  19. lemma OAI.ExactSLEGreen.kernel_top_of_not_injective line 408