OAI/Probability/SLEGauge/MassVersionsCore.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

Hausdorff gauges, Loewner evolution and trace measures.

  1. theorem OAI.SLEExactGauge.MassVersions.open_countable_tests line 19
  2. theorem OAI.SLEExactGauge.MassVersions.measurable_measure_of_compact_tests line 62
  3. def OAI.SLEExactGauge.MassVersions.determiningTests line 106
  4. def OAI.SLEExactGauge.MassVersions.TestConverges line 111
  5. lemma OAI.SLEExactGauge.MassVersions.exists_radon_of_testConverges line 114
  6. def OAI.SLEExactGauge.MassVersions.radonLimit line 122
  7. lemma OAI.SLEExactGauge.MassVersions.radonLimit_finite line 126
  8. lemma OAI.SLEExactGauge.MassVersions.radonLimit_regular line 134
  9. lemma OAI.SLEExactGauge.MassVersions.tendsto_radonLimit line 142
  10. lemma OAI.SLEExactGauge.MassVersions.radonLimit_eq line 149
  11. lemma OAI.SLEExactGauge.MassVersions.measurableSet_testConverges line 158
  12. theorem OAI.SLEExactGauge.MassVersions.measurable_radonLimit line 168
  13. theorem OAI.SLEExactGauge.MassVersions.radonLimit_ae_eq line 191
  14. lemma OAI.ExactSLEGreen.level_step_le_one line 211
  15. def OAI.ExactSLEGreen.actualMassFunctionals line 219
  16. lemma OAI.ExactSLEGreen.actualMassFunctionals_apply line 227
  17. def OAI.ExactSLEGreen.recoveredMass line 236
  18. lemma OAI.ExactSLEGreen.recoveredMass_measurable line 241
  19. lemma OAI.ExactSLEGreen.recoveredMass_raw_measurable line 252
  20. theorem OAI.ExactSLEGreen.actual_radon_measurable_conditional line 265
  21. lemma OAI.ExactSLEGreen.timeMassDensity_joint_measurable line 347
  22. lemma OAI.ExactSLEGreen.timeMassDensity_raw_progressive_joint line 371
  23. lemma OAI.ExactSLEGreen.actualMassEval_progressive line 392
  24. lemma OAI.ExactSLEGreen.actualUpperMass_eval_progressive line 403
  25. theorem OAI.ExactSLEGreen.recoveredMass_progressive line 412