OAI/Probability/SLEGauge/RadialMeasurability.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

Hausdorff gauges, Loewner evolution and trace measures.

  1. theorem OAI.ExactSLEGreen.joint_radialTime_measurable line 34
  2. theorem OAI.ExactSLEGreen.joint_radial_approximant_measurable line 119
  3. def OAI.ExactSLEGreen.timeMassDensity line 132
  4. def OAI.ExactSLEGreen.actualMassEval line 135
  5. lemma OAI.ExactSLEGreen.timeMassDensity_le line 138
  6. lemma OAI.ExactSLEGreen.timeMassDensity_measurable line 143
  7. lemma OAI.ExactSLEGreen.actualMassEval_measurable line 160
  8. lemma OAI.ExactSLEGreen.actualMassEval_enorm_bound line 168
  9. lemma OAI.ExactSLEGreen.actualMassEval_L2_bound line 180
  10. theorem OAI.ExactSLEGreen.actualMassEval_integrable line 213
  11. theorem OAI.ExactSLEGreen.actual_common_mass_extraction line 241
  12. theorem OAI.ExactSLEMassExtraction.supported_dense_tests line 297
  13. theorem OAI.ExactSLEMassExtraction.cutoff_test line 329
  14. theorem OAI.ExactSLEMassExtraction.positive_map_error line 337
  15. theorem OAI.ExactSLEMassExtraction.determining_tests_radon_limit line 358
  16. abbrev OAI.ExactSLEGreen.UpperPlane line 424
  17. def OAI.ExactSLEGreen.upperArea line 425
  18. def OAI.ExactSLEGreen.actualUpperMass line 426
  19. lemma OAI.ExactSLEGreen.upperPlane_open line 428
  20. instance OAI.ExactSLEGreen.upperPlane_locallyCompact line 430
  21. lemma OAI.ExactSLEGreen.upper_embedding line 433
  22. lemma OAI.ExactSLEGreen.upper_compact_lower line 436
  23. lemma OAI.ExactSLEGreen.timeMassDensity_finite line 444
  24. lemma OAI.ExactSLEGreen.timeMassDensity_local_bound line 450