OAI/Probability/SLEGauge/BrownianGerm.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

Hausdorff gauges, Loewner evolution and trace measures.

  1. def OAI.SLEExactGauge.BrownianGerm.future line 21
  2. lemma OAI.SLEExactGauge.BrownianGerm.measurable_shift line 25
  3. lemma OAI.SLEExactGauge.BrownianGerm.future_le line 30
  4. lemma OAI.SLEExactGauge.BrownianGerm.future_antitone line 35
  5. lemma OAI.SLEExactGauge.BrownianGerm.measurable_eval_iSup_future line 49
  6. theorem OAI.SLEExactGauge.BrownianGerm.measure_zero_or_one line 70
  7. lemma OAI.SLEExactGauge.BrownianGerm.measurableSet_limsup_germ line 106
  8. theorem OAI.SLEExactGauge.BrownianGerm.measure_zero_or_one_limsup line 124
  9. lemma OAI.SLEExactGauge.GermPositivity.mem_limsup_iff_mem_iInter line 150
  10. lemma OAI.SLEExactGauge.GermPositivity.limsup_ae_eq_iInter line 162
  11. theorem OAI.SLEExactGauge.GermPositivity.ae_all_mem line 169
  12. def OAI.SLEExactGauge.GermPositivity.smallTime line 198
  13. lemma OAI.SLEExactGauge.GermPositivity.smallTime_pos line 200
  14. lemma OAI.SLEExactGauge.GermPositivity.smallTime_antitone line 202
  15. lemma OAI.SLEExactGauge.GermPositivity.tendsto_smallTime line 208
  16. theorem OAI.SLEExactGauge.GermPositivity.ae_positive_all_times line 215
  17. theorem OAI.SLEExactGauge.GermPositivity.ae_positive_all_times_of_same_probability line 239
  18. lemma OAI.ExactSLEGreen.physicalGreen_split_bound line 268
  19. lemma OAI.ExactSLEGreen.killedGreen_split_bound line 306
  20. lemma OAI.ExactSLEGreen.killedObservable_real_joint_measurable line 324
  21. lemma OAI.ExactSLEGreen.killedGreen_timeIntegral_bound line 331
  22. theorem OAI.ExactSLEGreen.killedGreen_polynomial_decay line 419
  23. theorem OAI.ExactSLEGreen.killedGreen_mean_tendsto_zero line 462
  24. theorem OAI.ExactSLEGreen.survivingGreen_mean_tendsto_zero line 476
  25. theorem OAI.ExactSLEGreen.survivingGreen_lintegral_tendsto_zero line 484
  26. lemma OAI.ExactSLEGreen.survivingGreen_lintegral_le_initial line 514
  27. theorem OAI.ExactSLEGreen.survivingGreen_compact_mean_tendsto_zero line 527