OAI/Probability/SLEGauge/TraceRestriction.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

Hausdorff gauges, Loewner evolution and trace measures.

  1. def OAI.SLEExactGauge.TraceRestriction.visited line 22
  2. lemma OAI.SLEExactGauge.TraceRestriction.visited_mono line 26
  3. lemma OAI.SLEExactGauge.TraceRestriction.measurableSet_visited line 30
  4. lemma OAI.SLEExactGauge.TraceRestriction.visited_symmDiff_subset line 38
  5. lemma OAI.SLEExactGauge.TraceRestriction.nnreal_dist_right_le line 49
  6. lemma OAI.SLEExactGauge.TraceRestriction.eventually_not_mem_visited_symmDiff line 58
  7. lemma OAI.SLEExactGauge.TraceRestriction.eventually_visited_iff line 71
  8. lemma OAI.SLEExactGauge.TraceRestriction.preimage_singleton_null_of_injective line 84
  9. lemma OAI.SLEExactGauge.TraceRestriction.tendsto_measure_visited_symmDiff line 100
  10. lemma OAI.SLEExactGauge.TraceRestriction.continuous_integral_visited line 133
  11. def OAI.SLEExactGauge.TraceRestriction.firstVisit line 156
  12. lemma OAI.SLEExactGauge.TraceRestriction.firstVisit_le_iff line 161
  13. lemma OAI.SLEExactGauge.TraceRestriction.firstVisit_lt_top_iff line 178
  14. lemma OAI.SLEExactGauge.TraceRestriction.measurable_firstVisit line 187
  15. lemma OAI.SLEExactGauge.TraceRestriction.iUnion_visited_nat line 203
  16. lemma OAI.SLEExactGauge.TraceRestriction.restrict_sub_restrict line 215
  17. lemma OAI.SLEExactGauge.TraceRestriction.visited_diff_subset line 231
  18. lemma OAI.SLEExactGauge.TraceRestriction.increment_carried_by_segment line 239
  19. lemma OAI.SLEExactGauge.DenseTimeSqueeze.tendsto_of_dense line 268
  20. lemma OAI.SLEExactGauge.DenseTimeSqueeze.tendsto_integral_of_dense line 304
  21. lemma OAI.SLEExactGauge.FirstVisitReconstruction.tendsto_all_times line 361
  22. lemma OAI.SLEExactGauge.FirstVisitReconstruction.radonLimit_all_times line 379
  23. lemma OAI.ExactSLEGreen.actualConvexMass_mono_time line 410
  24. def OAI.SLEExactGauge.TraceMassContinuity.internalTrace line 426
  25. lemma OAI.SLEExactGauge.TraceMassContinuity.continuous_internalTrace line 429
  26. lemma OAI.SLEExactGauge.TraceMassContinuity.internalTrace_image line 433
  27. lemma OAI.SLEExactGauge.TraceMassContinuity.visited_internalTrace line 450
  28. lemma OAI.SLEExactGauge.TraceMassContinuity.actualMass_tendsto_all_times line 457
  29. lemma OAI.SLEExactGauge.TraceMassContinuity.recoveredMass_all_times line 487
  30. lemma OAI.SLEExactGauge.TraceMassContinuity.local_variation_visited line 507