OAI/Probability/SLEGauge/RadonKernels.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

Hausdorff gauges, Loewner evolution and trace measures.

  1. theorem OAI.SLEExactGauge.MassVersions.isSFiniteKernel_of_pointwise_finite line 19
  2. theorem OAI.SLEExactGauge.MassVersions.isSFiniteKernel_of_locally_finite line 51
  3. theorem OAI.SLEExactGauge.MassVersions.average_finiteOnCompacts line 75
  4. lemma OAI.SLEExactGauge.MassVersions.average_integrable_compact_test line 92
  5. lemma OAI.SLEExactGauge.MassVersions.average_compact_eval line 101
  6. theorem OAI.SLEExactGauge.MassVersions.average_eq_of_compact_tests line 114
  7. lemma OAI.SLEExactGauge.MassVersions.prod_sigma_le line 129
  8. theorem OAI.SLEExactGauge.MassVersions.conditional_product_eq_of_compact_tests line 135
  9. theorem OAI.SLEExactGauge.MassVersions.conditional_lintegral_eq_of_compact_tests line 179
  10. lemma OAI.SLEExactGauge.MassVersions.average_mono line 209
  11. lemma OAI.SLEExactGauge.MassVersions.average_restrict_finite line 217
  12. lemma OAI.SLEExactGauge.MassVersions.average_compact_eval_of_average_finite line 226
  13. theorem OAI.SLEExactGauge.MassVersions.conditional_product_eq_of_average_finite line 235
  14. theorem OAI.SLEExactGauge.MassVersions.conditional_lintegral_eq_of_average_finite line 275
  15. lemma OAI.SLEExactGauge.MassVersions.finiteOnCompacts_of_integrable_tests line 299
  16. lemma OAI.SLEExactGauge.MassVersions.average_add line 310
  17. instance OAI.ExactSLEGreen.upperArea_finiteOnCompacts line 326
  18. lemma OAI.ExactSLEGreen.survivingGreen_joint_measurable line 332
  19. lemma OAI.ExactSLEGreen.survivingGreen_spatial_measurable line 336
  20. def OAI.ExactSLEGreen.survivingKernel line 341
  21. instance OAI.ExactSLEGreen.survivingKernel_sfinite line 346
  22. lemma OAI.ExactSLEGreen.survivingKernel_apply line 350
  23. lemma OAI.ExactSLEGreen.survivingKernel_compact_eval line 354
  24. lemma OAI.ExactSLEGreen.surviving_compact_spatial_integrable line 362
  25. lemma OAI.ExactSLEGreen.survivingKernel_compact_mean_integrable line 378
  26. lemma OAI.ExactSLEGreen.survivingKernel_compact_ae_integrable line 389
  27. lemma OAI.ExactSLEGreen.survivingKernel_average_compact_integrable line 403
  28. lemma OAI.ExactSLEGreen.survivingKernel_average_finiteOnCompacts line 418
  29. theorem OAI.ExactSLEGreen.compact_conditional_to_random_tests line 426
  30. theorem OAI.ExactSLEGreen.actual_raw_mass_extraction line 494