OAI/Probability/SLEGauge/PastHullSupport.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

Hausdorff gauges, Loewner evolution and trace measures.

  1. lemma OAI.ExactSLEGreen.fullLoewnerRadius_continuousOn line 19
  2. lemma OAI.ExactSLEGreen.physicalRadius_actual_continuousOn line 28
  3. lemma OAI.ExactSLEGreen.surviving_compact_radius_margin line 38
  4. lemma OAI.ExactSLEGreen.timeMassDensity_zero_of_radius_lt line 54
  5. lemma OAI.ExactSLEGreen.timeMassDensity_eventually_zero_on_surviving_compact line 72
  6. lemma OAI.ExactSLEGreen.actualUpperMass_eval_eventually_zero_on_surviving line 83
  7. lemma OAI.ExactSLEGreen.mass_levels_tendsto_zero line 102
  8. lemma OAI.ExactSLEGreen.actual_limit_integral_zero_on_surviving line 114
  9. lemma OAI.SLEExactGauge.MassVersions.open_null_of_compact_tests line 138
  10. theorem OAI.ExactSLEGreen.actual_limit_past_hull_support line 165
  11. def OAI.SLEExactGauge.TraceLevelLocalization.AngularRegular line 193
  12. lemma OAI.SLEExactGauge.TraceLevelLocalization.angularRegular_ae line 201
  13. lemma OAI.SLEExactGauge.TraceLevelLocalization.inverse_actual_state line 205
  14. theorem OAI.SLEExactGauge.TraceLevelLocalization.level_near_trace line 231
  15. lemma OAI.SLEExactGauge.MassVersions.sub_add_cancel_of_locally_finite line 302
  16. lemma OAI.SLEExactGauge.MassVersions.restriction_of_complementary_support line 313
  17. theorem OAI.ExactSLEGreen.actual_raw_mass_hull_accounting line 330
  18. lemma OAI.SLEExactGauge.TraceMassIntegration.a_gt_quarter line 410
  19. lemma OAI.SLEExactGauge.TraceMassIntegration.past_trace_subset_dead line 418
  20. theorem OAI.SLEExactGauge.TraceMassIntegration.actual_mass_remaining_avoids_past line 435