OAI/Probability/SLE/WindowBGeometry.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Window BGeometry for chordal SLE.

  1. lemma OAI.SLEExactGauge.source_witness_initial_domain line 15
  2. lemma OAI.SLEExactGauge.source_window_initial_ball line 24
  3. lemma OAI.SLEExactGauge.source_window_first_geometry line 35
  4. lemma OAI.SLEExactGauge.source_windowB_le_disk line 53
  5. lemma OAI.SLEExactGauge.source_condExp_bound_supported line 86
  6. lemma OAI.SLEExactGauge.source_windowB_integrable line 105
  7. lemma OAI.SLEExactGauge.source_windowB_mean line 117
  8. def OAI.SLEExactGauge.SourceSpatialWindowMeansTarget line 184
  9. theorem OAI.SLEExactGauge.sourceSpatialWindowMeans_proved line 202