OAI/Probability/SLE/WindowAssembly.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

Window Assembly for chordal SLE.

  1. lemma OAI.SLEExactGauge.window_prod_telescope line 12
  2. lemma OAI.SLEExactGauge.window_integrable_bounded line 42
  3. lemma OAI.SLEExactGauge.window_exp_secant line 47
  4. lemma OAI.SLEExactGauge.window_weighted_cond_mean line 66
  5. lemma OAI.SLEExactGauge.window_weighted_hoeffding line 79
  6. def OAI.SLEExactGauge.windowBefore line 118
  7. lemma OAI.SLEExactGauge.window_prod_before line 122
  8. lemma OAI.SLEExactGauge.window_before_measurable line 144
  9. lemma OAI.SLEExactGauge.window_measurable_on_event line 158
  10. lemma OAI.SLEExactGauge.window_integrable_nonneg line 183
  11. lemma OAI.SLEExactGauge.window_weighted_normalized line 189
  12. lemma OAI.SLEExactGauge.window_finite_mgf line 212
  13. structure OAI.SLEExactGauge.SourceDisjointWindows line 307
  14. lemma OAI.SLEExactGauge.window_cond_mean_at_infinity line 337
  15. lemma OAI.SLEExactGauge.window_capped_cond_mean line 362
  16. lemma OAI.SLEExactGauge.window_geometric_order line 385
  17. lemma OAI.SLEExactGauge.window_source_finite_mgf line 413
  18. lemma OAI.SLEExactGauge.window_integral_grid_1d line 468
  19. def OAI.SLEExactGauge.windowSquare line 496
  20. instance OAI.SLEExactGauge.windowSquare_finite line 499
  21. lemma OAI.SLEExactGauge.window_grid_2d line 503
  22. def OAI.SLEExactGauge.windowShiftLaw line 539
  23. lemma OAI.SLEExactGauge.windowSquare_mass line 542
  24. lemma OAI.SLEExactGauge.windowShiftLaw_probability line 545
  25. lemma OAI.SLEExactGauge.window_rectangle_integral line 550
  26. def OAI.SLEExactGauge.windowCenter line 568
  27. lemma OAI.SLEExactGauge.window_grid_average line 571
  28. lemma OAI.SLEExactGauge.window_nat_spacing line 585
  29. lemma OAI.SLEExactGauge.window_centers_separated line 597
  30. lemma OAI.SLEExactGauge.window_choose_grid line 617
  31. lemma OAI.SLEExactGauge.window_jensen_mgf line 634
  32. lemma OAI.SLEExactGauge.window_source_mgf_pos line 681
  33. lemma OAI.SLEExactGauge.window_source_integral_measurable line 746
  34. lemma OAI.SLEExactGauge.window_source_integral_bounded line 755
  35. lemma OAI.SLEExactGauge.window_source_mgf line 772
  36. lemma OAI.SLEExactGauge.window_source_tail line 802