OAI/Probability/SLEGauge/AngularControlMass.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

Hausdorff gauges, Loewner evolution and trace measures.

  1. def OAI.ExactSLEGreen.angularDensity line 22
  2. def OAI.ExactSLEGreen.angularCompactMass line 27
  3. lemma OAI.ExactSLEGreen.angularDensity_measurable line 30
  4. lemma OAI.ExactSLEGreen.angularCompactMass_measurable line 39
  5. lemma OAI.ExactSLEGreen.angularInitial_continuous line 42
  6. theorem OAI.ExactSLEGreen.angularCompactMass_uniform_mean line 55
  7. def OAI.ExactSLEGreen.convexAngularMass line 89
  8. lemma OAI.ExactSLEGreen.convexAngularMass_measurable line 93
  9. lemma OAI.ExactSLEGreen.convexAngularMass_mean_bound line 99
  10. theorem OAI.ExactSLEGreen.convexAngularMass_liminf_finite line 115
  11. theorem OAI.ExactSLEGreen.actual_raw_mass_endpoint line 146
  12. def OAI.ExactSLEGreen.localPairMeasure line 223
  13. lemma OAI.ExactSLEGreen.localPairMeasure_finite line 227
  14. lemma OAI.ExactSLEGreen.localPairMeasure_diagonal line 260
  15. theorem OAI.ExactSLEGreen.localized_actualConvexMass_pair_bound line 266
  16. theorem OAI.SLEExactGauge.MassVersions.ae_atomless_of_localizations line 308
  17. theorem OAI.ExactSLEGreen.actual_limit_pair_bound line 346
  18. theorem OAI.ExactSLEGreen.actual_limit_localized_atomless line 390
  19. theorem OAI.ExactSLEGreen.actual_limit_atomless line 410
  20. theorem OAI.ExactSLEGreen.actual_raw_atomless_mass_endpoint line 438