OAI/Probability/SLE/MainReduction.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Main Reduction for chordal SLE.

  1. def OAI.SLEExactGauge.FiniteExpectedWholeTrace line 46
  2. lemma OAI.SLEExactGauge.integerRectangle_subset_closedBall line 51
  3. lemma OAI.SLEExactGauge.trace_inter_bounded_lt_top_of_integer_balls line 64
  4. lemma OAI.SLEExactGauge.segment_lt_top_of_integer_balls line 78
  5. lemma OAI.SLEExactGauge.mainEvent_of_integer_balls line 91
  6. lemma OAI.SLEExactGauge.ae_integer_balls_lt_top_of_finiteExpectation line 108
  7. theorem OAI.SLEExactGauge.mainConclusion_of_lower_and_finiteExpectation line 123
  8. lemma OAI.SLEExactGauge.finiteExpectedWholeTrace_of_mainConclusion line 142
  9. lemma OAI.SLEExactGauge.finiteExpectedWholeTrace_iff_integer_balls line 152
  10. theorem OAI.SLEExactGauge.mainConclusion_iff_finiteExpectedWholeTrace line 179