OAI/Probability/SLEGauge/AdaptedFailure.lean

GitHub source file

51 declarations, 0 contain sorry, 0 declared as axioms

Hausdorff gauges, Loewner evolution and trace measures.

  1. def OAI.SLEExactGauge.AdaptedFailure.failed line 20
  2. lemma OAI.SLEExactGauge.AdaptedFailure.failed_iff line 25
  3. lemma OAI.SLEExactGauge.AdaptedFailure.failed_measurable line 38
  4. theorem OAI.SLEExactGauge.AdaptedFailure.failure_product line 47
  5. lemma OAI.SLEExactGauge.AdaptedFailure.product_le_exp line 68
  6. lemma OAI.SLEExactGauge.AdaptedFailure.tested_of_conditional line 81
  7. theorem OAI.SLEExactGauge.AdaptedFailure.conditional_failure line 99
  8. lemma OAI.SLEExactGauge.AdaptedFailure.weighted_past_bound line 114
  9. theorem OAI.SLEExactGauge.AdaptedFailure.weighted_conditional_failure line 127
  10. structure OAI.SLEExactGauge.CenteredMoments.RadialTestSchedule line 158
  11. def OAI.SLEExactGauge.CenteredMoments.CenteredMomentModel.testSuccess line 174
  12. def OAI.SLEExactGauge.CenteredMoments.CenteredMomentModel.testFailure line 177
  13. lemma OAI.SLEExactGauge.CenteredMoments.CenteredMomentModel.testFailure_raw line 180
  14. theorem OAI.SLEExactGauge.CenteredMoments.CenteredMomentModel.testFailure_product line 203
  15. lemma OAI.SLEExactGauge.CenteredMoments.CenteredMomentModel.testFailure_exponential line 260
  16. theorem OAI.SLEExactGauge.CenteredMoments.CenteredMomentModel.testFailure_chordal line 275
  17. def OAI.SLEExactGauge.CenteredMoments.batchRadius line 306
  18. lemma OAI.SLEExactGauge.CenteredMoments.batchRadius_pos line 309
  19. lemma OAI.SLEExactGauge.CenteredMoments.batchRadius_zero line 311
  20. lemma OAI.SLEExactGauge.CenteredMoments.batchRadius_succ line 314
  21. lemma OAI.SLEExactGauge.CenteredMoments.batchRadius_antitone line 320
  22. lemma OAI.SLEExactGauge.CenteredMoments.mixingTime_nonneg line 327
  23. def OAI.SLEExactGauge.CenteredMoments.BatchReady line 331
  24. lemma OAI.SLEExactGauge.CenteredMoments.eventually_batchReady line 335
  25. lemma OAI.SLEExactGauge.CenteredMoments.BatchReady.mixing line 348
  26. def OAI.SLEExactGauge.CenteredMoments.batchBoundary line 355
  27. lemma OAI.SLEExactGauge.CenteredMoments.batchBoundary_pos line 359
  28. lemma OAI.SLEExactGauge.CenteredMoments.batchBoundary_start line 364
  29. lemma OAI.SLEExactGauge.CenteredMoments.batchBoundary_le line 383
  30. def OAI.SLEExactGauge.CenteredMoments.batchSchedule line 394
  31. lemma OAI.SLEExactGauge.CenteredMoments.batch_final_gap line 409
  32. lemma OAI.SLEExactGauge.CenteredMoments.batch_final_le line 418
  33. lemma OAI.SLEExactGauge.CenteredMoments.sum_getD_eq_map_sum line 442
  34. def OAI.SLEExactGauge.CenteredMoments.CenteredMomentModel.batchLevel line 453
  35. def OAI.SLEExactGauge.CenteredMoments.CenteredMomentModel.testCount line 455
  36. def OAI.SLEExactGauge.CenteredMoments.CenteredMomentModel.testThreshold line 457
  37. def OAI.SLEExactGauge.CenteredMoments.CenteredMomentModel.finalRadius line 459
  38. lemma OAI.SLEExactGauge.CenteredMoments.CenteredMomentModel.finalRadius_pos line 461
  39. lemma OAI.SLEExactGauge.CenteredMoments.CenteredMomentModel.finalRadius_le line 463
  40. lemma OAI.SLEExactGauge.CenteredMoments.CenteredMomentModel.testThreshold_pos line 467
  41. def OAI.SLEExactGauge.CenteredMoments.CenteredMomentModel.testIndex line 482
  42. lemma OAI.SLEExactGauge.CenteredMoments.CenteredMomentModel.testIndex_threshold line 488
  43. lemma OAI.SLEExactGauge.CenteredMoments.CenteredMomentModel.testIndex_radius line 493
  44. lemma OAI.SLEExactGauge.CenteredMoments.CenteredMomentModel.cleanup_radius line 496
  45. lemma OAI.SLEExactGauge.CenteredMoments.CenteredMomentModel.batch_success line 499
  46. lemma OAI.SLEExactGauge.CenteredMoments.CenteredMomentModel.testCount_pos line 515
  47. lemma OAI.SLEExactGauge.CenteredMoments.CenteredMomentModel.batch_half_success line 524
  48. def OAI.SLEExactGauge.CenteredMoments.CenteredMomentModel.batchFailures line 530
  49. lemma OAI.SLEExactGauge.CenteredMoments.CenteredMomentModel.batchFailures_eq_testFailure line 534
  50. lemma OAI.SLEExactGauge.CenteredMoments.CenteredMomentModel.batch_failures_measurable line 543
  51. theorem OAI.SLEExactGauge.CenteredMoments.CenteredMomentModel.batch_failure_chordal line 553