OAI/Probability/SLEGauge/GaugeBounds.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

Hausdorff gauges, Loewner evolution and trace measures.

  1. instance OAI.SLEExactGauge.BrownianLaw.(instance at line 30) line 30
  2. def OAI.SLEExactGauge.BrownianLaw.code line 32
  3. lemma OAI.SLEExactGauge.BrownianLaw.measurable_code line 34
  4. lemma OAI.SLEExactGauge.BrownianLaw.dense_rational_time line 37
  5. lemma OAI.SLEExactGauge.BrownianLaw.code_injective line 41
  6. lemma OAI.SLEExactGauge.BrownianLaw.code_embedding line 47
  7. lemma OAI.SLEExactGauge.BrownianLaw.evaluation_law_unique line 49
  8. def OAI.SLEExactGauge.Deterministic.diameterCost line 77
  9. lemma OAI.SLEExactGauge.Deterministic.diameterCost_zero line 80
  10. lemma OAI.SLEExactGauge.Deterministic.gauge_nonneg line 84
  11. theorem OAI.SLEExactGauge.Deterministic.hausdorff_countable_covers line 91
  12. theorem OAI.SLEExactGauge.Deterministic.hausdorff_tendsto_content line 111
  13. theorem OAI.SLEExactGauge.Deterministic.mass_bound line 120
  14. theorem OAI.SLEExactGauge.Deterministic.hausdorff_pos_of_mass_bound line 132
  15. theorem OAI.SLEExactGauge.Deterministic.hausdorff_le_liminf_cost line 146
  16. theorem OAI.SLEExactGauge.Deterministic.all_real_intervals_of_rational line 162
  17. theorem OAI.SLEExactGauge.Deterministic.ae_all_real_intervals_iff_rational line 186
  18. def OAI.SLEExactGauge.QuadraticGauge.entry line 221
  19. def OAI.SLEExactGauge.QuadraticGauge.gauge line 224
  20. lemma OAI.SLEExactGauge.QuadraticGauge.entry_nonneg line 227
  21. lemma OAI.SLEExactGauge.QuadraticGauge.base_le_entry line 232
  22. lemma OAI.SLEExactGauge.QuadraticGauge.entry_eq_base line 237
  23. lemma OAI.SLEExactGauge.QuadraticGauge.entry_mono line 244
  24. lemma OAI.SLEExactGauge.QuadraticGauge.entry_scale line 251
  25. lemma OAI.SLEExactGauge.QuadraticGauge.power_le_entry line 264
  26. lemma OAI.SLEExactGauge.QuadraticGauge.entry_bddBelow line 294
  27. lemma OAI.SLEExactGauge.QuadraticGauge.gauge_nonneg line 299
  28. lemma OAI.SLEExactGauge.QuadraticGauge.gauge_le_entry line 303
  29. lemma OAI.SLEExactGauge.QuadraticGauge.gauge_mono line 307
  30. lemma OAI.SLEExactGauge.QuadraticGauge.gauge_scale line 311
  31. lemma OAI.SLEExactGauge.QuadraticGauge.gauge_comparison line 322
  32. lemma OAI.SLEExactGauge.QuadraticGauge.gauge_continuousAt line 337
  33. lemma OAI.SLEExactGauge.QuadraticGauge.gauge_zero line 356
  34. lemma OAI.SLEExactGauge.QuadraticGauge.gauge_continuousWithinAt_zero line 365
  35. theorem OAI.SLEExactGauge.QuadraticGauge.isHausdorffGauge line 382
  36. theorem OAI.SLEExactGauge.QuadraticGauge.finite_exclusions line 400