OAI/Probability/SLEGauge/InverseDomains.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

Hausdorff gauges, Loewner evolution and trace measures.

  1. lemma OAI.SLEExactGauge.LiteralTrace.PositiveSolution.surviving line 20
  2. lemma OAI.SLEExactGauge.LiteralTrace.cutoff_positiveSolution line 37
  3. lemma OAI.SLEExactGauge.LiteralTrace.PositiveSolution.restrict line 52
  4. lemma OAI.SLEExactGauge.LiteralTrace.PositiveSolution.flow_eq line 59
  5. lemma OAI.SLEExactGauge.LiteralTrace.PositiveSolution.flow_eqOn line 66
  6. lemma OAI.SLEExactGauge.LiteralTrace.surviving_iff_positiveSolution line 70
  7. lemma OAI.SLEExactGauge.LiteralTrace.surviving_flow_positiveSolution line 78
  8. lemma OAI.SLEExactGauge.LiteralTrace.PositiveSolution.extend line 96
  9. def OAI.SLEExactGauge.LiteralTrace.clockIntegrand line 135
  10. def OAI.SLEExactGauge.LiteralTrace.rawClock line 138
  11. lemma OAI.SLEExactGauge.LiteralTrace.PositiveSolution.shifted_ne_zero line 141
  12. lemma OAI.SLEExactGauge.LiteralTrace.PositiveSolution.continuous_clockIntegrand line 148
  13. def OAI.SLEExactGauge.LiteralTrace.timeClip line 155
  14. lemma OAI.SLEExactGauge.LiteralTrace.continuous_timeClip line 156
  15. lemma OAI.SLEExactGauge.LiteralTrace.timeClip_mem line 157
  16. lemma OAI.SLEExactGauge.LiteralTrace.timeClip_eq line 159
  17. def OAI.SLEExactGauge.LiteralTrace.pathClock line 164
  18. lemma OAI.SLEExactGauge.LiteralTrace.PositiveSolution.continuous_timeClippedIntegrand line 167
  19. lemma OAI.SLEExactGauge.LiteralTrace.PositiveSolution.pathClock_deriv line 171
  20. lemma OAI.SLEExactGauge.LiteralTrace.PositiveSolution.pathClock_continuous line 179
  21. lemma OAI.SLEExactGauge.LiteralTrace.PositiveSolution.rawClock_eq line 183
  22. lemma OAI.SLEExactGauge.LiteralTrace.PositiveSolution.pathClock_strictMono line 194
  23. lemma OAI.SLEExactGauge.LiteralTrace.PositiveSolution.rawClock_strictMono line 203
  24. def OAI.SLEExactGauge.LiteralTrace.rawLevelTime line 212
  25. lemma OAI.SLEExactGauge.LiteralTrace.clock_eq_rawClock line 216
  26. lemma OAI.SLEExactGauge.LiteralTrace.levelTime_eq_rawLevelTime line 218
  27. lemma OAI.SLEExactGauge.LiteralTrace.rawClock_zero line 220
  28. lemma OAI.SLEExactGauge.LiteralTrace.PositiveSolution.rawClock_continuous line 223
  29. lemma OAI.SLEExactGauge.LiteralTrace.PositiveSolution.rawLevelTime_eq line 229
  30. lemma OAI.SLEExactGauge.LiteralTrace.rawLevelTime_eq_top_of_no_hit line 261
  31. lemma OAI.SLEExactGauge.LiteralTrace.cutoffField_lipschitz line 282
  32. lemma OAI.SLEExactGauge.LiteralTrace.PositiveSolution.initial_eq_of_terminal_eq line 291
  33. lemma OAI.SLEExactGauge.LiteralTrace.flow_injOn line 324
  34. lemma OAI.SLEExactGauge.LiteralTrace.inverseFlow_spec line 330
  35. lemma OAI.SLEExactGauge.LiteralTrace.inverseFlow_flow line 337
  36. lemma OAI.SLEExactGauge.LiteralTrace.reverse_height_formula line 349
  37. lemma OAI.SLEExactGauge.LiteralTrace.reverse_height_le line 380
  38. lemma OAI.SLEExactGauge.Cutoff.field_im line 395
  39. lemma OAI.SLEExactGauge.Cutoff.field_eq_div line 400