OAI/Probability/SLEGauge/StoppingMeasurability.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

Hausdorff gauges, Loewner evolution and trace measures.

  1. lemma OAI.SLEExactGauge.RationalStop.measurableSet_safe line 37
  2. lemma OAI.SLEExactGauge.RationalStop.safe_past line 44
  3. def OAI.SLEExactGauge.RationalStop.Exit line 56
  4. lemma OAI.SLEExactGauge.RationalStop.exit_mem line 59
  5. lemma OAI.SLEExactGauge.RationalStop.exit_bounds line 67
  6. lemma OAI.SLEExactGauge.RationalStop.exit_le line 75
  7. lemma OAI.SLEExactGauge.RationalStop.lt_exit_iff line 80
  8. lemma OAI.SLEExactGauge.RationalStop.bound_until_exit line 101
  9. lemma OAI.SLEExactGauge.RationalStop.measurable_exit line 127
  10. lemma OAI.SLEExactGauge.RationalStop.measurable_stopped_eval line 148
  11. lemma OAI.SLEExactGauge.AngleCalculus.contDiffAt_V line 167
  12. lemma OAI.SLEExactGauge.OnePoint.contDiffOn_field line 177
  13. lemma OAI.SLEExactGauge.OnePoint.exists_cutoff_field line 193
  14. theorem OAI.SLEExactGauge.OnePoint.exists_stopped_green line 215
  15. def OAI.SLEExactGauge.ReverseDerivative.r line 305
  16. def OAI.SLEExactGauge.ReverseDerivative.zeta line 306
  17. def OAI.SLEExactGauge.ReverseDerivative.lambda line 307
  18. def OAI.SLEExactGauge.ReverseDerivative.R line 308
  19. def OAI.SLEExactGauge.ReverseDerivative.D line 309
  20. def OAI.SLEExactGauge.ReverseDerivative.H line 311
  21. def OAI.SLEExactGauge.ReverseDerivative.F line 314
  22. def OAI.SLEExactGauge.ReverseDerivative.Hx line 315
  23. def OAI.SLEExactGauge.ReverseDerivative.Hxx line 316
  24. def OAI.SLEExactGauge.ReverseDerivative.Hy line 318
  25. def OAI.SLEExactGauge.ReverseDerivative.residual line 321
  26. lemma OAI.SLEExactGauge.ReverseDerivative.R_pos line 325
  27. lemma OAI.SLEExactGauge.ReverseDerivative.D_pos line 329
  28. lemma OAI.SLEExactGauge.ReverseDerivative.parameters line 332
  29. lemma OAI.SLEExactGauge.ReverseDerivative.residual_nonneg line 352
  30. lemma OAI.SLEExactGauge.ReverseDerivative.hasDerivAt_Hx line 363
  31. lemma OAI.SLEExactGauge.ReverseDerivative.hasDerivAt_Hxx line 375
  32. lemma OAI.SLEExactGauge.ReverseDerivative.deriv_Fx line 391
  33. lemma OAI.SLEExactGauge.ReverseDerivative.deriv_Fxx line 396
  34. lemma OAI.SLEExactGauge.ReverseDerivative.generator_identity line 406
  35. lemma OAI.SLEExactGauge.ReverseDerivative.generator_nonpos line 420
  36. abbrev OAI.SLEExactGauge.ReverseDerivative.State line 434
  37. def OAI.SLEExactGauge.ReverseDerivative.test line 436
  38. def OAI.SLEExactGauge.ReverseDerivative.vector line 439
  39. lemma OAI.SLEExactGauge.ReverseDerivative.differentiableAt_test line 442