OAI/Probability/SLE/Gauge/GaugeCompletion.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

Continuous monotone completions of the explicit and exponent-one log-log gauges.

  1. def OAI.SLEExactGauge.GaugeCompletion.cutoff line 16
  2. def OAI.SLEExactGauge.GaugeCompletion.tailProfile line 18
  3. def OAI.SLEExactGauge.GaugeCompletion.completed line 20
  4. lemma OAI.SLEExactGauge.GaugeCompletion.cutoff_one_lt line 23
  5. lemma OAI.SLEExactGauge.GaugeCompletion.cutoff_pos line 25
  6. lemma OAI.SLEExactGauge.GaugeCompletion.log_one_le line 27
  7. lemma OAI.SLEExactGauge.GaugeCompletion.tailProfile_pos line 30
  8. lemma OAI.SLEExactGauge.GaugeCompletion.tailProfile_continuousAt line 33
  9. lemma OAI.SLEExactGauge.GaugeCompletion.tailProfile_hasDerivAt line 40
  10. lemma OAI.SLEExactGauge.GaugeCompletion.tailProfile_antitoneOn line 54
  11. lemma OAI.SLEExactGauge.GaugeCompletion.tailProfile_tendsto_zero line 69
  12. lemma OAI.SLEExactGauge.GaugeCompletion.log_inv_tendsto_atTop line 86
  13. lemma OAI.SLEExactGauge.GaugeCompletion.completed_zero line 91
  14. lemma OAI.SLEExactGauge.GaugeCompletion.completed_eq_tail_eventually line 94
  15. lemma OAI.SLEExactGauge.GaugeCompletion.completed_tendsto_zero line 101
  16. lemma OAI.SLEExactGauge.GaugeCompletion.completed_continuousAt_pos line 106
  17. lemma OAI.SLEExactGauge.GaugeCompletion.completed_monotoneOn line 122
  18. theorem OAI.SLEExactGauge.GaugeCompletion.completed_isGauge line 144
  19. lemma OAI.SLEExactGauge.GaugeCompletion.tailProfile_log_inv line 157
  20. lemma OAI.SLEExactGauge.GaugeCompletion.completed_small_formula line 167
  21. def OAI.SLEExactGauge.explicitGauge line 177

    Source documentation

    A fixed, deterministic continuous nondecreasing completion of the explicit exact Hausdorff gauge.

    def explicitGauge (κ : ℝ) : ℝ → ℝ :=
…
  22. def OAI.SLEExactGauge.schrammGauge line 182

    Source documentation

    A deterministic completion of the exponent-one log-log gauge proposed by Schramm.

    def schrammGauge (κ : ℝ) : ℝ → ℝ :=
…
  23. theorem OAI.SLEExactGauge.explicitGauge_isGauge line 185
  24. theorem OAI.SLEExactGauge.explicitGauge_small_formula line 192
  25. theorem OAI.SLEExactGauge.schrammGauge_isGauge line 196
  26. theorem OAI.SLEExactGauge.schrammGauge_small_formula line 202
  27. theorem OAI.SLEExactGauge.exists_explicitGauge line 209