OAI/Probability/SLEGauge/TraceContinuity.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

Hausdorff gauges, Loewner evolution and trace measures.

  1. theorem OAI.SLEExactGauge.LiteralTrace.inverseFlow_time_modulus line 43
  2. def OAI.SLEExactGauge.BrownianCalculus.gaussianMoment line 97
  3. lemma OAI.SLEExactGauge.BrownianCalculus.gaussianMoment_nonneg line 99
  4. lemma OAI.SLEExactGauge.BrownianCalculus.gaussian_abs_pow_integrable line 102
  5. lemma OAI.SLEExactGauge.BrownianCalculus.gaussian_abs_pow_scaled line 107
  6. lemma OAI.SLEExactGauge.BrownianCalculus.increment_abs_pow_scaled line 117
  7. lemma OAI.SLEExactGauge.BrownianCalculus.increment_abs_pow_integrable line 124
  8. lemma OAI.SLEExactGauge.BrownianCalculus.increment_scaled_tail line 131
  9. def OAI.SLEExactGauge.BrownianCalculus.modulusBase line 157
  10. def OAI.SLEExactGauge.BrownianCalculus.modulusStd line 158
  11. def OAI.SLEExactGauge.BrownianCalculus.modulusRate line 159
  12. def OAI.SLEExactGauge.BrownianCalculus.modulusGridBad line 161
  13. lemma OAI.SLEExactGauge.BrownianCalculus.modulus_grid_measure line 165
  14. lemma OAI.SLEExactGauge.BrownianCalculus.modulus_grid_eventually line 194
  15. lemma OAI.SLEExactGauge.BrownianCalculus.modulus_std_square line 209
  16. lemma OAI.SLEExactGauge.BrownianCalculus.modulus_rate_pos line 217
  17. lemma OAI.SLEExactGauge.BrownianCalculus.modulus_rate_lt_one line 220
  18. def OAI.SLEExactGauge.TraceChaining.grid line 235
  19. def OAI.SLEExactGauge.TraceChaining.index line 237
  20. def OAI.SLEExactGauge.TraceChaining.approx line 239
  21. lemma OAI.SLEExactGauge.TraceChaining.approx_bounds line 241
  22. lemma OAI.SLEExactGauge.TraceChaining.approx_tendsto line 252
  23. lemma OAI.SLEExactGauge.TraceChaining.index_le line 265
  24. lemma OAI.SLEExactGauge.TraceChaining.index_refine line 271
  25. lemma OAI.SLEExactGauge.TraceChaining.grid_refine line 276
  26. lemma OAI.SLEExactGauge.TraceChaining.grid_distance_le line 283
  27. lemma OAI.SLEExactGauge.TraceChaining.approx_step line 293
  28. lemma OAI.SLEExactGauge.TraceChaining.approx_distance line 312
  29. lemma OAI.SLEExactGauge.TraceChaining.grid_modulus line 331
  30. lemma OAI.SLEExactGauge.BrownianCalculus.increment_grid_eq line 369
  31. theorem OAI.SLEExactGauge.BrownianCalculus.brownian_uniform_modulus line 386
  32. abbrev OAI.SLEExactGauge.LiteralTrace.radialValue line 414
  33. lemma OAI.SLEExactGauge.LiteralTrace.radial_increment_real line 417
  34. lemma OAI.SLEExactGauge.LiteralTrace.time_bound_below line 423
  35. lemma OAI.SLEExactGauge.LiteralTrace.radial_interpolation line 443
  36. def OAI.SLEExactGauge.LiteralTrace.traceRatio line 461
  37. def OAI.SLEExactGauge.LiteralTrace.traceMeshBase line 462
  38. def OAI.SLEExactGauge.LiteralTrace.brownianModulusConst line 463
  39. def OAI.SLEExactGauge.LiteralTrace.traceError line 466