OAI/Probability/SLE/MeasureSupport.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

Measure Support for chordal SLE.

  1. def OAI.SLEExactGauge.spatialGreenMass line 15
  2. lemma OAI.SLEExactGauge.RegularSLEPresentation.spatialGreenMass_measurable line 23
  3. lemma OAI.SLEExactGauge.RegularSLEPresentation.spatialGreenMass_expectation line 30
  4. lemma OAI.SLEExactGauge.RegularSLEPresentation.spatialGreenMass_expectation_le line 54
  5. lemma OAI.SLEExactGauge.finite_density_crossing_bound line 87
  6. lemma OAI.SLEExactGauge.finite_density_crossing_bound_of_subset line 119
  7. lemma OAI.SLEExactGauge.limitRadiusKernel_pos_iff line 144
  8. lemma OAI.SLEExactGauge.finiteCenteredLaw_eq_radiusKernel line 165
  9. lemma OAI.SLEExactGauge.radiusKernel_density_bound line 179
  10. lemma OAI.SLEExactGauge.finiteCenteredLaw_consistent_at_radius line 197
  11. lemma OAI.SLEExactGauge.finite_radius_density_crossing line 227
  12. lemma OAI.SLEExactGauge.radius_kernel_scale_cancel line 269
  13. lemma OAI.SLEExactGauge.finite_radius_scaled_crossing line 298
  14. lemma OAI.SLEExactGauge.limitRadiusKernel_eq_of_surviving_cutoff line 365
  15. lemma OAI.SLEExactGauge.limitRadiusKernel_eq_below line 375
  16. lemma OAI.SLEExactGauge.exists_cutoff_of_radiusStop_lt_top line 386
  17. lemma OAI.SLEExactGauge.limitRadiusKernel_continuousOn_of_live line 393
  18. lemma OAI.SLEExactGauge.limitRadiusKernel_pos_of_live line 403
  19. lemma OAI.SLEExactGauge.radius_limit_clock_angle line 411
  20. lemma OAI.SLEExactGauge.finite_grid_from_monotone line 442
  21. lemma OAI.SLEExactGauge.countable_grid_from_monotone line 486
  22. lemma OAI.SLEExactGauge.continuous_crossing_from_monotone line 519
  23. lemma OAI.SLEExactGauge.terminalRadiusKernel_continuousOn line 558
  24. lemma OAI.SLEExactGauge.terminalRadiusKernel_pos line 572
  25. lemma OAI.SLEExactGauge.continuous_radius_scaled_crossing line 581
  26. def OAI.SLEExactGauge.radiusInverseAngle line 623
  27. lemma OAI.SLEExactGauge.radiusInverseAngle_product line 628
  28. lemma OAI.SLEExactGauge.radiusInverseAngle_large_imp_crossing line 637
  29. lemma OAI.SLEExactGauge.inverse_angle_window_bound line 655