OAI/Probability/SLEGauge/TailBatches.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

Hausdorff gauges, Loewner evolution and trace measures.

  1. lemma OAI.SLEExactGauge.MomentBatches.sum_repeated_thresholds line 18
  2. lemma OAI.SLEExactGauge.MomentBatches.noncleanup_sum line 25
  3. lemma OAI.SLEExactGauge.MomentBatches.batch_sum line 33
  4. lemma OAI.SLEExactGauge.MomentBatches.fin_sum_batch line 39
  5. lemma OAI.SLEExactGauge.MomentBatches.cleanup_counts_le line 48
  6. lemma OAI.SLEExactGauge.MomentBatches.cleanup_sum_le line 67
  7. theorem OAI.SLEExactGauge.MomentBatches.cleanup_tail line 83
  8. lemma OAI.SLEExactGauge.MomentBatches.upper_tail_bound_geometric line 90
  9. lemma OAI.SLEExactGauge.MomentBatches.summable_noncleanup_tails line 103
  10. theorem OAI.SLEExactGauge.MomentBatches.summable_batch_tails line 122
  11. theorem OAI.SLEExactGauge.MomentBatches.summable_entry_tails line 133
  12. theorem OAI.SLEExactGauge.MomentBatches.tail_summability line 160
  13. lemma OAI.SLEExactGauge.MomentBatches.increasing_level_bounds line 182
  14. lemma OAI.SLEExactGauge.MomentBatches.integrable_level_pow line 190
  15. theorem OAI.SLEExactGauge.MomentBatches.increasing_moments line 200
  16. lemma OAI.SLEExactGauge.MomentBatches.level_eq_tsum_indicators line 227
  17. def OAI.SLEExactGauge.MomentBatches.momentLevel line 249
  18. def OAI.SLEExactGauge.MomentBatches.fullMomentGauge line 252
  19. theorem OAI.SLEExactGauge.MomentBatches.selected_level_moment line 259
  20. theorem OAI.SLEExactGauge.MomentBatches.success_selected_level line 277
  21. theorem OAI.SLEExactGauge.MomentBatches.fullMomentGauge_properties line 296
  22. def OAI.SLEExactGauge.CenteredMoments.sequenceMassReal line 324
  23. def OAI.SLEExactGauge.CenteredMoments.sequenceLevelReal line 325
  24. lemma OAI.SLEExactGauge.CenteredMoments.sequenceMassReal_measurable line 327
  25. lemma OAI.SLEExactGauge.CenteredMoments.sequenceLevelReal_measurable line 330
  26. lemma OAI.SLEExactGauge.CenteredMoments.sequenceMassReal_nonneg line 333
  27. lemma OAI.SLEExactGauge.CenteredMoments.sequenceLevelReal_nonneg line 334
  28. lemma OAI.SLEExactGauge.CenteredMoments.sequenceReal_monotone line 337
  29. lemma OAI.SLEExactGauge.CenteredMoments.sequenceReal_tendsto line 342
  30. lemma OAI.SLEExactGauge.CenteredMoments.sequenceMassReal_integrable_pow line 347
  31. lemma OAI.SLEExactGauge.CenteredMoments.sequenceMassReal_moment line 354
  32. lemma OAI.SLEExactGauge.CenteredMoments.sequenceLevelReal_moment line 362
  33. theorem OAI.SLEExactGauge.CenteredMoments.sequenceReal_moment_data line 382
  34. structure OAI.SLEExactGauge.CenteredMoments.CenteredMomentModel line 428
  35. theorem OAI.SLEExactGauge.CenteredMoments.actual_centered_moment_model line 447
  36. def OAI.SLEExactGauge.CenteredMoments.CenteredMomentModel.gauge line 472
  37. def OAI.SLEExactGauge.CenteredMoments.CenteredMomentModel.mass line 474
  38. lemma OAI.SLEExactGauge.CenteredMoments.CenteredMomentModel.mass_measurable line 477
  39. lemma OAI.SLEExactGauge.CenteredMoments.CenteredMomentModel.integrable_moments line 480
  40. lemma OAI.SLEExactGauge.CenteredMoments.CenteredMomentModel.moments_positive line 485
  41. lemma OAI.SLEExactGauge.CenteredMoments.CenteredMomentModel.moment_finite_level line 490
  42. lemma OAI.SLEExactGauge.CenteredMoments.CenteredMomentModel.finite_moments_increasing line 497
  43. lemma OAI.SLEExactGauge.CenteredMoments.CenteredMomentModel.finite_moments_tendsto line 503
  44. lemma OAI.SLEExactGauge.CenteredMoments.CenteredMomentModel.gauge_admissible line 510
  45. lemma OAI.SLEExactGauge.CenteredMoments.CenteredMomentModel.gauge_doubling line 516
  46. lemma OAI.SLEExactGauge.CenteredMoments.CenteredMomentModel.selected_moments line 523
  47. lemma OAI.SLEExactGauge.CenteredMoments.CenteredMomentModel.success line 537
  48. lemma OAI.SLEExactGauge.CenteredMoments.CenteredMomentModel.tails_summable line 551