OAI/Probability/SLEGauge/ReverseGenerators.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

Hausdorff gauges, Loewner evolution and trace measures.

  1. lemma OAI.SLEExactGauge.ReverseDerivative.line_deriv_test line 40
  2. lemma OAI.SLEExactGauge.ReverseDerivative.fderiv_test_vector line 77
  3. lemma OAI.SLEExactGauge.ReverseDerivative.second_driver_test line 99
  4. lemma OAI.SLEExactGauge.ReverseDerivative.test_generator_nonpos line 118
  5. def OAI.SLEExactGauge.ReverseDerivative.domain line 132
  6. lemma OAI.SLEExactGauge.ReverseDerivative.isOpen_domain line 134
  7. lemma OAI.SLEExactGauge.ReverseDerivative.contDiffOn_test line 140
  8. lemma OAI.SLEExactGauge.ReverseDerivative.contDiffOn_vector line 162
  9. def OAI.SLEExactGauge.ReverseDerivative.globalVector line 185
  10. def OAI.SLEExactGauge.ReverseDerivative.bound line 188
  11. def OAI.SLEExactGauge.ReverseDerivative.lipBound line 190
  12. lemma OAI.SLEExactGauge.ReverseDerivative.continuous_globalVector line 192
  13. lemma OAI.SLEExactGauge.ReverseDerivative.norm_globalVector_le line 201
  14. lemma OAI.SLEExactGauge.ReverseDerivative.inverse_sq_sub_le line 222
  15. lemma OAI.SLEExactGauge.ReverseDerivative.globalVector_sub_le line 231
  16. lemma OAI.SLEExactGauge.ReverseDerivative.inverse_eq_of_height line 261
  17. lemma OAI.SLEExactGauge.ReverseDerivative.globalVector_eq line 268
  18. def OAI.SLEExactGauge.ReverseDerivative.timeClip line 275
  19. lemma OAI.SLEExactGauge.ReverseDerivative.continuous_timeClip line 276
  20. lemma OAI.SLEExactGauge.ReverseDerivative.timeClip_mem line 277
  21. lemma OAI.SLEExactGauge.ReverseDerivative.timeClip_eq line 279
  22. lemma OAI.SLEExactGauge.ReverseDerivative.reverse_height_formula line 282
  23. lemma OAI.SLEExactGauge.ReverseDerivative.reverse_height_le line 313
  24. lemma OAI.SLEExactGauge.ReverseDerivative.globalVector_height line 325
  25. def OAI.SLEExactGauge.ReverseDerivative.initial line 330
  26. def OAI.SLEExactGauge.ReverseDerivative.reverseFlow line 331
  27. lemma OAI.SLEExactGauge.ReverseDerivative.reverseFlow_solution line 334
  28. lemma OAI.SLEExactGauge.ReverseDerivative.reverseFlow_height line 343
  29. lemma OAI.SLEExactGauge.ReverseDerivative.reverseFlow_time line 374
  30. lemma OAI.SLEExactGauge.ReverseDerivative.reverseFlow_actual line 393