OAI/Probability/SLEGauge/StateBounds.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Hausdorff gauges, Loewner evolution and trace measures.

  1. def OAI.ExactSLEGreen.regimeState line 22
  2. lemma OAI.ExactSLEGreen.regimeState_continuous line 26
  3. lemma OAI.ExactSLEGreen.regimeState_adapted line 35
  4. lemma OAI.ExactSLEGreen.regimeState_eq line 47
  5. lemma OAI.ExactSLEGreen.regimeDiscount_congr line 81
  6. theorem OAI.ExactSLEGreen.vector_regime_weighted_optional line 98
  7. theorem OAI.ExactSLEGreen.vector_regime_weighted_optional_bounded line 146
  8. lemma OAI.ExactSLEMain.upper_pair_norm_sq line 203
  9. lemma OAI.ExactSLEMain.upper_pair_norm_lt line 209
  10. lemma OAI.ExactSLEMain.upper_harnack line 215
  11. lemma OAI.ExactSLEMain.upper_velocity_harnack line 232
  12. lemma OAI.ExactSLEMain.upper_initial_growth line 256
  13. lemma OAI.ExactSLEMain.complex_linear_norm_deriv line 290
  14. lemma OAI.ExactSLEMain.loewner_pair_drift line 302
  15. lemma OAI.ExactSLEMain.growth_factor_deriv line 316
  16. lemma OAI.ExactSLEMain.odeUntil_pair_ne line 328
  17. lemma OAI.ExactSLEMain.odeUntil_pair_ratio_deriv line 344