OAI/Probability/SLEGauge/RadonMoments.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

Hausdorff gauges, Loewner evolution and trace measures.

  1. theorem OAI.ExactSLEGreen.actual_radon_all_moments line 38
  2. lemma OAI.ExactSLEGreen.unifIntegrable_of_L2_bound line 72
  3. lemma OAI.ExactSLEGreen.actual_radon_limit_L1 line 102
  4. theorem OAI.ExactSLEGreen.actual_radon_L1_convergence line 135
  5. lemma OAI.ExactSLEGreen.actualMassEval_joint_integrable line 179
  6. lemma OAI.ExactSLEGreen.terminal_density_mean line 204
  7. lemma OAI.ExactSLEGreen.actualMassEval_terminal_mean line 219
  8. lemma OAI.ExactSLEGreen.actualUpperMass_terminal_mean line 235
  9. lemma OAI.ExactSLEGreen.actual_radon_limit_mean line 258
  10. theorem OAI.ExactSLEGreen.actual_radon_terminal_mean line 298
  11. def OAI.ExactSLEGenerator.pastDriver line 336
  12. lemma OAI.ExactSLEGenerator.pastDriver_eq line 338
  13. lemma OAI.ExactSLEGenerator.pastDriver_raw_measurable line 340
  14. lemma OAI.ExactSLEMain.odeUntil_driver_congr line 361
  15. lemma OAI.ExactSLEMain.alive_driver_congr line 366
  16. lemma OAI.ExactSLEMain.loewnerMap_driver_congr line 370
  17. lemma OAI.ExactSLEGreen.actualState_driver_congr line 383
  18. lemma OAI.ExactSLEGreen.radialTime_driver_congr_before line 386
  19. lemma OAI.ExactSLEGreen.timeMassDensity_driver_congr line 412
  20. lemma OAI.ExactSLEGreen.timeMassDensity_past_eq line 437
  21. lemma OAI.ExactSLEGreen.rawPastPair_measurable line 444
  22. theorem OAI.ExactSLEGreen.timeMassDensity_raw_joint line 451