OAI/Probability/SLE/InverseMoments.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

Inverse Moments for chordal SLE.

  1. theorem OAI.SLEExactGauge.physicalGreenLimit_stopping_condExp_terminal line 17
  2. theorem OAI.SLEExactGauge.exists_physical_green_stopping_regular line 93
  3. theorem OAI.SLEExactGauge.exists_physical_green_stopping line 161
  4. def OAI.SLEExactGauge.spatialHitTime line 215
  5. lemma OAI.SLEExactGauge.spatialHitTime_le_iff line 218
  6. lemma OAI.SLEExactGauge.spatialHitTime_lt_of_dist_lt line 226
  7. lemma OAI.SLEExactGauge.IsCapacityTwoWitness.radius_hit_forces_spatial_before line 235
  8. lemma OAI.SLEExactGauge.IsCapacityTwoWitness.physicalGreen_eq_before_spatial line 257
  9. lemma OAI.SLEExactGauge.IsCapacityTwoWitness.radius_no_hit_of_spatial_no_hit line 268
  10. def OAI.SLEExactGauge.spatialGreenWeight line 281
  11. def OAI.SLEExactGauge.boundedSpatialHit line 286
  12. lemma OAI.SLEExactGauge.boundedSpatialHit_coe line 289
  13. lemma OAI.SLEExactGauge.boundedSpatialHit_le line 297
  14. lemma OAI.SLEExactGauge.IsCapacityTwoWitness.spatialGreen_limit line 304
  15. lemma OAI.SLEExactGauge.IsCapacityTwoWitness.live_initial line 343
  16. lemma OAI.SLEExactGauge.IsCapacityTwoWitness.green_initial line 352
  17. lemma OAI.SLEExactGauge.RegularSLEPresentation.boundedSpatialHit_stopping line 368
  18. theorem OAI.SLEExactGauge.RegularSLEPresentation.spatialGreen_expectation_of_level line 375
  19. theorem OAI.SLEExactGauge.RegularSLEPresentation.spatialGreen_expectation line 444
  20. structure OAI.SLEExactGauge.SpatialClippedFamily line 475
  21. def OAI.SLEExactGauge.spatialClippedFamily line 483
  22. def OAI.SLEExactGauge.SpatialClippedFamily.valid line 496
  23. lemma OAI.SLEExactGauge.SpatialClippedFamily.valid_measurable line 499
  24. lemma OAI.SLEExactGauge.SpatialClippedFamily.derivative_compact line 510
  25. lemma OAI.SLEExactGauge.SpatialClippedFamily.live_of_valid line 516
  26. lemma OAI.SLEExactGauge.SpatialClippedFamily.agrees_of_live line 525
  27. lemma OAI.SLEExactGauge.SpatialClippedFamily.eventually_valid_agrees line 535
  28. def OAI.SLEExactGauge.SpatialClippedFamily.greenApprox line 568
  29. lemma OAI.SLEExactGauge.SpatialClippedFamily.greenApprox_measurable line 573
  30. def OAI.SLEExactGauge.SpatialClippedFamily.jointGreen line 583
  31. lemma OAI.SLEExactGauge.SpatialClippedFamily.jointGreen_measurable line 586
  32. lemma OAI.SLEExactGauge.SpatialClippedFamily.jointGreen_eq line 591
  33. theorem OAI.SLEExactGauge.exists_joint_green_density line 612
  34. def OAI.SLEExactGauge.SpatialClippedFamily.chartApprox line 646
  35. lemma OAI.SLEExactGauge.SpatialClippedFamily.chartApprox_measurable line 652