OAI/Probability/SLE/PhysicalMeshWindowCore.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

Physical Mesh Window Core for chordal SLE.

  1. structure OAI.SLEExactGauge.SourceWindowCore line 18
  2. lemma OAI.SLEExactGauge.SourceWindowCore.attach line 36
  3. lemma OAI.SLEExactGauge.source_mesh_window_core line 55
  4. lemma OAI.SLEExactGauge.source_if_bound line 112
  5. lemma OAI.SLEExactGauge.source_collar_HB_bounds line 119
  6. lemma OAI.SLEExactGauge.source_collar_end_zero line 129
  7. lemma OAI.SLEExactGauge.source_collar_start_zero line 139
  8. lemma OAI.SLEExactGauge.source_collar_weight_bounds line 150
  9. lemma OAI.SLEExactGauge.source_collar_weight_zero line 163
  10. lemma OAI.SLEExactGauge.source_collar_weight_joint line 176
  11. lemma OAI.SLEExactGauge.source_collar_mean_transfer line 185
  12. lemma OAI.SLEExactGauge.source_window_scaled_bound line 208
  13. lemma OAI.SLEExactGauge.source_collar_V_bounds line 215
  14. lemma OAI.SLEExactGauge.source_mesh_H_window line 251
  15. lemma OAI.SLEExactGauge.source_collar_V_mean line 322
  16. lemma OAI.SLEExactGauge.source_collar_V_joint line 356
  17. lemma OAI.SLEExactGauge.source_mesh_V_window line 372
  18. lemma OAI.SLEExactGauge.source_mesh_B_window line 437
  19. lemma OAI.SLEExactGauge.window_finite_mgf_at_starts line 504
  20. lemma OAI.SLEExactGauge.window_source_finite_mgf_at_starts line 593
  21. lemma OAI.SLEExactGauge.window_source_mgf_pos_at_starts line 647
  22. lemma OAI.SLEExactGauge.window_source_weighted_tail line 712