OAI/Probability/SLEGauge/SubdiskMoments.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

Hausdorff gauges, Loewner evolution and trace measures.

  1. theorem OAI.SLEExactGauge.CenteredMoments.common_limit_subdisk_tilted_moment line 20
  2. def OAI.SLEExactGauge.CenteredMoments.subdiskMoment line 66
  3. theorem OAI.SLEExactGauge.CenteredMoments.common_limit_subdisk_mixed_moment_bound line 72
  4. lemma OAI.SLEExactGauge.CenteredMoments.subdiskMass_monotone line 117
  5. lemma OAI.SLEExactGauge.CenteredMoments.subdiskMass_raw_measurable line 125
  6. lemma OAI.SLEExactGauge.CenteredMoments.subdiskMass_raw_measurable_of_le line 137
  7. lemma OAI.SLEExactGauge.CenteredMoments.subdisk_vector_consistent line 148
  8. theorem OAI.SLEExactGauge.CenteredMoments.exists_subdisk_sequence_law line 178
  9. theorem OAI.SLEExactGauge.CenteredMoments.subdiskSequence_moment line 219
  10. theorem OAI.SLEExactGauge.CenteredMoments.subdiskMoment_monotone line 239
  11. def OAI.SLEExactGauge.PastMass.pastGreenKernel line 276
  12. lemma OAI.SLEExactGauge.PastMass.pastGreenKernel_measurable line 281
  13. lemma OAI.SLEExactGauge.PastMass.initial_mul_pastGreenKernel line 287
  14. lemma OAI.SLEExactGauge.PastMass.pastGreenKernel_eq_ofReal line 294
  15. lemma OAI.SLEExactGauge.PastMass.pastGreenKernel_le_one line 305
  16. lemma OAI.SLEExactGauge.PastMass.pastGreenKernel_antitone line 314
  17. lemma OAI.SLEExactGauge.PastMass.radialLaw_strict_past line 328
  18. theorem OAI.SLEExactGauge.PastMass.radialLaw_strict_past_tendsto line 356
  19. def OAI.SLEExactGauge.PastMass.finiteTestTime line 387
  20. lemma OAI.SLEExactGauge.PastMass.finiteTestTime_lt_iff line 392
  21. lemma OAI.SLEExactGauge.PastMass.finiteTestTime_le_iff line 400
  22. lemma OAI.SLEExactGauge.PastMass.finiteTestTime_stopping line 407
  23. lemma OAI.SLEExactGauge.PastMass.finiteTestTime_antitone line 425
  24. lemma OAI.SLEExactGauge.PastMass.finiteTestTime_iUnion line 432
  25. lemma OAI.SLEExactGauge.PastMass.finiteTestTime_sequence_antitone line 446
  26. def OAI.SLEExactGauge.PastMass.visitTime line 468
  27. lemma OAI.SLEExactGauge.PastMass.stopped_restriction_add line 471
  28. lemma OAI.SLEExactGauge.PastMass.stopped_strictPast_mass line 487
  29. lemma OAI.SLEExactGauge.PastMass.finite_past_mass line 495
  30. lemma OAI.SLEExactGauge.PastMass.all_past_mass_eq_iSup line 508