OAI/Probability/SLEGauge/MomentBatches.lean

GitHub source file

52 declarations, 0 contain sorry, 0 declared as axioms

Hausdorff gauges, Loewner evolution and trace measures.

  1. def OAI.SLEExactGauge.MomentBatches.moment line 18
  2. lemma OAI.SLEExactGauge.MomentBatches.mean_pow_le_moment line 21
  3. def OAI.SLEExactGauge.MomentBatches.cutoff line 29
  4. def OAI.SLEExactGauge.MomentBatches.multiplicity line 32
  5. lemma OAI.SLEExactGauge.MomentBatches.multiplicity_bounds line 35
  6. lemma OAI.SLEExactGauge.MomentBatches.finite_multiplicity_support line 49
  7. def OAI.SLEExactGauge.MomentBatches.support line 65
  8. lemma OAI.SLEExactGauge.MomentBatches.mem_support line 69
  9. def OAI.SLEExactGauge.MomentBatches.noncleanup line 76
  10. def OAI.SLEExactGauge.MomentBatches.batch line 79
  11. lemma OAI.SLEExactGauge.MomentBatches.batch_length_pos line 81
  12. lemma OAI.SLEExactGauge.MomentBatches.batch_entry_lower line 84
  13. lemma OAI.SLEExactGauge.MomentBatches.batch_cleanup line 95
  14. def OAI.SLEExactGauge.MomentBatches.badLevels line 101
  15. lemma OAI.SLEExactGauge.MomentBatches.finite_badLevels line 103
  16. def OAI.SLEExactGauge.MomentBatches.level line 115
  17. lemma OAI.SLEExactGauge.MomentBatches.level_pos line 119
  18. lemma OAI.SLEExactGauge.MomentBatches.level_moment_gt line 123
  19. abbrev OAI.SLEExactGauge.MomentBatches.EntryIndex line 139
  20. instance OAI.SLEExactGauge.MomentBatches.(instance at line 141) line 141
  21. def OAI.SLEExactGauge.MomentBatches.threshold line 144
  22. def OAI.SLEExactGauge.MomentBatches.radius line 148
  23. lemma OAI.SLEExactGauge.MomentBatches.radius_pos line 151
  24. lemma OAI.SLEExactGauge.MomentBatches.radius_le line 154
  25. def OAI.SLEExactGauge.MomentBatches.cleanupIndex line 161
  26. lemma OAI.SLEExactGauge.MomentBatches.cleanup_threshold line 164
  27. lemma OAI.SLEExactGauge.MomentBatches.cleanup_cost_small line 167
  28. def OAI.SLEExactGauge.MomentBatches.momentGauge line 191
  29. theorem OAI.SLEExactGauge.MomentBatches.momentGauge_admissible line 196
  30. lemma OAI.SLEExactGauge.MomentBatches.momentGauge_doubling line 208
  31. lemma OAI.SLEExactGauge.MomentBatches.dyadic_predecessor line 231
  32. lemma OAI.SLEExactGauge.MomentBatches.dyadic_sum_le line 236

    Distinct definitions of this name: OAI/Probability/SLE/Gauge/MomentBatches.lean:30 (different declaration text). Qualify references as OAI.SLEExactGauge.MomentBatches.dyadic_sum_le@path.

  33. lemma OAI.SLEExactGauge.MomentBatches.dyadic_sum_below line 263
  34. lemma OAI.SLEExactGauge.MomentBatches.multiplicity_le_weight line 283
  35. def OAI.SLEExactGauge.MomentBatches.counts line 292
  36. lemma OAI.SLEExactGauge.MomentBatches.counts_nonneg line 295
  37. lemma OAI.SLEExactGauge.MomentBatches.counts_eq_sum_filter line 299
  38. lemma OAI.SLEExactGauge.MomentBatches.counts_upper line 304
  39. lemma OAI.SLEExactGauge.MomentBatches.multiplicity_le_counts line 320
  40. lemma OAI.SLEExactGauge.MomentBatches.counts_lower line 334
  41. lemma OAI.SLEExactGauge.MomentBatches.finite_entries_before line 357
  42. theorem OAI.SLEExactGauge.MomentBatches.momentGauge_finite_exclusions line 379
  43. lemma OAI.SLEExactGauge.MomentBatches.integrable_counts line 411
  44. lemma OAI.SLEExactGauge.MomentBatches.integral_counts line 417
  45. theorem OAI.SLEExactGauge.MomentBatches.upper_tail_finite line 431
  46. lemma OAI.SLEExactGauge.MomentBatches.sum_eq_tsum_multiplicity line 455
  47. lemma OAI.SLEExactGauge.MomentBatches.moment_sequence_properties line 467
  48. theorem OAI.SLEExactGauge.MomentBatches.upper_tail line 475
  49. lemma OAI.SLEExactGauge.MomentBatches.truncated_moment_lower line 488
  50. theorem OAI.SLEExactGauge.MomentBatches.success_strong line 527
  51. lemma OAI.SLEExactGauge.MomentBatches.success_numerics line 562
  52. theorem OAI.SLEExactGauge.MomentBatches.success line 584