OAI/Probability/SLE/BoundaryDensity.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

Boundary Density for chordal SLE.

  1. def OAI.SLEExactGauge.smoothPositiveGap line 17
  2. lemma OAI.SLEExactGauge.smoothPositiveGap_pos line 20
  3. lemma OAI.SLEExactGauge.smoothPositiveGap_eq line 31
  4. lemma OAI.SLEExactGauge.smoothPositiveGap_contDiff line 37
  5. def OAI.SLEExactGauge.boundaryDensity line 42
  6. def OAI.SLEExactGauge.smoothBoundaryDensity line 45
  7. lemma OAI.SLEExactGauge.smoothBoundaryDensity_contDiff line 48
  8. lemma OAI.SLEExactGauge.smoothBoundaryDensity_eq line 59
  9. lemma OAI.SLEExactGauge.smoothBoundaryDensity_eventuallyEq line 64
  10. lemma OAI.SLEExactGauge.boundaryDensity_contDiffAt line 84
  11. lemma OAI.SLEExactGauge.boundaryDensity_spatial_derivative line 94
  12. lemma OAI.SLEExactGauge.boundaryDensity_spatial_second line 104
  13. lemma OAI.SLEExactGauge.boundaryDensity_directional line 128
  14. lemma OAI.SLEExactGauge.boundaryDensity_generator line 153
  15. lemma OAI.SLEExactGauge.exists_compact_boundary_field line 174
  16. lemma OAI.SLEExactGauge.compact_boundary_drift_zero line 196
  17. theorem OAI.SLEExactGauge.BoundaryClockSolution.stopped_boundary_density line 219
  18. lemma OAI.SLEExactGauge.continuous_hittingBtwn_mem line 308
  19. lemma OAI.SLEExactGauge.continuous_zero_iff_dense line 320
  20. theorem OAI.SLEExactGauge.continuous_nonnegative_first_zero_stopping line 345
  21. def OAI.SLEExactGauge.logRadiusClock line 408
  22. def OAI.SLEExactGauge.logAngleSq line 411
  23. def OAI.SLEExactGauge.logClockRate line 414
  24. lemma OAI.SLEExactGauge.logAngleSq_pos line 417
  25. lemma OAI.SLEExactGauge.logAngleSq_le_one line 421
  26. lemma OAI.SLEExactGauge.continuous_logAngleSq line 426
  27. lemma OAI.SLEExactGauge.continuous_logRadiusClock line 437
  28. lemma OAI.SLEExactGauge.greenLogDensity_radius_angle line 440
  29. lemma OAI.SLEExactGauge.codimension_pos line 451
  30. lemma OAI.SLEExactGauge.greenExponent_pos line 455
  31. lemma OAI.SLEExactGauge.greenLogDensity_le_at_angular_exit line 461
  32. lemma OAI.SLEExactGauge.logClockRate_pos line 476
  33. lemma OAI.SLEExactGauge.logClockRate_angle line 482
  34. lemma OAI.SLEExactGauge.log_ode_im_derivative line 487
  35. lemma OAI.SLEExactGauge.log_ode_clock_derivative line 494
  36. lemma OAI.SLEExactGauge.log_height_clock_derivative_nonneg line 515
  37. lemma OAI.SLEExactGauge.log_clock_rate_lower line 530
  38. theorem OAI.SLEExactGauge.log_loewner_height_clock_bounds line 541
  39. structure OAI.SLEExactGauge.ClippedLogSolution line 607
  40. lemma OAI.SLEExactGauge.exists_clippedLogSolution line 621
  41. lemma OAI.SLEExactGauge.compact_green_drift_zero line 642
  42. theorem OAI.SLEExactGauge.ClippedLogSolution.stopped_green line 659