OAI/Probability/SLEGauge/ConformalFlow.lean

GitHub source file

52 declarations, 0 contain sorry, 0 declared as axioms

Hausdorff gauges, Loewner evolution and trace measures.

  1. theorem OAI.ExactSLEMain.hasDerivAt_loewnerMap line 20
  2. lemma OAI.ExactSLEMain.deriv_loewnerMap_ne_zero line 90
  3. lemma OAI.ExactSLEMain.loewnerMap_eq_solution_time line 100
  4. lemma OAI.ExactSLEMain.odeUntil_center_ne_zero line 106
  5. lemma OAI.ExactSLEMain.odeUntil_center_continuousOn line 115
  6. lemma OAI.ExactSLEMain.loewner_derivative_integrable line 121
  7. theorem OAI.ExactSLEMain.log_norm_deriv_loewnerMap line 138
  8. lemma OAI.ExactSLEMain.loewner_radius_drift line 146
  9. lemma OAI.ExactSLEMain.real_scalar_linear_solution_on line 156
  10. theorem OAI.ExactSLEMain.loewner_height_formula line 172
  11. theorem OAI.ExactSLEMain.loewner_radius_ratio line 192
  12. abbrev OAI.ExactSLEGreen.State line 239
  13. def OAI.ExactSLEGreen.X line 240
  14. def OAI.ExactSLEGreen.Y line 241
  15. def OAI.ExactSLEGreen.J line 242
  16. def OAI.ExactSLEGreen.Q line 243
  17. def OAI.ExactSLEGreen.p line 244
  18. def OAI.ExactSLEGreen.alpha line 245
  19. def OAI.ExactSLEGreen.logGreen line 246
  20. def OAI.ExactSLEGreen.physicalGreen line 248
  21. def OAI.ExactSLEGreen.logGreenDeriv line 249
  22. def OAI.ExactSLEGreen.physicalDrift line 252
  23. def OAI.ExactSLEGreen.noise line 254
  24. lemma OAI.ExactSLEGreen.X_apply line 256
  25. lemma OAI.ExactSLEGreen.Y_apply line 257
  26. lemma OAI.ExactSLEGreen.J_apply line 258
  27. lemma OAI.ExactSLEGreen.Q_eq line 259
  28. lemma OAI.ExactSLEGreen.Q_pos line 261
  29. lemma OAI.ExactSLEGreen.hasFDerivAt_Q line 265
  30. lemma OAI.ExactSLEGreen.hasFDerivAt_logGreen line 272
  31. lemma OAI.ExactSLEGreen.hasFDerivAt_physicalGreen line 280
  32. lemma OAI.ExactSLEGreen.contDiffAt_physicalGreen line 284
  33. lemma OAI.ExactSLEGreen.logGreenDeriv_noise line 291
  34. lemma OAI.ExactSLEGreen.logGreenDeriv_drift line 299
  35. def OAI.ExactSLEGreen.noiseLog line 316
  36. def OAI.ExactSLEGreen.noiseLogDeriv line 317
  37. lemma OAI.ExactSLEGreen.hasFDerivAt_noiseLog line 320
  38. lemma OAI.ExactSLEGreen.noiseLogDeriv_noise line 330
  39. lemma OAI.ExactSLEGreen.green_fderiv_noise line 341
  40. lemma OAI.ExactSLEGreen.hasFDerivAt_green_noise line 346
  41. lemma OAI.ExactSLEGreen.green_second_noise line 356
  42. lemma OAI.ExactSLEGreen.green_generator_zero line 365
  43. def OAI.ExactSLEGreen.spaceBump line 381
  44. def OAI.ExactSLEGreen.heightTurn line 387
  45. def OAI.ExactSLEGreen.greenCutoff line 390
  46. lemma OAI.ExactSLEGreen.heightTurn_smooth line 393
  47. lemma OAI.ExactSLEGreen.heightTurn_zero line 397
  48. lemma OAI.ExactSLEGreen.heightTurn_one line 403
  49. lemma OAI.ExactSLEGreen.greenCutoff_smooth line 409
  50. lemma OAI.ExactSLEGreen.greenCutoff_compact line 421
  51. lemma OAI.ExactSLEGreen.greenCutoff_eq_near line 424
  52. lemma OAI.ExactSLEGreen.greenCutoff_generator_zero line 435