OAI/Probability/SLE/SimplePastMesh.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

Simple Past Mesh for chordal SLE.

  1. theorem OAI.SLEExactGauge.RegularSLEPresentation.source_past_half_plane_mesh_tail line 49
  2. def OAI.SLEExactGauge.SourceSimpleEntranceMeshTarget line 135
  3. theorem OAI.SLEExactGauge.sourceSimpleEntranceMesh_proved line 145
  4. lemma OAI.SLEExactGauge.source_simple_entrance_bound line 220
  5. def OAI.SLEExactGauge.SourceSimpleStretchedTailTarget line 251
  6. theorem OAI.SLEExactGauge.sourceSimpleStretchedTail_proved line 261
  7. lemma OAI.SLEExactGauge.source_simple_entrance_all_tail line 314
  8. def OAI.SLEExactGauge.SourceSimplePhysicalBallAllTailTarget line 366
  9. theorem OAI.SLEExactGauge.sourceSimplePhysicalBallAllTail_proved line 376
  10. def OAI.SLEExactGauge.SourcePhysicalBallEveryKappaTarget line 440
  11. theorem OAI.SLEExactGauge.sourcePhysicalBallEveryKappa_proved line 450
  12. def OAI.SLEExactGauge.SourceActualSquareTailTarget_allKappa line 467
  13. theorem OAI.SLEExactGauge.sourceActualSquareTail_proved_allKappa line 477
  14. lemma OAI.SLEExactGauge.RegularSLEPresentation.source_actual_retained_experiment_allKappa line 542
  15. def OAI.SLEExactGauge.SourceActualRetainedLowerTarget_allKappa line 591
  16. theorem OAI.SLEExactGauge.sourceActualRetainedLower_proved_allKappa line 599
  17. def OAI.SLEExactGauge.SourceInteriorRetainedTransferTarget_allKappa line 633
  18. theorem OAI.SLEExactGauge.sourceInteriorRetainedTransfer_proved_allKappa line 645
  19. lemma OAI.SLEExactGauge.source_dilation_gauge_positive_allKappa line 685
  20. lemma OAI.SLEExactGauge.RegularSLEPresentation.source_trace_path_measurable_allKappa line 701
  21. lemma OAI.SLEExactGauge.RegularSLEPresentation.source_scale_trace_law_allKappa line 709
  22. def OAI.SLEExactGauge.SourceUniformInteriorSeedTarget_allKappa line 724
  23. theorem OAI.SLEExactGauge.sourceUniformInteriorSeed_proved_allKappa line 733