OAI/Probability/SLEGauge/LocalFiniteness.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Hausdorff gauges, Loewner evolution and trace measures.

  1. lemma OAI.ExactSLEGreen.actualUpperMass_finiteOnCompacts line 38
  2. def OAI.ExactSLEGreen.upperExtension line 56
  3. lemma OAI.ExactSLEGreen.upperExtension_apply line 59
  4. lemma OAI.ExactSLEGreen.upperExtension_measurable line 62
  5. lemma OAI.ExactSLEGreen.upperExtension_zero line 65
  6. lemma OAI.ExactSLEGreen.actualUpperMass_eval line 74
  7. lemma OAI.ExactSLEGreen.upperExtension_bounded line 96
  8. def OAI.ExactSLEGreen.positive_mass_combination line 104
  9. lemma OAI.ExactSLEGreen.positive_mass_combination_apply line 116
  10. theorem OAI.ExactSLEGreen.actual_radon_mass_extraction line 123
  11. lemma OAI.ExactSLEGreen.radon_le_of_positive_integrals line 182
  12. lemma OAI.ExactSLEGreen.actualUpperMass_mono_time line 208
  13. lemma OAI.ExactSLEGreen.ordered_radon_limits line 220
  14. lemma OAI.ExactSLEGreen.actualUpperMass_eval_measurable line 251
  15. theorem OAI.ExactSLEGreen.actual_ordered_radon_extraction line 259
  16. lemma OAI.ExactSLEGreen.actualMassEval_Lp_bound line 328
  17. lemma OAI.ExactSLEGreen.convex_eLpNorm_bound line 362
  18. lemma OAI.ExactSLEGreen.actualUpperMass_Lp_bound line 387
  19. lemma OAI.ExactSLEGreen.actual_radon_limit_memLp line 405