OAI/Probability/SLE/RadiusClocks.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

Radius Clocks for chordal SLE.

  1. lemma OAI.SLEExactGauge.measurableSet_exists_zero_compact line 14
  2. lemma OAI.SLEExactGauge.hittingAfter_zero_le_iff line 46
  3. theorem OAI.SLEExactGauge.continuous_zero_hit_stopping line 75
  4. lemma OAI.SLEExactGauge.stopped_min_measurable line 109
  5. theorem OAI.SLEExactGauge.continuous_zero_hit_after_stopping line 118
  6. def OAI.SLEExactGauge.diskHitAfter line 175
  7. lemma OAI.SLEExactGauge.RegularSLEPresentation.diskHitAfter_stopping line 183
  8. def OAI.SLEExactGauge.RegularSLEPresentation.boundedDiskHit line 196
  9. lemma OAI.SLEExactGauge.RegularSLEPresentation.boundedDiskHit_coe line 200
  10. lemma OAI.SLEExactGauge.RegularSLEPresentation.boundedDiskHit_stopping line 210
  11. theorem OAI.SLEExactGauge.RegularSLEPresentation.boundedDiskHit_restart_law line 218
  12. lemma OAI.SLEExactGauge.complex_bilinear_rotation_trace line 242
  13. lemma OAI.SLEExactGauge.complex_hessian_rotation line 255
  14. def OAI.SLEExactGauge.polarPoint line 262
  15. lemma OAI.SLEExactGauge.polarPoint_eq_circleMap line 264
  16. lemma OAI.SLEExactGauge.polarPoint_norm line 267
  17. lemma OAI.SLEExactGauge.polarPoint_radial_hasDeriv line 270
  18. lemma OAI.SLEExactGauge.polarPoint_angular_hasDeriv line 274
  19. lemma OAI.SLEExactGauge.radial_partial_hasDeriv line 279
  20. lemma OAI.SLEExactGauge.radial_second_hasDeriv line 286
  21. lemma OAI.SLEExactGauge.angular_partial_hasDeriv line 297
  22. lemma OAI.SLEExactGauge.angular_second_hasDeriv line 304
  23. lemma OAI.SLEExactGauge.polar_laplacian_identity line 318
  24. def OAI.SLEExactGauge.polarRadialFlux line 341
  25. def OAI.SLEExactGauge.polarAngularFlux line 345
  26. lemma OAI.SLEExactGauge.polarPoint_contDiff line 349
  27. lemma OAI.SLEExactGauge.polarRadialFlux_differentiableAt line 358
  28. lemma OAI.SLEExactGauge.polarAngularFlux_differentiableAt line 368
  29. lemma OAI.SLEExactGauge.polarRadialFlux_radial_hasDeriv line 380
  30. lemma OAI.SLEExactGauge.polarAngularFlux_angular_hasDeriv line 394
  31. lemma OAI.SLEExactGauge.polarGreen_divergence line 402
  32. lemma OAI.SLEExactGauge.polarPoint_endpoints line 424
  33. lemma OAI.SLEExactGauge.polarAngularFlux_endpoints line 430
  34. lemma OAI.SLEExactGauge.plane_laplacian_continuousAt line 445
  35. lemma OAI.SLEExactGauge.polarPoint_mem_ball line 457
  36. lemma OAI.SLEExactGauge.annulus_green_identity line 464
  37. lemma OAI.SLEExactGauge.annulus_green_le line 526
  38. lemma OAI.SLEExactGauge.derivative_locally_bounded line 569
  39. def OAI.SLEExactGauge.annulusDensity line 591
  40. def OAI.SLEExactGauge.greenRectangle line 594
  41. def OAI.SLEExactGauge.greenTruncation line 596
  42. lemma OAI.SLEExactGauge.annulusDensity_continuousOn line 599
  43. lemma OAI.SLEExactGauge.annulusDensity_integrableOn line 610
  44. lemma OAI.SLEExactGauge.greenTruncation_integrable line 616
  45. lemma OAI.SLEExactGauge.greenTruncation_nonneg line 623
  46. lemma OAI.SLEExactGauge.greenTruncation_integral line 634
  47. lemma OAI.SLEExactGauge.greenTruncation_lintegral_le line 647