OAI/Probability/SLEGauge/ProductGenerators.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

Hausdorff gauges, Loewner evolution and trace measures.

  1. lemma OAI.ExactSLECalculus.normalized_product_generator line 22
  2. lemma OAI.ExactSLECalculus.N_comp_clm line 57
  3. lemma OAI.ExactSLECalculus.L_comp_clm line 62
  4. lemma OAI.ExactSLEFiniteTilt.pair_noise_form line 77
  5. lemma OAI.ExactSLEGreen.actual_noise_pair line 102
  6. lemma OAI.ExactSLECalculus.sum_square_off_diagonal line 146
  7. lemma OAI.ExactSLECalculus.sum_pair_endpoints line 154
  8. lemma OAI.ExactSLECalculus.sum_generator_absorption line 166
  9. def OAI.ExactSLEGreen.multiDrift line 191
  10. def OAI.ExactSLEGreen.multiNoise line 193
  11. def OAI.ExactSLEGreen.regularizedProduct line 194
  12. theorem OAI.ExactSLEGreen.regularized_product_drift line 198
  13. abbrev OAI.ExactSLEGreen.RegimeState line 272
  14. def OAI.ExactSLEGreen.regimeDiscount line 273
  15. def OAI.ExactSLEGreen.discountedProduct line 280
  16. lemma OAI.ExactSLECalculus.discounted_generator line 287
  17. lemma OAI.ExactSLEGreen.physicalRegularized_smooth_infty line 314
  18. lemma OAI.ExactSLEGreen.regularizedProduct_smooth_infty line 327
  19. lemma OAI.ExactSLEGreen.regularizedProduct_generator_agrees line 335
  20. lemma OAI.ExactSLEGreen.discountedProduct_nonpos line 366
  21. def OAI.ExactSLEGreen.regularizedHeightTurn line 384
  22. lemma OAI.ExactSLEGreen.regularizedHeightTurn_smooth line 386
  23. lemma OAI.ExactSLEGreen.regularizedHeightTurn_zero line 389
  24. lemma OAI.ExactSLEGreen.regularizedHeightTurn_one line 394
  25. lemma OAI.ExactSLEGreen.height_regularized_smooth line 399
  26. def OAI.ExactSLEGreen.regimeBump line 410
  27. def OAI.ExactSLEGreen.regimeCutoff line 415
  28. lemma OAI.ExactSLEGreen.regimeCutoff_smooth line 419
  29. lemma OAI.ExactSLEGreen.regimeCutoff_compact line 428
  30. lemma OAI.ExactSLEGreen.regimeCutoff_eq_near line 432