OAI/Probability/SLEGauge/JacobiKernel.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

Hausdorff gauges, Loewner evolution and trace measures.

  1. def OAI.SLEExactGauge.Jacobi.eigenvalue line 18
  2. def OAI.SLEExactGauge.Jacobi.majorantBase line 19
  3. def OAI.SLEExactGauge.Jacobi.mixingTime line 20
  4. def OAI.SLEExactGauge.Jacobi.mode line 22
  5. def OAI.SLEExactGauge.Jacobi.kernel line 26
  6. lemma OAI.SLEExactGauge.Jacobi.eigenvalue_nonneg line 28
  7. lemma OAI.SLEExactGauge.Jacobi.eigenvalue_ge line 32
  8. lemma OAI.SLEExactGauge.Jacobi.norm_ratio_le line 41
  9. lemma OAI.SLEExactGauge.Jacobi.mode_bound line 48
  10. lemma OAI.SLEExactGauge.Jacobi.geometric_factor line 67
  11. lemma OAI.SLEExactGauge.Jacobi.mode_geometric_bound line 75
  12. lemma OAI.SLEExactGauge.Jacobi.mode_summable line 87
  13. lemma OAI.SLEExactGauge.Jacobi.mode_continuous line 92
  14. lemma OAI.SLEExactGauge.Jacobi.kernel_continuous line 95
  15. lemma OAI.SLEExactGauge.Jacobi.mode_zero line 101
  16. lemma OAI.SLEExactGauge.Jacobi.kernel_bounds line 106
  17. lemma OAI.SLEExactGauge.Jacobi.integral_mode_poly line 137
  18. lemma OAI.SLEExactGauge.Jacobi.integral_kernel_poly line 152
  19. lemma OAI.SLEExactGauge.Jacobi.kernel_integrable line 183
  20. lemma OAI.SLEExactGauge.Jacobi.integral_kernel line 189
  21. def OAI.SLEExactGauge.Jacobi.transition line 195
  22. lemma OAI.SLEExactGauge.Jacobi.transition_probability line 198
  23. lemma OAI.SLEExactGauge.Jacobi.integral_transition_poly line 207
  24. lemma OAI.SLEExactGauge.Jacobi.polynomial_integrable line 231
  25. lemma OAI.SLEExactGauge.Jacobi.measure_eq_of_polynomial_integral line 237
  26. def OAI.SLEExactGauge.Jacobi.polynomialIntegral line 266
  27. lemma OAI.SLEExactGauge.Jacobi.measure_eq_of_poly_integral line 275
  28. lemma OAI.SLEExactGauge.Jacobi.transition_identified line 289
  29. lemma OAI.SLEExactGauge.Jacobi.transition_lintegral_bounds line 300
  30. lemma OAI.SLEExactGauge.Jacobi.weight_cos_sin line 337
  31. lemma OAI.SLEExactGauge.Jacobi.integral_sin_cos line 349
  32. lemma OAI.SLEExactGauge.Jacobi.integral_angleArea line 372
  33. lemma OAI.SLEExactGauge.Jacobi.angleNormalization_jacobi line 377
  34. def OAI.SLEExactGauge.Jacobi.angleCos line 398
  35. lemma OAI.SLEExactGauge.Jacobi.angleCos_measurable line 400
  36. lemma OAI.SLEExactGauge.Jacobi.integral_angleLaw_poly line 404
  37. lemma OAI.SLEExactGauge.Jacobi.map_angleLaw_eq_pi line 417