OAI/Probability/SLEGauge/OptionalPastPalm.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

Hausdorff gauges, Loewner evolution and trace measures.

  1. lemma OAI.SLEExactGauge.PastMass.optional_green_set_balance line 19
  2. lemma OAI.SLEExactGauge.PastMass.expected_green_past_kernel line 43
  3. lemma OAI.SLEExactGauge.PastMass.strict_past_mass_ae line 53
  4. lemma OAI.SLEExactGauge.PastMass.strict_past_mass_aemeasurable line 62
  5. lemma OAI.SLEExactGauge.PastMass.strict_past_Palm line 74
  6. structure OAI.SLEExactGauge.PastMass.TracePalmData line 115
  7. def OAI.SLEExactGauge.PastMass.countablePastKernel line 133
  8. lemma OAI.SLEExactGauge.PastMass.TracePalmData.evaluation_adapted line 144
  9. lemma OAI.SLEExactGauge.PastMass.TracePalmData.test_stopping line 148
  10. lemma OAI.SLEExactGauge.PastMass.TracePalmData.compact_expected_finite line 152
  11. lemma OAI.SLEExactGauge.PastMass.TracePalmData.compact_finite line 157
  12. lemma OAI.SLEExactGauge.PastMass.TracePalmData.stopped_Palm line 162
  13. lemma OAI.SLEExactGauge.PastMass.TracePalmData.finite_Palm line 171
  14. lemma OAI.SLEExactGauge.PastMass.TracePalmData.compact_past_aemeasurable line 179
  15. lemma OAI.SLEExactGauge.PastMass.TracePalmData.countable_kernel_measurable line 186
  16. lemma OAI.SLEExactGauge.PastMass.TracePalmData.countable_Palm line 193
  17. lemma OAI.SLEExactGauge.PastMass.TracePalmData.countable_past_aemeasurable line 222
  18. theorem OAI.SLEExactGauge.PastMass.actual_Palm_data line 236
  19. structure OAI.SLEExactGauge.TraceMassContinuity.CanonicalMassData line 268
  20. theorem OAI.SLEExactGauge.TraceMassContinuity.actual_canonical_mass_data line 287
  21. theorem OAI.SLEExactGauge.CenteredMoments.actual_subdisk_positive_moments line 353