OAI/Probability/SLE/TracePosCombined.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

Trace Pos Combined for chordal SLE.

  1. lemma OAI.SLEExactGauge.source_gauge_cost_nonempty line 15
  2. lemma OAI.SLEExactGauge.source_gauge_cover_formula line 22
  3. lemma OAI.SLEExactGauge.source_gauge_open_enlargement line 28
  4. def OAI.SLEExactGauge.sourceFiniteOpenCover line 59
  5. lemma OAI.SLEExactGauge.source_null_compact_finite_open_cover line 64
  6. def OAI.SLEExactGauge.sourceFineGaugeContent line 107
  7. lemma OAI.SLEExactGauge.source_fine_content_finite_cover line 110
  8. def OAI.SLEExactGauge.sourceCoverScale line 132
  9. lemma OAI.SLEExactGauge.source_coverScale_pos line 133
  10. lemma OAI.SLEExactGauge.source_coverScale_tendsto line 136
  11. lemma OAI.SLEExactGauge.source_compact_gauge_null_criterion line 141
  12. lemma OAI.SLEExactGauge.source_finite_open_cover_trace_isOpen line 167
  13. def OAI.SLEExactGauge.SourceTracePositiveMeasurableTarget line 188
  14. theorem OAI.SLEExactGauge.sourceTracePositiveMeasurable_proved line 191
  15. lemma OAI.SLEExactGauge.source_dilation_gauge_positive line 220
  16. lemma OAI.SLEExactGauge.RegularSLEPresentation.source_trace_path_measurable line 236
  17. lemma OAI.SLEExactGauge.RegularSLEPresentation.source_scale_trace_law line 244
  18. def OAI.SLEExactGauge.SourceUniformInteriorSeedTarget line 259
  19. theorem OAI.SLEExactGauge.sourceUniformInteriorSeed_proved line 268
  20. lemma OAI.SLEExactGauge.source_translation_gauge_positive line 329
  21. lemma OAI.SLEExactGauge.source_restart_segment_positive line 345
  22. lemma OAI.SLEExactGauge.RegularSLEPresentation.source_segment_positive_measurable_at line 368
  23. lemma OAI.SLEExactGauge.RegularSLEPresentation.source_segment_null_measurable_at line 392
  24. lemma OAI.SLEExactGauge.RegularSLEPresentation.source_uniform_null_slot_bound line 399
  25. lemma OAI.SLEExactGauge.RegularSLEPresentation.source_positive_fixed_interval line 475
  26. lemma OAI.SLEExactGauge.RegularSLEPresentation.source_positive_all_intervals line 529
  27. def OAI.SLEExactGauge.SourceLowerAllIntervalsTarget line 557
  28. theorem OAI.SLEExactGauge.sourceLowerAllIntervals_proved line 564
  29. def OAI.SLEExactGauge.sourceSausageSet line 580
  30. def OAI.SLEExactGauge.sourceSausageMass line 582
  31. def OAI.SLEExactGauge.SourceSmallSausageTarget line 586
  32. lemma OAI.SLEExactGauge.source_sausage_isOpen line 600
  33. lemma OAI.SLEExactGauge.source_sausage_joint_open line 606
  34. lemma OAI.SLEExactGauge.source_sausage_local_volume_measurable line 615
  35. lemma OAI.SLEExactGauge.source_sausage_mass_measurable line 627
  36. lemma OAI.SLEExactGauge.source_second_moment_seed line 640
  37. lemma OAI.SLEExactGauge.RegularSLEPresentation.source_finite_mass_le_sausage line 707
  38. lemma OAI.SLEExactGauge.RegularSLEPresentation.source_positive_probability_initial_sausage line 731
  39. lemma OAI.SLEExactGauge.source_volume_lipschitz_image line 774
  40. lemma OAI.SLEExactGauge.source_holomorphic_compact_lipschitz line 788
  41. lemma OAI.SLEExactGauge.source_inverse_chart_compact_bilipschitz line 795