OAI/Probability/SLE/PhysicalKernelUtilities.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

Physical Kernel Utilities for chordal SLE.

  1. def OAI.SLEExactGauge.sourcePhysicalDiskKernel line 20
  2. lemma OAI.SLEExactGauge.sourcePhysicalDiskKernel_measurable line 24
  3. lemma OAI.SLEExactGauge.sourcePhysicalDiskKernel_norm_le line 27
  4. lemma OAI.SLEExactGauge.source_physical_exit_open line 32
  5. lemma OAI.SLEExactGauge.source_restarted_interior_dense line 43
  6. lemma OAI.SLEExactGauge.source_firsthit_inverse_access line 68
  7. lemma OAI.SLEExactGauge.source_physical_exit_interior_inclusion line 118
  8. def OAI.SLEExactGauge.SourceFinitePhysicalDiskTarget line 161
  9. lemma OAI.SLEExactGauge.source_physical_kernel_mean_le line 182
  10. lemma OAI.SLEExactGauge.source_firsthit_kernel_mean_le line 221
  11. lemma OAI.SLEExactGauge.source_physical_exit_measurable line 261
  12. theorem OAI.SLEExactGauge.sourceFinitePhysicalDisk_proved line 273
  13. def OAI.SLEExactGauge.sourceStopTruncate line 376
  14. lemma OAI.SLEExactGauge.sourceStopTruncate_coe line 379
  15. lemma OAI.SLEExactGauge.sourceStopTruncate_stopping line 388
  16. lemma OAI.SLEExactGauge.sourceStop_indicator_tendsto line 394
  17. lemma OAI.SLEExactGauge.source_unbounded_setIntegral_le line 406
  18. lemma OAI.SLEExactGauge.source_condExp_le_of_setIntegral_le line 459
  19. lemma OAI.SLEExactGauge.source_unbounded_conditional_bound_on line 480
  20. lemma OAI.SLEExactGauge.source_physical_closed_prefix_isClosed line 537
  21. lemma OAI.SLEExactGauge.source_physical_closed_exit_measurableSet line 555
  22. lemma OAI.SLEExactGauge.source_physical_closed_exit_measurable line 594
  23. lemma OAI.SLEExactGauge.source_physical_slack_large line 611
  24. lemma OAI.SLEExactGauge.source_physical_slack_small line 621
  25. def OAI.SLEExactGauge.SourcePhysicalDiskTarget line 648
  26. theorem OAI.SLEExactGauge.sourcePhysicalDisk_proved line 671