OAI/Probability/SLE/LoewnerCharts.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

Loewner Charts for chordal SLE.

  1. def OAI.SLEExactGauge.upperHalfPlane line 16

    Also declared: ComparatorChallenges/SLELowerPositivity.lean:17 (same declaration text).

  2. def OAI.SLEExactGauge.survivingDomain line 20

    Also declared: ComparatorChallenges/SLELowerPositivity.lean:19 (same declaration text).

  3. def OAI.SLEExactGauge.IsCapacityTwoWitness line 26

    Also declared: ComparatorChallenges/SLELowerPositivity.lean:23 (same declaration text).

  4. lemma OAI.SLEExactGauge.survivingDomain_antitone line 44
  5. lemma OAI.SLEExactGauge.isOpen_upperHalfPlane line 54
  6. lemma OAI.SLEExactGauge.isOpen_survivingDomain line 56
  7. lemma OAI.SLEExactGauge.IsCapacityTwoWitness.time_derivative line 69
  8. lemma OAI.SLEExactGauge.IsCapacityTwoWitness.time_continuousOn line 82
  9. lemma OAI.SLEExactGauge.IsCapacityTwoWitness.imag_positive line 89
  10. lemma OAI.SLEExactGauge.IsCapacityTwoWitness.centered_ne_zero line 94
  11. lemma OAI.SLEExactGauge.IsCapacityTwoWitness.imag_derivative line 103
  12. lemma OAI.SLEExactGauge.IsCapacityTwoWitness.imag_antitoneOn line 113
  13. lemma OAI.SLEExactGauge.complex_linear_ode_exp line 131
  14. lemma OAI.SLEExactGauge.IsCapacityTwoWitness.live_at_real_time line 167
  15. lemma OAI.SLEExactGauge.IsCapacityTwoWitness.spatial_differentiableAt line 174
  16. lemma OAI.SLEExactGauge.IsCapacityTwoWitness.initial_value line 180
  17. def OAI.SLEExactGauge.loewnerPairCoefficient line 185
  18. lemma OAI.SLEExactGauge.IsCapacityTwoWitness.pair_coefficient_continuousOn line 190
  19. lemma OAI.SLEExactGauge.IsCapacityTwoWitness.difference_derivative line 203
  20. lemma OAI.SLEExactGauge.IsCapacityTwoWitness.difference_formula line 222
  21. lemma OAI.SLEExactGauge.IsCapacityTwoWitness.imag_ge_terminal line 236
  22. lemma OAI.SLEExactGauge.IsCapacityTwoWitness.centered_norm_ge_terminal line 243
  23. lemma OAI.SLEExactGauge.IsCapacityTwoWitness.pair_coefficient_bound line 252
  24. lemma OAI.SLEExactGauge.IsCapacityTwoWitness.pair_coefficient_intervalIntegrable line 266
  25. lemma OAI.SLEExactGauge.IsCapacityTwoWitness.pair_coefficient_tendsto line 274
  26. lemma OAI.SLEExactGauge.IsCapacityTwoWitness.pair_integral_tendsto line 284
  27. theorem OAI.SLEExactGauge.loewner_spatial_derivative line 315
  28. def OAI.SLEExactGauge.fullRadius line 337
  29. lemma OAI.SLEExactGauge.IsCapacityTwoWitness.derivative_norm_positive line 340
  30. lemma OAI.SLEExactGauge.IsCapacityTwoWitness.fullRadius_positive line 348
  31. lemma OAI.SLEExactGauge.IsCapacityTwoWitness.derivative_norm_derivative line 356
  32. lemma OAI.SLEExactGauge.loewnerPairCoefficient_re line 388
  33. lemma OAI.SLEExactGauge.IsCapacityTwoWitness.radius_derivative line 398
  34. theorem OAI.SLEExactGauge.loewner_radius_clock_derivative line 431
  35. def OAI.SLEExactGauge.logLoewnerCoordinates line 452
  36. lemma OAI.SLEExactGauge.IsCapacityTwoWitness.log_height_bounds line 456
  37. lemma OAI.SLEExactGauge.clippedCenter_logCoordinates line 470
  38. lemma OAI.SLEExactGauge.logLoewnerCoordinates_derivative line 487
  39. lemma OAI.SLEExactGauge.hasDerivWithinAt_Ici_of_Icc line 525
  40. lemma OAI.SLEExactGauge.logLoewnerCoordinates_initial line 533
  41. theorem OAI.SLEExactGauge.clipped_log_loewner_agrees line 544
  42. theorem OAI.SLEExactGauge.loewner_survival_of_positive_solution line 566