OAI/Probability/SLEGauge/SpatialPastTail.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

Hausdorff gauges, Loewner evolution and trace measures.

  1. lemma OAI.SLEExactGauge.CenteredMoments.half_le_subdiskRadius line 20
  2. lemma OAI.SLEExactGauge.CenteredMoments.radial_exp_tendsto line 26
  3. lemma OAI.SLEExactGauge.CenteredMoments.CenteredMomentModel.finite_past_tail line 37
  4. lemma OAI.SLEExactGauge.CenteredMoments.CenteredMomentModel.past_kernel_tail line 78
  5. lemma OAI.SLEExactGauge.CenteredMoments.CenteredMomentModel.rational_past_kernel_tail line 106
  6. lemma OAI.SLEExactGauge.CenteredMoments.CenteredMomentModel.expected_spatial_bad_mass line 122
  7. lemma OAI.SLEExactGauge.CenteredMoments.clock_gap_of_small line 173
  8. lemma OAI.SLEExactGauge.CenteredMoments.batchRadius_eventually_small line 188
  9. lemma OAI.SLEExactGauge.CenteredMoments.compact_batch_mixing line 197
  10. abbrev OAI.SLEExactGauge.CenteredMoments.CenteredMomentModel.Entries line 217
  11. def OAI.SLEExactGauge.CenteredMoments.CenteredMomentModel.entryThreshold line 219
  12. def OAI.SLEExactGauge.CenteredMoments.CenteredMomentModel.entryRadius line 221
  13. lemma OAI.SLEExactGauge.CenteredMoments.CenteredMomentModel.entryRadius_pos line 224
  14. lemma OAI.SLEExactGauge.CenteredMoments.CenteredMomentModel.entryThreshold_pos line 226
  15. lemma OAI.SLEExactGauge.CenteredMoments.CenteredMomentModel.gauge_eq_quadratic line 235
  16. lemma OAI.SLEExactGauge.CenteredMoments.CenteredMomentModel.entry_tails_finite line 238
  17. def OAI.SLEExactGauge.CenteredMoments.spatialRestriction line 261
  18. lemma OAI.SLEExactGauge.CenteredMoments.spatialRestriction_apply line 264
  19. lemma OAI.SLEExactGauge.CenteredMoments.spatialRestriction_mono line 270
  20. lemma OAI.SLEExactGauge.CenteredMoments.spatialRestriction_univ line 274
  21. lemma OAI.SLEExactGauge.CenteredMoments.spatialRestriction_finite line 279
  22. lemma OAI.SLEExactGauge.CenteredMoments.spatialRestriction_atomless line 283
  23. lemma OAI.SLEExactGauge.CenteredMoments.spatialRestriction_measurable line 291
  24. def OAI.SLEExactGauge.CenteredMoments.CenteredMomentModel.gridConstant line 317
  25. lemma OAI.SLEExactGauge.CenteredMoments.CenteredMomentModel.gridConstant_pos line 319
  26. lemma OAI.SLEExactGauge.CenteredMoments.CenteredMomentModel.grid_threshold line 323
  27. theorem OAI.SLEExactGauge.CenteredMoments.CenteredMomentModel.compact_finitely_bad line 337
  28. theorem OAI.SLEExactGauge.CenteredMoments.CenteredMomentModel.hausdorff_positive line 394
  29. def OAI.SLEExactGauge.CenteredMoments.CenteredMomentModel.stoppedTest line 467
  30. lemma OAI.SLEExactGauge.CenteredMoments.CenteredMomentModel.testEndpoint_pos line 471
  31. lemma OAI.SLEExactGauge.CenteredMoments.CenteredMomentModel.testEndpoint_le line 474
  32. lemma OAI.SLEExactGauge.CenteredMoments.CenteredMomentModel.stoppedTest_measurable line 479
  33. lemma OAI.SLEExactGauge.CenteredMoments.CenteredMomentModel.stoppedTest_eq line 487
  34. lemma OAI.SLEExactGauge.CenteredMoments.CenteredMomentModel.subdisk_ge_real_law line 495
  35. theorem OAI.SLEExactGauge.CenteredMoments.CenteredMomentModel.stopped_success_lower line 505