OAI/Probability/SLEGauge/CutoffFlow.lean

GitHub source file

68 declarations, 0 contain sorry, 0 declared as axioms

Hausdorff gauges, Loewner evolution and trace measures.

  1. abbrev OAI.SLEExactGauge.LiteralTrace.Driver line 18
  2. instance OAI.SLEExactGauge.LiteralTrace.(instance at line 19) line 19
  3. instance OAI.SLEExactGauge.LiteralTrace.(instance at line 20) line 20
  4. abbrev OAI.SLEExactGauge.LiteralTrace.WienerLaw line 21
  5. def OAI.SLEExactGauge.LiteralTrace.IsWiener line 23
  6. def OAI.SLEExactGauge.LiteralTrace.a line 26
  7. def OAI.SLEExactGauge.LiteralTrace.d line 27
  8. def OAI.SLEExactGauge.LiteralTrace.α line 28
  9. def OAI.SLEExactGauge.LiteralTrace.p line 29
  10. def OAI.SLEExactGauge.LiteralTrace.driverValue line 31
  11. def OAI.SLEExactGauge.LiteralTrace.diskMap line 33
  12. def OAI.SLEExactGauge.LiteralTrace.diskMapInv line 36
  13. def OAI.SLEExactGauge.LiteralTrace.cutoffField line 40
  14. def OAI.SLEExactGauge.LiteralTrace.mesh line 44
  15. def OAI.SLEExactGauge.LiteralTrace.eulerSteps line 46
  16. def OAI.SLEExactGauge.LiteralTrace.eulerFlow line 51
  17. def OAI.SLEExactGauge.LiteralTrace.cutoffFlow line 56
  18. def OAI.SLEExactGauge.LiteralTrace.Surviving line 59
  19. instance OAI.SLEExactGauge.LiteralTrace.(instance at line 63) line 63
  20. def OAI.SLEExactGauge.LiteralTrace.flow line 66
  21. def OAI.SLEExactGauge.LiteralTrace.centeredFlow line 69
  22. def OAI.SLEExactGauge.LiteralTrace.clock line 73
  23. def OAI.SLEExactGauge.LiteralTrace.initialRadius line 78
  24. def OAI.SLEExactGauge.LiteralTrace.radius line 81
  25. def OAI.SLEExactGauge.LiteralTrace.angle line 84
  26. def OAI.SLEExactGauge.LiteralTrace.green line 87
  27. def OAI.SLEExactGauge.LiteralTrace.levelTime line 93
  28. def OAI.SLEExactGauge.LiteralTrace.diskK line 97
  29. def OAI.SLEExactGauge.LiteralTrace.potential line 99
  30. def OAI.SLEExactGauge.LiteralTrace.concat line 104
  31. def OAI.SLEExactGauge.LiteralTrace.potentialDifference line 117
  32. def OAI.SLEExactGauge.LiteralTrace.discreteMass line 123
  33. def OAI.SLEExactGauge.LiteralTrace.levelDensity line 128
  34. def OAI.SLEExactGauge.LiteralTrace.angleLaw line 134
  35. def OAI.SLEExactGauge.LiteralTrace.clip line 139
  36. def OAI.SLEExactGauge.LiteralTrace.finiteMoment line 143
  37. def OAI.SLEExactGauge.LiteralTrace.moment line 148
  38. def OAI.SLEExactGauge.LiteralTrace.batchLevel line 152
  39. def OAI.SLEExactGauge.LiteralTrace.threshold line 155
  40. def OAI.SLEExactGauge.LiteralTrace.multiplicity line 158
  41. abbrev OAI.SLEExactGauge.LiteralTrace.Entry line 164
  42. def OAI.SLEExactGauge.LiteralTrace.ValidEntry line 166
  43. def OAI.SLEExactGauge.LiteralTrace.entryValue line 171
  44. def OAI.SLEExactGauge.LiteralTrace.entryPosition line 176
  45. def OAI.SLEExactGauge.LiteralTrace.entryRadius line 181
  46. def OAI.SLEExactGauge.LiteralTrace.entryCost line 185
  47. def OAI.SLEExactGauge.LiteralTrace.gauge line 189
  48. def OAI.SLEExactGauge.LiteralTrace.IsHausdorffGauge line 192
  49. def OAI.SLEExactGauge.LiteralTrace.hausdorff line 196
  50. def OAI.SLEExactGauge.LiteralTrace.inverseFlow line 199
  51. def OAI.SLEExactGauge.LiteralTrace.trace line 204
  52. def OAI.SLEExactGauge.LiteralTrace.MainObligation line 210
  53. def OAI.SLEExactGauge.Cutoff.denominator line 226
  54. def OAI.SLEExactGauge.Cutoff.inverse line 228
  55. lemma OAI.SLEExactGauge.Cutoff.denominator_pos line 230
  56. lemma OAI.SLEExactGauge.Cutoff.q_mul_norm_le_denominator line 233
  57. lemma OAI.SLEExactGauge.Cutoff.norm_inverse_le line 245
  58. lemma OAI.SLEExactGauge.Cutoff.denominator_sub_le line 255
  59. lemma OAI.SLEExactGauge.Cutoff.inverse_sub_bound_ordered line 275
  60. lemma OAI.SLEExactGauge.Cutoff.inverse_sub_bound line 325
  61. lemma OAI.SLEExactGauge.Cutoff.lipschitz_inverse line 331
  62. def OAI.SLEExactGauge.Cutoff.field line 339
  63. lemma OAI.SLEExactGauge.Cutoff.norm_field_le line 342
  64. lemma OAI.SLEExactGauge.Cutoff.field_sub_le line 349
  65. lemma OAI.SLEExactGauge.Cutoff.continuous_field_time line 356
  66. lemma OAI.SLEExactGauge.Cutoff.field_joint_sub_le line 361
  67. theorem OAI.SLEExactGauge.Cutoff.exists_solution_on_compact line 377
  68. def OAI.SLEExactGauge.Euler.nodes line 410