OAI/Probability/SLEGauge/TraceMassEndpoint.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

Hausdorff gauges, Loewner evolution and trace measures.

  1. theorem OAI.SLEExactGauge.TraceMassContinuity.actual_raw_mass_trace line 24
  2. lemma OAI.ExactSLEGreen.stoppedSurvivingGreen_spatial_measurable line 183
  3. def OAI.ExactSLEGreen.stoppedSurvivingKernel line 191
  4. instance OAI.ExactSLEGreen.stoppedSurvivingKernel_sfinite line 197
  5. lemma OAI.ExactSLEGreen.stoppedSurvivingKernel_apply line 202
  6. lemma OAI.ExactSLEGreen.stoppedSurvivingKernel_raw_measurable line 209
  7. lemma OAI.ExactSLEGreen.stoppedSurvivingGreen_lintegral_le_initial line 218
  8. theorem OAI.ExactSLEGreen.stoppedSurvivingKernel_average_le_initial line 232
  9. lemma OAI.ExactSLEGreen.stoppedSurvivingKernel_average_finiteOnCompacts line 248
  10. lemma OAI.ExactSLEGreen.stoppedSurvivingKernel_compact_eval line 258
  11. lemma OAI.ExactSLEGreen.stoppedSurvivingKernel_compact_ae_integrable line 268
  12. lemma OAI.ExactSLEGreen.stoppedSurvivingKernel_compact_mean_integrable line 278
  13. def OAI.ExactSLEGreen.unhitMassDensity line 306
  14. lemma OAI.ExactSLEGreen.unhitMassDensity_nonneg line 312
  15. lemma OAI.ExactSLEGreen.timeMassDensity_add_unhit line 320
  16. lemma OAI.ExactSLEGreen.unhitMassDensity_joint_measurable line 331
  17. lemma OAI.ExactSLEGreen.unhitMassDensity_integrable line 342
  18. lemma OAI.ExactSLEGreen.unhitMassDensity_conditional line 351
  19. lemma OAI.ExactSLEGreen.unhitMassDensity_lintegral_conditional line 366
  20. def OAI.ExactSLEGreen.unhitMassKernel line 383
  21. def OAI.ExactSLEGreen.stoppedRemainingKernel line 388
  22. instance OAI.ExactSLEGreen.unhitMassKernel_sfinite line 393
  23. instance OAI.ExactSLEGreen.stoppedRemainingKernel_sfinite line 397
  24. lemma OAI.ExactSLEGreen.unhitMassKernel_apply line 401
  25. lemma OAI.ExactSLEGreen.stoppedRemainingKernel_apply line 408
  26. lemma OAI.ExactSLEGreen.stoppedRemainingKernel_raw_measurable line 415
  27. theorem OAI.ExactSLEGreen.unhitMassKernel_conditional_average line 427
  28. lemma OAI.ExactSLEGreen.stoppedRemainingKernel_le_surviving line 451
  29. lemma OAI.ExactSLEGreen.stoppedRemainingKernel_average_le_surviving line 462
  30. lemma OAI.ExactSLEGreen.stoppedRemainingKernel_average_finiteOnCompacts line 473
  31. lemma OAI.ExactSLEGreen.unhitMassKernel_average_finiteOnCompacts line 484
  32. theorem OAI.ExactSLEGreen.unhitMassKernel_random_test line 497