OAI/Probability/SLEGauge/FiniteAngleEigen.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

Hausdorff gauges, Loewner evolution and trace measures.

  1. def OAI.ExactSLEGreen.angleEigenCutoff line 20
  2. lemma OAI.ExactSLEGreen.angleEigenCutoff_smooth line 23
  3. lemma OAI.ExactSLEGreen.angleEigenCutoff_compact line 39
  4. lemma OAI.ExactSLEGreen.angleEigenCutoff_eq_near line 43
  5. lemma OAI.ExactSLEGreen.angleEigenCutoff_generator line 49
  6. theorem OAI.ExactSLEGreen.local_angle_eigen line 71
  7. theorem OAI.ExactSLEGreen.finite_level_angle_eigen line 121
  8. def OAI.SLEExactGauge.Jacobi.anglePoly line 259
  9. lemma OAI.SLEExactGauge.Jacobi.eval_cos_deriv line 261
  10. lemma OAI.SLEExactGauge.Jacobi.eval_cos_second line 265
  11. lemma OAI.SLEExactGauge.Jacobi.angleGenerator_poly line 279
  12. lemma OAI.SLEExactGauge.Jacobi.anglePoly_smooth line 288
  13. lemma OAI.SLEExactGauge.Jacobi.anglePoly_bound line 298
  14. lemma OAI.SLEExactGauge.Jacobi.anglePoly_eigen line 302
  15. theorem OAI.SLEExactGauge.Jacobi.finite_angle_poly line 310
  16. lemma OAI.SLEExactGauge.Jacobi.radialState_measurable line 339
  17. lemma OAI.SLEExactGauge.Jacobi.radialWeight_measurable line 347
  18. def OAI.SLEExactGauge.Jacobi.cosState line 355
  19. lemma OAI.SLEExactGauge.Jacobi.cosState_measurable line 358
  20. def OAI.SLEExactGauge.Jacobi.finiteCos line 362
  21. lemma OAI.SLEExactGauge.Jacobi.finiteCos_measurable line 365
  22. def OAI.SLEExactGauge.Jacobi.finiteCosLaw line 370
  23. lemma OAI.SLEExactGauge.Jacobi.levelRadius_initial_le line 373
  24. lemma OAI.SLEExactGauge.Jacobi.finiteCosLaw_probability line 378
  25. lemma OAI.SLEExactGauge.Jacobi.finiteCosLaw_poly_integral line 388
  26. theorem OAI.SLEExactGauge.Jacobi.finiteCosLaw_eq_transition line 419
  27. theorem OAI.SLEExactGauge.Jacobi.finiteCosLaw_integral_bounds line 429
  28. def OAI.SLEExactGauge.Jacobi.arccosAngle line 453
  29. lemma OAI.SLEExactGauge.Jacobi.arccosAngle_measurable line 457
  30. lemma OAI.SLEExactGauge.Jacobi.arccosAngle_angleCos line 464
  31. def OAI.SLEExactGauge.Jacobi.angleState line 474
  32. lemma OAI.SLEExactGauge.Jacobi.angleState_measurable line 476
  33. lemma OAI.SLEExactGauge.Jacobi.arccosAngle_cosState line 480
  34. def OAI.SLEExactGauge.Jacobi.finiteAngle line 483
  35. lemma OAI.SLEExactGauge.Jacobi.finiteAngle_measurable line 486
  36. def OAI.SLEExactGauge.Jacobi.finiteAngleLaw line 490
  37. lemma OAI.SLEExactGauge.Jacobi.finiteCosLaw_map_arccos line 493
  38. lemma OAI.SLEExactGauge.Jacobi.pi_map_arccos line 504
  39. theorem OAI.SLEExactGauge.Jacobi.finiteAngleLaw_integral_bounds line 510
  40. theorem OAI.SLEExactGauge.Jacobi.finiteAngleLaw_inverse_power_finite line 524