OAI/Probability/SLE/SausageCharge.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Sausage Charge for chordal SLE.

  1. def OAI.SLEExactGauge.wholeSausageSet line 49
  2. def OAI.SLEExactGauge.wholeSausageCharge line 53
  3. lemma OAI.SLEExactGauge.wholeSausageSet_isOpen line 56
  4. lemma OAI.SLEExactGauge.wholeSausage_joint_open line 64
  5. lemma OAI.SLEExactGauge.wholeSausageCharge_measurable line 74
  6. lemma OAI.SLEExactGauge.wholeSausageCharge_expectation line 90
  7. def OAI.SLEExactGauge.wholeSausageChargeBound line 124
  8. lemma OAI.SLEExactGauge.wholeSausageChargeBound_lt_top line 128
  9. lemma OAI.SLEExactGauge.regularSLE_wholeSausageCharge_bound line 138
  10. theorem OAI.SLEExactGauge.source_cover_charge line 161
  11. lemma OAI.SLEExactGauge.source_cover_charge_sup line 197