OAI/Probability/SLEGauge/TracePastSupport.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

Hausdorff gauges, Loewner evolution and trace measures.

  1. lemma OAI.SLEExactGauge.TraceLevelLocalization.compact_away_angle_large line 20
  2. lemma OAI.SLEExactGauge.TraceLevelLocalization.angleLift_ge_cot_rpow line 62
  3. lemma OAI.SLEExactGauge.TraceLevelLocalization.timeMassDensity_le_angular line 75
  4. lemma OAI.SLEExactGauge.TraceLevelLocalization.actualUpperMass_ofReal_integral line 116
  5. lemma OAI.SLEExactGauge.TraceLevelLocalization.angularCompactMass_const_mul line 130
  6. lemma OAI.SLEExactGauge.TraceLevelLocalization.actualUpperMass_integral_le_angular line 141
  7. theorem OAI.SLEExactGauge.TraceLevelLocalization.actual_limit_integral_zero_away_trace line 175
  8. lemma OAI.SLEExactGauge.MassVersions.open_null_of_nonneg_compact_tests line 231
  9. theorem OAI.SLEExactGauge.TraceLevelLocalization.actual_limit_past_trace_support line 259
  10. def OAI.SLEExactGauge.LoewnerScaling.upperDilation line 297
  11. lemma OAI.SLEExactGauge.LoewnerScaling.upperDilation_apply line 314
  12. lemma OAI.SLEExactGauge.LoewnerScaling.upperDilation_symm_apply line 317
  13. lemma OAI.SLEExactGauge.LoewnerScaling.upperDilation_symm line 320
  14. lemma OAI.SLEExactGauge.LoewnerScaling.map_upperArea line 325
  15. lemma OAI.SLEExactGauge.LoewnerScaling.map_withDensity_comp line 358
  16. lemma OAI.SLEExactGauge.LoewnerScaling.scaling_factor line 381
  17. lemma OAI.SLEExactGauge.LoewnerScaling.map_actualUpperMass_scaled line 388
  18. lemma OAI.SLEExactGauge.LoewnerScaling.map_actualConvexMass_scaled line 409
  19. lemma OAI.SLEExactGauge.MassVersions.compact_comp_symm_comp line 444
  20. lemma OAI.SLEExactGauge.MassVersions.testConverges_equiv line 452
  21. theorem OAI.SLEExactGauge.MassVersions.radonLimit_equiv line 473
  22. lemma OAI.SLEExactGauge.LoewnerScaling.actualMassFunctionals_integral line 511
  23. lemma OAI.SLEExactGauge.LoewnerScaling.actualMassFunctionals_scaled line 517
  24. theorem OAI.SLEExactGauge.LoewnerScaling.map_recoveredMass_scaled line 532
  25. theorem OAI.SLEExactGauge.LoewnerScaling.recoveredMass_scaled line 543
  26. lemma OAI.SLEExactGauge.LoewnerScaling.recoveredMass_scaled_univ_pos_iff line 554
  27. theorem OAI.SLEExactGauge.LoewnerScaling.recoveredMass_positivity_probability line 568