OAI/Probability/SLEGauge/AngleMeasure.lean

GitHub source file

76 declarations, 0 contain sorry, 0 declared as axioms

Hausdorff gauges, Loewner evolution and trace measures.

  1. abbrev OAI.SLEExactGauge.CenteredMoments.Angle line 18
  2. def OAI.SLEExactGauge.CenteredMoments.angleArea line 20
  3. def OAI.SLEExactGauge.CenteredMoments.angleWeight line 22
  4. def OAI.SLEExactGauge.CenteredMoments.angleNormalization line 24
  5. def OAI.SLEExactGauge.CenteredMoments.angleLaw line 28
  6. lemma OAI.SLEExactGauge.CenteredMoments.angleArea_univ line 31
  7. instance OAI.SLEExactGauge.CenteredMoments.(instance at line 37) line 37
  8. lemma OAI.SLEExactGauge.CenteredMoments.angleArea_ne_zero line 39
  9. lemma OAI.SLEExactGauge.CenteredMoments.angleWeight_measurable line 43
  10. lemma OAI.SLEExactGauge.CenteredMoments.angleWeight_pos line 47
  11. lemma OAI.SLEExactGauge.CenteredMoments.angleWeight_le_one line 50
  12. lemma OAI.SLEExactGauge.CenteredMoments.angleNormalization_pos line 55
  13. lemma OAI.SLEExactGauge.CenteredMoments.angleNormalization_lt_top line 63
  14. lemma OAI.SLEExactGauge.CenteredMoments.angleLaw_probability line 68
  15. lemma OAI.SLEExactGauge.CenteredMoments.angleLaw_integral line 74
  16. lemma OAI.SLEExactGauge.CenteredMoments.angleWeight_cancel line 81
  17. lemma OAI.SLEExactGauge.CenteredMoments.angle_inverse_power_finite line 89
  18. def OAI.SLEExactGauge.Jacobi.operator line 118
  19. def OAI.SLEExactGauge.Jacobi.raise line 122
  20. lemma OAI.SLEExactGauge.Jacobi.raise_derivative line 125
  21. lemma OAI.SLEExactGauge.Jacobi.raise_eigen line 135
  22. lemma OAI.SLEExactGauge.Jacobi.raise_lowering line 147
  23. def OAI.SLEExactGauge.Jacobi.poly line 156
  24. lemma OAI.SLEExactGauge.Jacobi.poly_zero line 160
  25. lemma OAI.SLEExactGauge.Jacobi.poly_succ line 161
  26. lemma OAI.SLEExactGauge.Jacobi.poly_eigen line 164
  27. lemma OAI.SLEExactGauge.Jacobi.poly_lowering line 171
  28. lemma OAI.SLEExactGauge.Jacobi.raise_eq_X_sub line 176
  29. lemma OAI.SLEExactGauge.Jacobi.poly_one line 184
  30. def OAI.SLEExactGauge.Jacobi.beta line 189
  31. lemma OAI.SLEExactGauge.Jacobi.poly_recurrence line 192
  32. lemma OAI.SLEExactGauge.Jacobi.beta_pos line 204
  33. lemma OAI.SLEExactGauge.Jacobi.beta_le_one line 208
  34. lemma OAI.SLEExactGauge.Jacobi.beta_lower line 214
  35. lemma OAI.SLEExactGauge.Jacobi.poly_eval_bound line 232
  36. def OAI.SLEExactGauge.Jacobi.weight line 267
  37. def OAI.SLEExactGauge.Jacobi.flux line 268
  38. def OAI.SLEExactGauge.Jacobi.inner line 270
  39. lemma OAI.SLEExactGauge.Jacobi.continuous_weight line 273
  40. lemma OAI.SLEExactGauge.Jacobi.continuous_flux line 276
  41. lemma OAI.SLEExactGauge.Jacobi.flux_eq line 279
  42. lemma OAI.SLEExactGauge.Jacobi.hasDerivAt_flux line 286
  43. lemma OAI.SLEExactGauge.Jacobi.inner_comm line 296
  44. lemma OAI.SLEExactGauge.Jacobi.inner_integrable line 301
  45. lemma OAI.SLEExactGauge.Jacobi.inner_add_left line 305
  46. lemma OAI.SLEExactGauge.Jacobi.inner_sub_left line 310
  47. lemma OAI.SLEExactGauge.Jacobi.inner_C_mul_left line 315
  48. lemma OAI.SLEExactGauge.Jacobi.inner_neg_left line 321
  49. lemma OAI.SLEExactGauge.Jacobi.inner_X line 325
  50. lemma OAI.SLEExactGauge.Jacobi.operator_symmetric line 332
  51. lemma OAI.SLEExactGauge.Jacobi.eigenvalue_strictMono line 358
  52. lemma OAI.SLEExactGauge.Jacobi.poly_orthogonal line 365
  53. lemma OAI.SLEExactGauge.Jacobi.poly_monic_degree line 389
  54. def OAI.SLEExactGauge.Jacobi.basis line 406
  55. lemma OAI.SLEExactGauge.Jacobi.basis_apply line 413
  56. def OAI.SLEExactGauge.Jacobi.normSq line 416
  57. lemma OAI.SLEExactGauge.Jacobi.normSq_zero_pos line 418
  58. lemma OAI.SLEExactGauge.Jacobi.normSq_succ line 428
  59. lemma OAI.SLEExactGauge.Jacobi.normSq_pos line 449
  60. lemma OAI.SLEExactGauge.Jacobi.normSq_lower line 456
  61. abbrev OAI.SLEExactGauge.Jacobi.Interval line 485
  62. def OAI.SLEExactGauge.Jacobi.baseMeasure line 487
  63. instance OAI.SLEExactGauge.Jacobi.base_finite line 489
  64. lemma OAI.SLEExactGauge.Jacobi.weight_nonneg line 495
  65. lemma OAI.SLEExactGauge.Jacobi.continuous_weight_interval line 500
  66. lemma OAI.SLEExactGauge.Jacobi.integrable_weight_interval line 503
  67. lemma OAI.SLEExactGauge.Jacobi.integral_base line 507
  68. lemma OAI.SLEExactGauge.Jacobi.integral_weight_base line 512
  69. def OAI.SLEExactGauge.Jacobi.rawMeasure line 517
  70. def OAI.SLEExactGauge.Jacobi.pi line 520
  71. lemma OAI.SLEExactGauge.Jacobi.rawMeasure_univ line 522
  72. lemma OAI.SLEExactGauge.Jacobi.pi_probability line 528
  73. lemma OAI.SLEExactGauge.Jacobi.integral_pi_mul line 533
  74. lemma OAI.SLEExactGauge.Jacobi.integral_pi_poly line 546
  75. lemma OAI.SLEExactGauge.Jacobi.poly_interval_integrable line 554
  76. lemma OAI.SLEExactGauge.Jacobi.integral_pi_poly_single line 560