OAI/Probability/SLEGauge/FiniteVariationMartingale.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Hausdorff gauges, Loewner evolution and trace measures.

  1. lemma OAI.SLEExactGauge.FiniteVariationMartingale.integral_weighted_increment line 23
  2. lemma OAI.SLEExactGauge.FiniteVariationMartingale.integrable_detector line 48
  3. theorem OAI.SLEExactGauge.FiniteVariationMartingale.ae_eq_zero_at line 57
  4. theorem OAI.SLEExactGauge.FiniteVariationMartingale.ae_all_eq_zero line 117
  5. lemma OAI.SLEExactGauge.CompensatorUniqueness.integrable_at line 154
  6. lemma OAI.SLEExactGauge.CompensatorUniqueness.martingale_sub line 166
  7. theorem OAI.SLEExactGauge.CompensatorUniqueness.ae_all_eq line 182
  8. theorem OAI.SLEExactGauge.CompensatorUniqueness.ae_terminal_eq_of_ae_all_eq line 220
  9. theorem OAI.SLEExactGauge.CompensatorUniqueness.ae_all_measure_eq line 252
  10. theorem OAI.SLEExactGauge.CompensatorUniqueness.ae_terminal_measure_eq line 304
  11. theorem OAI.SLEExactGauge.CompensatorUniqueness.ae_all_random_weight_eq line 325
  12. theorem OAI.SLEExactGauge.CompensatorUniqueness.ae_all_measure_eq_of_ae_regular line 355
  13. theorem OAI.SLEExactGauge.CompensatorUniqueness.ae_terminal_measure_eq_of_ae_regular line 421
  14. lemma OAI.SLEExactGauge.MassVersions.integrable_test_of_ae_measure_le line 457
  15. lemma OAI.SLEExactGauge.MassVersions.double_lintegral_ofReal_eq line 469
  16. lemma OAI.SLEExactGauge.MassVersions.condExp_sub_eq_of_lintegral_potential line 485