OAI/Probability/SLE/FiniteMass.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

Finite Mass for chordal SLE.

  1. lemma OAI.SLEExactGauge.continuous_radius_density_crossing line 17
  2. def OAI.SLEExactGauge.initialAngleWindowConstant line 47
  3. lemma OAI.SLEExactGauge.initial_inverse_angle_window_bound line 50
  4. lemma OAI.SLEExactGauge.sum_exp_decay line 94
  5. lemma OAI.SLEExactGauge.exponential_envelope_bound line 105
  6. lemma OAI.SLEExactGauge.integral_exp_neg_half_le_two line 137
  7. def OAI.SLEExactGauge.angleEnvelopeConstant line 157
  8. lemma OAI.SLEExactGauge.angleEnvelopeConstant_pos line 160
  9. lemma OAI.SLEExactGauge.finite_inverse_angle_envelope line 164
  10. lemma OAI.SLEExactGauge.log_height_clock_derivative_nonpos line 236
  11. lemma OAI.SLEExactGauge.log_loewner_radius_height_decay line 249
  12. lemma OAI.SLEExactGauge.AngularLocalization.physical_derivative line 280
  13. def OAI.SLEExactGauge.AngularLocalization.radiusPhysicalRate line 290
  14. lemma OAI.SLEExactGauge.AngularLocalization.radiusPhysicalRate_continuous line 295
  15. lemma OAI.SLEExactGauge.AngularLocalization.radiusPhysicalRate_at_clock line 305
  16. lemma OAI.SLEExactGauge.AngularLocalization.radiusPhysicalRate_integral line 315
  17. lemma OAI.SLEExactGauge.AngularLocalization.radius_height_decay line 339
  18. lemma OAI.SLEExactGauge.inverse_angle_control_rate line 364
  19. lemma OAI.SLEExactGauge.AngularLocalization.physical_rate_of_envelope line 383
  20. def OAI.SLEExactGauge.physicalTimeThreshold line 426
  21. lemma OAI.SLEExactGauge.physicalTimeThreshold_pos line 429
  22. lemma OAI.SLEExactGauge.AngularLocalization.physical_time_of_envelope line 438
  23. lemma OAI.SLEExactGauge.localized_physical_time_of_envelope line 463
  24. lemma OAI.SLEExactGauge.finite_physical_tail_of_localizations line 502
  25. lemma OAI.SLEExactGauge.finite_physical_tail_regular line 539
  26. theorem OAI.SLEExactGauge.finite_physical_tail line 573
  27. theorem OAI.SLEExactGauge.finite_physical_clock_tight line 604
  28. theorem OAI.SLEExactGauge.finite_physical_clock_positive line 634
  29. def OAI.SLEExactGauge.finiteSpatialGreenMass line 679
  30. def OAI.SLEExactGauge.SourceFiniteTimeFirstMomentTarget line 683
  31. lemma OAI.SLEExactGauge.initialGreen_continuousOn line 694
  32. lemma OAI.SLEExactGauge.angleEnvelopeConstant_continuousOn line 710
  33. def OAI.SLEExactGauge.halfClockThreshold line 721
  34. lemma OAI.SLEExactGauge.halfClockThreshold_pos line 725
  35. lemma OAI.SLEExactGauge.halfClockThreshold_continuousOn line 734
  36. lemma OAI.SLEExactGauge.RegularSLEPresentation.spatialHitTime_stopping line 752
  37. lemma OAI.SLEExactGauge.RegularSLEPresentation.finite_spatial_density_identity line 758
  38. lemma OAI.SLEExactGauge.RegularSLEPresentation.finite_spatial_lintegral_identity line 807
  39. lemma OAI.SLEExactGauge.RegularSLEPresentation.finite_spatial_lintegral_lower line 848
  40. lemma OAI.SLEExactGauge.RegularSLEPresentation.finiteSpatialGreenMass_expectation_swap line 923
  41. theorem OAI.SLEExactGauge.RegularSLEPresentation.source_finite_time_first_moment line 946
  42. theorem OAI.SLEExactGauge.sourceFiniteTimeFirstMoment line 985