OAI/Probability/SLE/SpatialMeans.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

Spatial Means for chordal SLE.

  1. def OAI.SLEExactGauge.SpatialClippedFamily.jointChart line 17
  2. lemma OAI.SLEExactGauge.SpatialClippedFamily.jointChart_measurable line 20
  3. lemma OAI.SLEExactGauge.SpatialClippedFamily.jointChart_eq line 23
  4. lemma OAI.SLEExactGauge.SpatialClippedFamily.live_measurable line 45
  5. lemma OAI.SLEExactGauge.spatialHitTime_mem line 75
  6. def OAI.SLEExactGauge.liveSpatialHitTime line 86
  7. lemma OAI.SLEExactGauge.spatialHitTime_le_of_dist_le line 90
  8. lemma OAI.SLEExactGauge.liveSpatialHitTime_eq line 97
  9. lemma OAI.SLEExactGauge.spatialGreenWeight_eq_live line 132
  10. lemma OAI.SLEExactGauge.spatialHitTime_measurable line 147
  11. lemma OAI.SLEExactGauge.RegularSLEPresentation.jointGreen_measurable line 164
  12. lemma OAI.SLEExactGauge.RegularSLEPresentation.spatialGreenWeight_measurable line 176
  13. def OAI.SLEExactGauge.spatialSlabCoefficient line 206
  14. lemma OAI.SLEExactGauge.IsCapacityTwoWitness.radius_before_spatial_hit line 213
  15. lemma OAI.SLEExactGauge.IsCapacityTwoWitness.slab_coefficient_bound line 227
  16. theorem OAI.SLEExactGauge.IsCapacityTwoWitness.slab_pair_later_start line 250
  17. lemma OAI.SLEExactGauge.IsCapacityTwoWitness.green_before_spatial_bound line 317
  18. lemma OAI.SLEExactGauge.IsCapacityTwoWitness.spatialGreenWeight_bound line 340
  19. def OAI.SLEExactGauge.spatialRealMass line 353
  20. lemma OAI.SLEExactGauge.RegularSLEPresentation.spatialRealMass_measurable line 361
  21. lemma OAI.SLEExactGauge.RegularSLEPresentation.spatialGreenWeight_spatial_integrable line 366
  22. lemma OAI.SLEExactGauge.RegularSLEPresentation.spatialRealMass_bound line 381
  23. lemma OAI.SLEExactGauge.source_halfplane_map_local_bound line 487
  24. theorem OAI.SLEExactGauge.source_killedGreen_progressive line 555
  25. def OAI.SLEExactGauge.sourceApproachKernel line 628
  26. lemma OAI.SLEExactGauge.sourceApproachKernel_measurable line 631
  27. lemma OAI.SLEExactGauge.sourceApproachKernel_norm_le line 650
  28. lemma OAI.SLEExactGauge.sourceApproachKernel_zero line 655
  29. lemma OAI.SLEExactGauge.source_rpow_scale line 664