OAI/Probability/SLE/HausdorffLimits.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

Hausdorff Limits for chordal SLE.

  1. def OAI.SLEExactGauge.retainedThreshold line 15
  2. def OAI.SLEExactGauge.excessiveSquares line 18
  3. def OAI.SLEExactGauge.retainedMeasure line 23
  4. def OAI.SLEExactGauge.SourceRetainedConstructionTarget line 28
  5. lemma OAI.SLEExactGauge.excessiveSquares_measurable line 53
  6. lemma OAI.SLEExactGauge.excessiveSquares_prod_measurable line 70
  7. lemma OAI.SLEExactGauge.retainedMeasure_measurable line 92
  8. lemma OAI.SLEExactGauge.retainedMeasure_square_bound line 103
  9. def OAI.SLEExactGauge.SourceRetainedBadSquareTarget line 122
  10. lemma OAI.SLEExactGauge.truncated_stretched_tail line 136
  11. theorem OAI.SLEExactGauge.sourceRetainedBadSquare line 198
  12. lemma OAI.SLEExactGauge.retained_total_bound line 236
  13. def OAI.SLEExactGauge.retainedBadSquareMass line 253
  14. lemma OAI.SLEExactGauge.retainedBadSquareMass_measurable line 258
  15. lemma OAI.SLEExactGauge.retained_removed_bound line 264
  16. lemma OAI.SLEExactGauge.retained_removed_expectation_bound line 295
  17. lemma OAI.SLEExactGauge.retainedBadSquareMass_expectation line 308
  18. lemma OAI.SLEExactGauge.retained_choose_D line 339
  19. lemma OAI.SLEExactGauge.retained_finite_power_tail line 352
  20. lemma OAI.SLEExactGauge.retained_level_sum_bound line 376
  21. lemma OAI.SLEExactGauge.retained_mass_add_removed line 391
  22. lemma OAI.SLEExactGauge.retained_first_moment line 398
  23. lemma OAI.SLEExactGauge.retained_positive_probability line 420
  24. lemma OAI.SLEExactGauge.retained_limsup_probability line 448
  25. theorem OAI.SLEExactGauge.sourceRetainedConstruction line 473
  26. structure OAI.SLEExactGauge.IsGauge line 544

    Also declared: ComparatorChallenges/SLELowerPositivity.lean:50 (same declaration text).

  27. def OAI.SLEExactGauge.hFormula line 550

    Also declared: ComparatorChallenges/SLELowerPositivity.lean:56 (same declaration text).

  28. def OAI.SLEExactGauge.gFormula line 553
  29. def OAI.SLEExactGauge.HasSmallRadiusFormula line 557

    Also declared: ComparatorChallenges/SLELowerPositivity.lean:59 (same declaration text).

  30. def OAI.SLEExactGauge.extendedGauge line 561

    Also declared: ComparatorChallenges/SLELowerPositivity.lean:62 (same declaration text).

  31. def OAI.SLEExactGauge.hausdorffGauge line 565

    Also declared: ComparatorChallenges/SLELowerPositivity.lean:65 (same declaration text).

  32. def OAI.SLEExactGauge.SourceRetainedDyadicTarget line 569
  33. lemma OAI.SLEExactGauge.normalized_supported_probability_compact line 585
  34. lemma OAI.SLEExactGauge.probability_limit_ball_bound line 597
  35. lemma OAI.SLEExactGauge.probability_limit_shrinking_carriers line 605
  36. lemma OAI.SLEExactGauge.gauge_mass_distribution line 635
  37. theorem OAI.SLEExactGauge.retained_compact_mass_lower_bound line 682
  38. theorem OAI.SLEExactGauge.retained_compact_mass_lower_bound_of_frequently line 738
  39. lemma OAI.SLEExactGauge.source_gauge_bounded_scaling line 759
  40. def OAI.SLEExactGauge.retainedBallSquares line 802
  41. lemma OAI.SLEExactGauge.retainedBallSquares_card line 806
  42. lemma OAI.SLEExactGauge.retainedBallSquares_cover line 815
  43. lemma OAI.SLEExactGauge.retained_dyadic_ball_bound line 849
  44. lemma OAI.SLEExactGauge.dyadic_side_rpow line 860
  45. lemma OAI.SLEExactGauge.dyadic_side_loglog line 864
  46. lemma OAI.SLEExactGauge.retained_threshold_gauge_eventually line 873
  47. theorem OAI.SLEExactGauge.sourceRetainedDyadic_proved line 907