OAI/Probability/SLE/SausageScaling.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

Sausage Scaling for chordal SLE.

  1. lemma OAI.SLEExactGauge.source_sausage_dilation line 15
  2. lemma OAI.SLEExactGauge.source_volume_dilation_lower line 34
  3. lemma OAI.SLEExactGauge.source_sausage_scale_mass_bound line 60
  4. lemma OAI.SLEExactGauge.RegularSLEPresentation.source_uniform_sausage_seed line 78
  5. lemma OAI.SLEExactGauge.source_volume_le_bilip_image line 145
  6. lemma OAI.SLEExactGauge.source_chart_sausage_area line 163
  7. lemma OAI.SLEExactGauge.source_inverse_translated_chart_compact_bounds line 196
  8. lemma OAI.SLEExactGauge.source_restart_sausage_countable_bound line 219
  9. lemma OAI.SLEExactGauge.source_sausage_mono_mesh line 258
  10. def OAI.SLEExactGauge.sourceSausageChartGood line 262
  11. lemma OAI.SLEExactGauge.source_chart_good_mono line 266
  12. lemma OAI.SLEExactGauge.source_chart_good_measurable line 279
  13. lemma OAI.SLEExactGauge.source_chart_good_real_bound line 293
  14. lemma OAI.SLEExactGauge.source_chart_good_high_probability line 305
  15. lemma OAI.SLEExactGauge.source_sausage_mono_interval line 339
  16. lemma OAI.SLEExactGauge.source_sausage_mass_mono_interval line 343
  17. lemma OAI.SLEExactGauge.RegularSLEPresentation.source_sausage_mass_measurable_at line 346
  18. lemma OAI.SLEExactGauge.source_chart_good_mass_bound line 379
  19. lemma OAI.SLEExactGauge.RegularSLEPresentation.source_uniform_sausage_slot_bound line 410
  20. lemma OAI.SLEExactGauge.RegularSLEPresentation.source_sausage_nslot_bound line 512
  21. lemma OAI.SLEExactGauge.RegularSLEPresentation.source_small_sausage line 572
  22. theorem OAI.SLEExactGauge.sourceSmallSausage_proved line 607