OAI/Probability/SLE/WindowTails.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Window Tails for chordal SLE.

  1. def OAI.SLEExactGauge.SourceSpatialConditionalMeanTarget line 19
  2. lemma OAI.SLEExactGauge.spatialHitTime_antitone_radius line 32
  3. lemma OAI.SLEExactGauge.source_nested_stops_condExp line 42
  4. theorem OAI.SLEExactGauge.sourceSpatialConditionalMean_proved line 163
  5. lemma OAI.SLEExactGauge.source_condExp_le_changed_stop line 265
  6. lemma OAI.SLEExactGauge.source_windowHB_range line 301
  7. lemma OAI.SLEExactGauge.source_windowHB_zero line 307
  8. lemma OAI.SLEExactGauge.source_windowH_le_indicator line 314
  9. lemma OAI.SLEExactGauge.source_window_origin_bound line 335
  10. lemma OAI.SLEExactGauge.source_window_change_live_mean line 342
  11. lemma OAI.SLEExactGauge.source_window_weight_zero line 370
  12. lemma OAI.SLEExactGauge.source_windowH_integrable line 378
  13. lemma OAI.SLEExactGauge.source_windowV_integrable_le line 390
  14. lemma OAI.SLEExactGauge.source_windowH_mean_of_raw line 436
  15. lemma OAI.SLEExactGauge.source_windowV_mean line 468
  16. lemma OAI.SLEExactGauge.source_window_HV_mean line 505