OAI/Probability/SLE/MomentGauge.lean

GitHub source file

103 declarations, 0 contain sorry, 0 declared as axioms

Quadratic moment envelopes, Hausdorff gauge admissibility and interval transfer.

  1. abbrev OAI.SLEExactGauge.Target.Driver line 16
  2. instance OAI.SLEExactGauge.Target.(instance at line 17) line 17
  3. instance OAI.SLEExactGauge.Target.(instance at line 18) line 18
  4. abbrev OAI.SLEExactGauge.Target.WienerLaw line 19
  5. def OAI.SLEExactGauge.Target.IsWiener line 21
  6. def OAI.SLEExactGauge.Target.a line 24
  7. def OAI.SLEExactGauge.Target.d line 25
  8. def OAI.SLEExactGauge.Target.α line 26
  9. def OAI.SLEExactGauge.Target.p line 27
  10. def OAI.SLEExactGauge.Target.driverValue line 29
  11. def OAI.SLEExactGauge.Target.cutoffField line 31
  12. def OAI.SLEExactGauge.Target.mesh line 35
  13. def OAI.SLEExactGauge.Target.eulerSteps line 37
  14. def OAI.SLEExactGauge.Target.eulerFlow line 42
  15. def OAI.SLEExactGauge.Target.cutoffFlow line 47
  16. def OAI.SLEExactGauge.Target.Surviving line 50
  17. instance OAI.SLEExactGauge.Target.(instance at line 54) line 54
  18. def OAI.SLEExactGauge.Target.flow line 57
  19. def OAI.SLEExactGauge.Target.IsHausdorffGauge line 60
  20. def OAI.SLEExactGauge.Target.hausdorff line 63
  21. def OAI.SLEExactGauge.Target.inverseFlow line 66
  22. def OAI.SLEExactGauge.Target.trace line 70
  23. def OAI.SLEExactGauge.Target.IsChordalSLE line 74
  24. def OAI.SLEExactGauge.QuadraticEnvelope.profile line 86
  25. def OAI.SLEExactGauge.QuadraticEnvelope.full line 89
  26. lemma OAI.SLEExactGauge.QuadraticEnvelope.profile_nonneg line 94
  27. lemma OAI.SLEExactGauge.QuadraticEnvelope.base_le_profile line 100
  28. lemma OAI.SLEExactGauge.QuadraticEnvelope.profile_mono line 106
  29. lemma OAI.SLEExactGauge.QuadraticEnvelope.profile_scale_le line 114
  30. lemma OAI.SLEExactGauge.QuadraticEnvelope.full_zero line 133
  31. lemma OAI.SLEExactGauge.QuadraticEnvelope.full_of_nonpos line 135
  32. lemma OAI.SLEExactGauge.QuadraticEnvelope.full_of_pos line 138
  33. lemma OAI.SLEExactGauge.QuadraticEnvelope.profiles_bddBelow line 142
  34. lemma OAI.SLEExactGauge.QuadraticEnvelope.le_full line 150
  35. lemma OAI.SLEExactGauge.QuadraticEnvelope.full_nonneg line 155
  36. lemma OAI.SLEExactGauge.QuadraticEnvelope.full_le_profile line 162
  37. lemma OAI.SLEExactGauge.QuadraticEnvelope.full_monoOn line 170
  38. theorem OAI.SLEExactGauge.QuadraticEnvelope.full_scale_le line 181
  39. lemma OAI.SLEExactGauge.QuadraticEnvelope.power_lower_bound line 198
  40. lemma OAI.SLEExactGauge.QuadraticEnvelope.full_pos line 225
  41. lemma OAI.SLEExactGauge.QuadraticEnvelope.ratio_bounds line 231
  42. lemma OAI.SLEExactGauge.QuadraticEnvelope.continuousAt_pos line 260
  43. lemma OAI.SLEExactGauge.QuadraticEnvelope.continuousAt_zero line 274
  44. theorem OAI.SLEExactGauge.QuadraticEnvelope.isHausdorffGauge line 298
  45. theorem OAI.SLEExactGauge.QuadraticEnvelope.restore_finite line 309
  46. def OAI.SLEExactGauge.Target.diskMap line 352
  47. def OAI.SLEExactGauge.Target.diskMapInv line 355
  48. def OAI.SLEExactGauge.Target.centeredFlow line 358
  49. def OAI.SLEExactGauge.Target.clock line 361
  50. def OAI.SLEExactGauge.Target.initialRadius line 366
  51. def OAI.SLEExactGauge.Target.radius line 369
  52. def OAI.SLEExactGauge.Target.angle line 372
  53. def OAI.SLEExactGauge.Target.green line 375
  54. def OAI.SLEExactGauge.Target.levelTime line 380
  55. def OAI.SLEExactGauge.Target.diskK line 384
  56. def OAI.SLEExactGauge.Target.potential line 386
  57. def OAI.SLEExactGauge.Target.concat line 389
  58. def OAI.SLEExactGauge.Target.potentialDifference line 401
  59. def OAI.SLEExactGauge.Target.discreteMass line 407
  60. def OAI.SLEExactGauge.Target.levelDensity line 412
  61. def OAI.SLEExactGauge.Target.angleLaw line 417
  62. def OAI.SLEExactGauge.Target.clip line 422
  63. def OAI.SLEExactGauge.Target.finiteMoment line 424
  64. def OAI.SLEExactGauge.Target.moment line 429
  65. def OAI.SLEExactGauge.Target.batchLevel line 432
  66. def OAI.SLEExactGauge.Target.threshold line 435
  67. def OAI.SLEExactGauge.Target.multiplicity line 438
  68. abbrev OAI.SLEExactGauge.Target.Entry line 442
  69. def OAI.SLEExactGauge.Target.ValidEntry line 444
  70. def OAI.SLEExactGauge.Target.entryValue line 449
  71. def OAI.SLEExactGauge.Target.entryPosition line 454
  72. def OAI.SLEExactGauge.Target.entryRadius line 459
  73. def OAI.SLEExactGauge.Target.entryCost line 463
  74. def OAI.SLEExactGauge.Target.gauge line 466
  75. theorem OAI.SLEExactGauge.Intervals.all_real_of_all_rational line 473
  76. theorem OAI.SLEExactGauge.Intervals.ae_all_real_of_ae_rational line 495
  77. abbrev OAI.SLEExactGauge.Target.GaugeIndex line 512
  78. def OAI.SLEExactGauge.Target.cleanupIndex line 514
  79. instance OAI.SLEExactGauge.Target.(instance at line 517) line 517
  80. abbrev OAI.SLEExactGauge.Target.weights line 520
  81. abbrev OAI.SLEExactGauge.Target.radii line 521
  82. lemma OAI.SLEExactGauge.Target.weights_pos line 523
  83. lemma OAI.SLEExactGauge.Target.radii_pos line 533
  84. lemma OAI.SLEExactGauge.Target.gauge_eq_full line 536
  85. lemma OAI.SLEExactGauge.Target.internal_a_pos line 550
  86. lemma OAI.SLEExactGauge.Target.dimension_pos line 552
  87. lemma OAI.SLEExactGauge.Target.cleanup_radius_le line 557
  88. lemma OAI.SLEExactGauge.Target.cleanup_base_le line 567
  89. lemma OAI.SLEExactGauge.Target.cleanup_small line 578
  90. theorem OAI.SLEExactGauge.Target.gauge_basic_properties line 598
  91. theorem OAI.SLEExactGauge.Target.hausdorff_arbitrary_covers line 616
  92. lemma OAI.SLEExactGauge.Target.trace_isChordalSLE line 636
  93. theorem OAI.SLEExactGauge.Target.transfer_interval_estimates line 641
  94. lemma OAI.SLEExactGauge.Target.dimension_eq line 666
  95. lemma OAI.SLEExactGauge.Target.dimension_lt_two line 671
  96. lemma OAI.SLEExactGauge.Target.multiplicity_positive_bounds line 675
  97. lemma OAI.SLEExactGauge.Target.weights_lower_of_moment_inequalities line 693
  98. theorem OAI.SLEExactGauge.Target.gauge_admissible_of_moment_inequalities line 710
  99. lemma OAI.SLEExactGauge.Target.multiplicity_support_finite line 723
  100. lemma OAI.SLEExactGauge.Target.repeated_entries_finite line 741
  101. lemma OAI.SLEExactGauge.Target.batch_entries_finite line 751
  102. lemma OAI.SLEExactGauge.Target.early_entries_finite line 765
  103. theorem OAI.SLEExactGauge.Target.gauge_restore_early_batches line 775